Theorem efi4p

Description: Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypothesis	efi4p.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	efi4p	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		efi4p.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		ax-icn	⊢ i ∈ ℂ
3		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4	2 3	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
5	1	ef4p	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )
6	4 5	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )
7		ax-1cn	⊢ 1 ∈ ℂ
8		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
9	7 4 8	sylancr	⊢ ( 𝐴 ∈ ℂ → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
10	4	sqcld	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) ∈ ℂ )
11	10	halfcld	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ∈ ℂ )
12		3nn0	⊢ 3 ∈ ℕ0
13		expcl	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ )
14	4 12 13	sylancl	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ )
15		6cn	⊢ 6 ∈ ℂ
16		6re	⊢ 6 ∈ ℝ
17		6pos	⊢ 0 < 6
18	16 17	gt0ne0ii	⊢ 6 ≠ 0
19		divcl	⊢ ( ( ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ∈ ℂ )
20	15 18 19	mp3an23	⊢ ( ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ∈ ℂ )
21	14 20	syl	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ∈ ℂ )
22	9 11 21	addassd	⊢ ( 𝐴 ∈ ℂ → ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( ( 1 + ( i · 𝐴 ) ) + ( ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) )
23	7	a1i	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
24	23 4 11 21	add4d	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( i · 𝐴 ) ) + ( ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) = ( ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) )
25		2nn0	⊢ 2 ∈ ℕ0
26		mulexp	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
27	2 25 26	mp3an13	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
28		i2	⊢ ( i ↑ 2 ) = - 1
29	28	oveq1i	⊢ ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
30	29	a1i	⊢ ( 𝐴 ∈ ℂ → ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) ) )
31		sqcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
32	31	mulm1d	⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
33	27 30 32	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
34	33	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
35		2cn	⊢ 2 ∈ ℂ
36		2ne0	⊢ 2 ≠ 0
37		divneg	⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( ( 𝐴 ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
38	35 36 37	mp3an23	⊢ ( ( 𝐴 ↑ 2 ) ∈ ℂ → - ( ( 𝐴 ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
39	31 38	syl	⊢ ( 𝐴 ∈ ℂ → - ( ( 𝐴 ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
40	34 39	eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) = - ( ( 𝐴 ↑ 2 ) / 2 ) )
41	40	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) = ( 1 + - ( ( 𝐴 ↑ 2 ) / 2 ) ) )
42	31	halfcld	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℂ )
43		negsub	⊢ ( ( 1 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℂ ) → ( 1 + - ( ( 𝐴 ↑ 2 ) / 2 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
44	7 42 43	sylancr	⊢ ( 𝐴 ∈ ℂ → ( 1 + - ( ( 𝐴 ↑ 2 ) / 2 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
45	41 44	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
46		mulexp	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 3 ) = ( ( i ↑ 3 ) · ( 𝐴 ↑ 3 ) ) )
47	2 12 46	mp3an13	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 3 ) = ( ( i ↑ 3 ) · ( 𝐴 ↑ 3 ) ) )
48		i3	⊢ ( i ↑ 3 ) = - i
49	48	oveq1i	⊢ ( ( i ↑ 3 ) · ( 𝐴 ↑ 3 ) ) = ( - i · ( 𝐴 ↑ 3 ) )
50	47 49	syl6eq	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 3 ) = ( - i · ( 𝐴 ↑ 3 ) ) )
51	50	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) = ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) )
52		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
53	12 52	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 3 ) ∈ ℂ )
54		negicn	⊢ - i ∈ ℂ
55	15 18	pm3.2i	⊢ ( 6 ∈ ℂ ∧ 6 ≠ 0 )
56		divass	⊢ ( ( - i ∈ ℂ ∧ ( 𝐴 ↑ 3 ) ∈ ℂ ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ) → ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) = ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) )
57	54 55 56	mp3an13	⊢ ( ( 𝐴 ↑ 3 ) ∈ ℂ → ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) = ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) )
58	53 57	syl	⊢ ( 𝐴 ∈ ℂ → ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) = ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) )
59		divcl	⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
60	15 18 59	mp3an23	⊢ ( ( 𝐴 ↑ 3 ) ∈ ℂ → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
61	53 60	syl	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
62		mulneg12	⊢ ( ( i ∈ ℂ ∧ ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) )
63	2 61 62	sylancr	⊢ ( 𝐴 ∈ ℂ → ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) )
64	51 58 63	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) = ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) )
65	64	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
66	61	negcld	⊢ ( 𝐴 ∈ ℂ → - ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
67		adddi	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ - ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
68	2 67	mp3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ - ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
69	66 68	mpdan	⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
70		negsub	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) )
71	61 70	mpdan	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) )
72	71	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
73	65 69 72	3eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
74	45 73	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) )
75	22 24 74	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) )
76	75	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )
77	6 76	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )