Euler's identity

   0 = 1 + ^ 1p1 * 0j1

is the most beautiful equation in all of mathematics, relating in one short phrase the fundamental quantities 0, 1, , , and 0j1 and the basic operations plus, times, and exponentiation. It is a particular case of Euler's formula

   (^0j1*x) = (cos x) + 0j1 * (sin x)

Standing on the shoulders of giants, herewith an informal proof of Euler's formula and Euler's identity.

The adverb t. is such that f t. i gives the i-th coefficient of the Taylor expansion of function f . Thus:

   ^ t. i.10
1 1 0.5 0.166667 0.0416667 0.00833333 0.00138889 0.000198413 2.48016e_5 2.75573e_6

If the right argument of the derived function is extended precision, then so too is the result:

   ^ t. i.10x
1 1 1r2 1r6 1r24 1r120 1r720 1r5040 1r40320 1r362880

Similarly for sin and cos:

   sin=: 1&o.
cos=: 2&o.

sin t. i.10x
0 1 0 _1r6 0 1r120 0 _1r5040 0 1r362880
cos t. i.10x
1 0 _1r2 0 1r24 0 _1r720 0 1r40320 0

The related adverb t: gives the coefficients weighted by %!i .  Thus:

   ] e=: ^ t: i.10
1 1 1 1 1 1 1 1 1 1
] s=: sin t: i.10
0 1 0 _1 0 1 0 _1 0 1
] c=: cos t: i.10
1 0 _1 0 1 0 _1 0 1 0

Now for ^0j1*x , the coefficients of the weighted series are:

   ] e1=. e * 0j1 ^ i.10
1 0j1 _1 0j_1 1 0j1 _1 0j_1 1 0j1

Aligning the columns of e1 and the coefficients for sin x and cos x , we get:

   e1 , s ,: c
1 0j1 _1 0j_1 1 0j1 _1 0j_1 1 0j1
0   1  0   _1 0   1  0   _1 0   1
1   0 _1    0 1   0 _1    0 1   0

Staring at this for a while, we note that on terms 0 2 4 6 8 ...  e1 is the same as for c ,  and on terms 1 3 5 7 ... e1 is s*0j1 :

   e1 , (s * 0j1) ,: c
1 0j1 _1 0j_1 1 0j1 _1 0j_1 1 0j1
0 0j1  0 0j_1 0 0j1  0 0j_1 0 0j1
1   0 _1    0 1   0 _1    0 1   0

That is:

   e1 ,: (s * 0j1) + c
1 0j1 _1 0j_1 1 0j1 _1 0j_1 1 0j1
1 0j1 _1 0j_1 1 0j1 _1 0j_1 1 0j1

e1 = (s * 0j1) + c
1 1 1 1 1 1 1 1 1 1

In other words,

   (^0j1*x) = (cos x) + 0j1 * sin x

Since j.y is 0j1*y and x j. y is x+0j1*y ,

   (^j.x) = (cos x) j. (sin x)

It is not too far a leap to plug in extremal values of the functions. Thus:

   pi=: o. 1
cos pi
_1
sin pi
1.22461e_16

^ 0j1 * pi
_1j1.22461e_16

In J7.01, the composition ^@o. ( composed with times) is supported by special code, and

   ^@o. 0j1
_1