Theorem efi4pt 7385

Description: Separate out the first four terms of the infinite series expansion of the exponential function of a pure imaginary number. (Contributed by Paul Chapman, 19-Jan-2008.)

Hypothesis

Ref	Expression
efit4pt.1	|- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}

Assertion

Ref	Expression
efi4pt	|- (A e. RR -> (exp` (i x. A)) = (((1 - ((A^2) / 2)) + (i x. (A - ((A^3) / 6)))) + sum_k e. (ZZ>` 4)(F` k)))

Distinct variable groups:   A,j,k,y   k,F

Proof of Theorem efi4pt

Step	Hyp	Ref	Expression
1		recnt 5293	. . . 4 |- (A e. RR -> A e. CC)
2		axicn 5250	. . . . 5 |- i e. CC
3		axmulcl 5253	. . . . 5 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
4	2, 3	mpan 694	. . . 4 |- (A e. CC -> (i x. A) e. CC)
5	1, 4	syl 10	. . 3 |- (A e. RR -> (i x. A) e. CC)
6		efit4pt.1	. . . 4 |- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
7	6	ef4pt 7349	. . 3 |- ((i x. A) e. CC -> (exp` (i x. A)) = ((((1 + (i x. A)) + (((i x. A)^2) / 2)) + (((i x. A)^3) / 6)) + sum_k e. (ZZ>` 4)(F` k)))
8	5, 7	syl 10	. 2 |- (A e. RR -> (exp` (i x. A)) = ((((1 + (i x. A)) + (((i x. A)^2) / 2)) + (((i x. A)^3) / 6)) + sum_k e. (ZZ>` 4)(F` k)))
9		axaddass 5257	. . . . 5 |- (((1 + (i x. A)) e. CC /\ (((i x. A)^2) / 2) e. CC /\ (((i x. A)^3) / 6) e. CC) -> (((1 + (i x. A)) + (((i x. A)^2) / 2)) + (((i x. A)^3) / 6)) = ((1 + (i x. A)) + ((((i x. A)^2) / 2) + (((i x. A)^3) / 6))))
10		ax1cn 5249	. . . . . . 7 |- 1 e. CC
11		axaddcl 5251	. . . . . . 7 |- ((1 e. CC /\ (i x. A) e. CC) -> (1 + (i x. A)) e. CC)
12	10, 11	mpan 694	. . . . . 6 |- ((i x. A) e. CC -> (1 + (i x. A)) e. CC)
13	5, 12	syl 10	. . . . 5 |- (A e. RR -> (1 + (i x. A)) e. CC)
14		sqclt 6550	. . . . . . 7 |- ((i x. A) e. CC -> ((i x. A)^2) e. CC)
15	5, 14	syl 10	. . . . . 6 |- (A e. RR -> ((i x. A)^2) e. CC)
16		2cn 5935	. . . . . . 7 |- 2 e. CC
17		2ne0 5945	. . . . . . 7 |- 2 =/= 0
18		divclt 5689	. . . . . . 7 |- ((((i x. A)^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> (((i x. A)^2) / 2) e. CC)
19	16, 17, 18	mp3an23 906	. . . . . 6 |- (((i x. A)^2) e. CC -> (((i x. A)^2) / 2) e. CC)
20	15, 19	syl 10	. . . . 5 |- (A e. RR -> (((i x. A)^2) / 2) e. CC)
21		3nn 5955	. . . . . . . . 9 |- 3 e. NN
22	21	nnnn0 6062	. . . . . . . 8 |- 3 e. NN0
23		expclt 6521	. . . . . . . 8 |- (((i x. A) e. CC /\ 3 e. NN0) -> ((i x. A)^3) e. CC)
24	22, 23	mpan2 695	. . . . . . 7 |- ((i x. A) e. CC -> ((i x. A)^3) e. CC)
25	5, 24	syl 10	. . . . . 6 |- (A e. RR -> ((i x. A)^3) e. CC)
26		6re 5939	. . . . . . . 8 |- 6 e. RR
27	26	recn 5294	. . . . . . 7 |- 6 e. CC
28		6pos 5949	. . . . . . . 8 |- 0 < 6
29	26, 28	gt0ne0i 5599	. . . . . . 7 |- 6 =/= 0
30		divclt 5689	. . . . . . 7 |- ((((i x. A)^3) e. CC /\ 6 e. CC /\ 6 =/= 0) -> (((i x. A)^3) / 6) e. CC)
31	27, 29, 30	mp3an23 906	. . . . . 6 |- (((i x. A)^3) e. CC -> (((i x. A)^3) / 6) e. CC)
32	25, 31	syl 10	. . . . 5 |- (A e. RR -> (((i x. A)^3) / 6) e. CC)
33	9, 13, 20, 32	syl3anc 857	. . . 4 |- (A e. RR -> (((1 + (i x. A)) + (((i x. A)^2) / 2)) + (((i x. A)^3) / 6)) = ((1 + (i x. A)) + ((((i x. A)^2) / 2) + (((i x. A)^3) / 6))))
34		add4t 5318	. . . . 5 |- (((1 e. CC /\ (i x. A) e. CC) /\ ((((i x. A)^2) / 2) e. CC /\ (((i x. A)^3) / 6) e. CC)) -> ((1 + (i x. A)) + ((((i x. A)^2) / 2) + (((i x. A)^3) / 6))) = ((1 + (((i x. A)^2) / 2)) + ((i x. A) + (((i x. A)^3) / 6))))
35	10	a1i 8	. . . . . 6 |- (A e. RR -> 1 e. CC)
36	35, 5	jca 288	. . . . 5 |- (A e. RR -> (1 e. CC /\ (i x. A) e. CC))
37	20, 32	jca 288	. . . . 5 |- (A e. RR -> ((((i x. A)^2) / 2) e. CC /\ (((i x. A)^3) / 6) e. CC))
38	34, 36, 37	sylanc 471	. . . 4 |- (A e. RR -> ((1 + (i x. A)) + ((((i x. A)^2) / 2) + (((i x. A)^3) / 6))) = ((1 + (((i x. A)^2) / 2)) + ((i x. A) + (((i x. A)^3) / 6))))
39		2nn0 6070	. . . . . . . . . . . 12 |- 2 e. NN0
40		mulexpt 6533	. . . . . . . . . . . 12 |- ((i e. CC /\ A e. CC /\ 2 e. NN0) -> ((i x. A)^2) = ((i^2) x. (A^2)))
41	2, 39, 40	mp3an13 905	. . . . . . . . . . 11 |- (A e. CC -> ((i x. A)^2) = ((i^2) x. (A^2)))
42	1, 41	syl 10	. . . . . . . . . 10 |- (A e. RR -> ((i x. A)^2) = ((i^2) x. (A^2)))
43		i2 6670	. . . . . . . . . . . 12 |- (i^2) = -u1
44	43	opreq1i 3962	. . . . . . . . . . 11 |- ((i^2) x. (A^2)) = (-u1 x. (A^2))
45	44	a1i 8	. . . . . . . . . 10 |- (A e. RR -> ((i^2) x. (A^2)) = (-u1 x. (A^2)))
46		sqclt 6550	. . . . . . . . . . . 12 |- (A e. CC -> (A^2) e. CC)
47	1, 46	syl 10	. . . . . . . . . . 11 |- (A e. RR -> (A^2) e. CC)
48		mulm1t 5451	. . . . . . . . . . 11 |- ((A^2) e. CC -> (-u1 x. (A^2)) = -u(A^2))
49	47, 48	syl 10	. . . . . . . . . 10 |- (A e. RR -> (-u1 x. (A^2)) = -u(A^2))
50	42, 45, 49	3eqtrd 1508	. . . . . . . . 9 |- (A e. RR -> ((i x. A)^2) = -u(A^2))
51	50	opreq1d 3966	. . . . . . . 8 |- (A e. RR -> (((i x. A)^2) / 2) = (-u(A^2) / 2))
52		divnegt 5738	. . . . . . . . . 10 |- (((A^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> -u((A^2) / 2) = (-u(A^2) / 2))
53	16, 17, 52	mp3an23 906	. . . . . . . . 9 |- ((A^2) e. CC -> -u((A^2) / 2) = (-u(A^2) / 2))
54	47, 53	syl 10	. . . . . . . 8 |- (A e. RR -> -u((A^2) / 2) = (-u(A^2) / 2))
55	51, 54	eqtr4d 1507	. . . . . . 7 |- (A e. RR -> (((i x. A)^2) / 2) = -u((A^2) / 2))
56	55	opreq2d 3967	. . . . . 6 |- (A e. RR -> (1 + (((i x. A)^2) / 2)) = (1 + -u((A^2) / 2)))
57		divclt 5689	. . . . . . . . 9 |- (((A^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((A^2) / 2) e. CC)
58	16, 17, 57	mp3an23 906	. . . . . . . 8 |- ((A^2) e. CC -> ((A^2) / 2) e. CC)
59	47, 58	syl 10	. . . . . . 7 |- (A e. RR -> ((A^2) / 2) e. CC)
60		negsubt 5362	. . . . . . . 8 |- ((1 e. CC /\ ((A^2) / 2) e. CC) -> (1 + -u((A^2) / 2)) = (1 - ((A^2) / 2)))
61	10, 60	mpan 694	. . . . . . 7 |- (((A^2) / 2) e. CC -> (1 + -u((A^2) / 2)) = (1 - ((A^2) / 2)))
62	59, 61	syl 10	. . . . . 6 |- (A e. RR -> (1 + -u((A^2) / 2)) = (1 - ((A^2) / 2)))
63	56, 62	eqtrd 1504	. . . . 5 |- (A e. RR -> (1 + (((i x. A)^2) / 2)) = (1 - ((A^2) / 2)))
64		mulexpt 6533	. . . . . . . . . . . 12 |- ((i e. CC /\ A e. CC /\ 3 e. NN0) -> ((i x. A)^3) = ((i