HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem efi4pt 7377
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
StepHypRef Expression
1 recnt 5285 . . . 4 |- (A e. RR -> A e. CC)
2 axicn 5242 . . . . 5 |- i e. CC
3 axmulcl 5245 . . . . 5 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
42, 3mpan 693 . . . 4 |- (A e. CC -> (i x. A) e. CC)
51, 4syl 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)))}
76ef4pt 7341 . . 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)))
85, 7syl 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 5249 . . . . 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 5241 . . . . . . 7 |- 1 e. CC
11 axaddcl 5243 . . . . . . 7 |- ((1 e. CC /\ (i x. A) e. CC) -> (1 + (i x. A)) e. CC)
1210, 11mpan 693 . . . . . 6 |- ((i x. A) e. CC -> (1 + (i x. A)) e. CC)
135, 12syl 10 . . . . 5 |- (A e. RR -> (1 + (i x. A)) e. CC)
14 sqclt 6542 . . . . . . 7 |- ((i x. A) e. CC -> ((i x. A)^2) e. CC)
155, 14syl 10 . . . . . 6 |- (A e. RR -> ((i x. A)^2) e. CC)
16 2cn 5927 . . . . . . 7 |- 2 e. CC
17 2ne0 5937 . . . . . . 7 |- 2 =/= 0
18 divclt 5681 . . . . . . 7 |- ((((i x. A)^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> (((i x. A)^2) / 2) e. CC)
1916, 17, 18mp3an23 905 . . . . . 6 |- (((i x. A)^2) e. CC -> (((i x. A)^2) / 2) e. CC)
2015, 19syl 10 . . . . 5 |- (A e. RR -> (((i x. A)^2) / 2) e. CC)
21 3nn 5947 . . . . . . . . 9 |- 3 e. NN
2221nnnn0 6054 . . . . . . . 8 |- 3 e. NN0
23 expclt 6513 . . . . . . . 8 |- (((i x. A) e. CC /\ 3 e. NN0) -> ((i x. A)^3) e. CC)
2422, 23mpan2 694 . . . . . . 7 |- ((i x. A) e. CC -> ((i x. A)^3) e. CC)
255, 24syl 10 . . . . . 6 |- (A e. RR -> ((i x. A)^3) e. CC)
26 6re 5931 . . . . . . . 8 |- 6 e. RR
2726recn 5286 . . . . . . 7 |- 6 e. CC
28 6pos 5941 . . . . . . . 8 |- 0 < 6
2926, 28gt0ne0i 5591 . . . . . . 7 |- 6 =/= 0
30 divclt 5681 . . . . . . 7 |- ((((i x. A)^3) e. CC /\ 6 e. CC /\ 6 =/= 0) -> (((i x. A)^3) / 6) e. CC)
3127, 29, 30mp3an23 905 . . . . . 6 |- (((i x. A)^3) e. CC -> (((i x. A)^3) / 6) e. CC)
3225, 31syl 10 . . . . 5 |- (A e. RR -> (((i x. A)^3) / 6) e. CC)
339, 13, 20, 32syl3anc 856 . . . 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 5310 . . . . 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))))
3510a1i 8 . . . . . 6 |- (A e. RR -> 1 e. CC)
3635, 5jca 288 . . . . 5 |- (A e. RR -> (1 e. CC /\ (i x. A) e. CC))
3720, 32jca 288 . . . . 5 |- (A e. RR -> ((((i x. A)^2) / 2) e. CC /\ (((i x. A)^3) / 6) e. CC))
3834, 36, 37sylanc 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 6062 . . . . . . . . . . . 12 |- 2 e. NN0
40 mulexpt 6525 . . . . . . . . . . . 12 |- ((i e. CC /\ A e. CC /\ 2 e. NN0) -> ((i x. A)^2) = ((i^2) x. (A^2)))
412, 39, 40mp3an13 904 . . . . . . . . . . 11 |- (A e. CC -> ((i x. A)^2) = ((i^2) x. (A^2)))
421, 41syl 10 . . . . . . . . . 10 |- (A e. RR -> ((i x. A)^2) = ((i^2) x. (A^2)))
43 i2 6662 . . . . . . . . . . . 12 |- (i^2) = -u1
4443opreq1i 3956 . . . . . . . . . . 11 |- ((i^2) x. (A^2)) = (-u1 x. (A^2))
4544a1i 8 . . . . . . . . . 10 |- (A e. RR -> ((i^2) x. (A^2)) = (-u1 x. (A^2)))
46 sqclt 6542 . . . . . . . . . . . 12 |- (A e. CC -> (A^2) e. CC)
471, 46syl 10 . . . . . . . . . . 11 |- (A e. RR -> (A^2) e. CC)
48 mulm1t 5443 . . . . . . . . . . 11 |- ((A^2) e. CC -> (-u1 x. (A^2)) = -u(A^2))
4947, 48syl 10 . . . . . . . . . 10 |- (A e. RR -> (-u1 x. (A^2)) = -u(A^2))
5042, 45, 493eqtrd 1503 . . . . . . . . 9 |- (A e. RR -> ((i x. A)^2) = -u(A^2))
5150opreq1d 3960 . . . . . . . 8 |- (A e. RR -> (((i x. A)^2) / 2) = (-u(A^2) / 2))
52 divnegt 5730 . . . . . . . . . 10 |- (((A^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> -u((A^2) / 2) = (-u(A^2) / 2))
5316, 17, 52mp3an23 905 . . . . . . . . 9 |- ((A^2) e. CC -> -u((A^2) / 2) = (-u(A^2) / 2))
5447, 53syl 10 . . . . . . . 8 |- (A e. RR -> -u((A^2) / 2) = (-u(A^2) / 2))
5551, 54eqtr4d 1502 . . . . . . 7 |- (A e. RR -> (((i x. A)^2) / 2) = -u((A^2) / 2))
5655opreq2d 3961 . . . . . 6 |- (A e. RR -> (1 + (((i x. A)^2) / 2)) = (1 + -u((A^2) / 2)))
57 divclt 5681 . . . . . . . . 9 |- (((A^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((A^2) / 2) e. CC)
5816, 17, 57mp3an23 905 . . . . . . . 8 |- ((A^2) e. CC -> ((A^2) / 2) e. CC)
5947, 58syl 10 . . . . . . 7 |- (A e. RR -> ((A^2) / 2) e. CC)
60 negsubt 5354 . . . . . . . 8 |- ((1 e. CC /\ ((A^2) / 2) e. CC) -> (1 + -u((A^2) / 2)) = (1 - ((A^2) / 2)))
6110, 60mpan 693 . . . . . . 7 |- (((A^2) / 2) e. CC -> (1 + -u((A^2) / 2)) = (1 - ((A^2) / 2)))
6259, 61syl 10 . . . . . 6 |- (A e. RR -> (1 + -u((A^2) / 2)) = (1 - ((A^2) / 2)))
6356, 62eqtrd 1499 . . . . 5 |- (A e. RR -> (1 + (((i x. A)^2) / 2)) = (1 - ((A^2) / 2)))
64 mulexpt 6525 . . . . . . . . . . . 12 |- ((i e. CC /\ A e. CC /\ 3 e. NN0) -> ((i x. A)^3) = ((