This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efsep

Description: Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses efsep.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
efsep.2 ⊢ 𝑁 = ( 𝑀 + 1 )
efsep.3 ⊢ 𝑀 ∈ ℕ0
efsep.4 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
efsep.5 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
efsep.6 ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) )
efsep.7 ⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) = 𝐷 )
Assertion efsep ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 efsep.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 efsep.2 ⊢ 𝑁 = ( 𝑀 + 1 )
3 efsep.3 ⊢ 𝑀 ∈ ℕ0
4 efsep.4 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5 efsep.5 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6 efsep.6 ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) )
7 efsep.7 ⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) = 𝐷 )
8 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
9 3 nn0zi ⊢ 𝑀 ∈ ℤ
10 9 a1i ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
11 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
12 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
13 3 12 mpan ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℕ0 )
14 1 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
16 eftcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
17 4 16 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
18 15 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
19 13 18 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
20 1 eftlcvg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
21 4 3 20 sylancl ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
22 8 10 11 19 21 isum1p ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
23 1 eftval ⊢ ( 𝑀 ∈ ℕ0 → ( 𝐹 ‘ 𝑀 ) = ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) )
24 3 23 ax-mp ⊢ ( 𝐹 ‘ 𝑀 ) = ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) )
25 2 eqcomi ⊢ ( 𝑀 + 1 ) = 𝑁
26 25 fveq2i ⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ 𝑁 )
27 26 sumeq1i ⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 )
28 24 27 oveq12i ⊢ ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) )
29 22 28 eqtrdi ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )
30 29 oveq2d ⊢ ( 𝜑 → ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 + ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) )
31 eftcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ )
32 4 3 31 sylancl ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ )
33 peano2nn0 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
34 3 33 ax-mp ⊢ ( 𝑀 + 1 ) ∈ ℕ0
35 2 34 eqeltri ⊢ 𝑁 ∈ ℕ0
36 1 eftlcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
37 4 35 36 sylancl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
38 5 32 37 addassd ⊢ ( 𝜑 → ( ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 + ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) )
39 30 38 eqtr4d ⊢ ( 𝜑 → ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )
40 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )
41 6 39 40 3eqtrd ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )