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

Metamath Proof Explorer

Theorem effsumlt

Description: The partial sums of the series expansion of the exponential function at a positive real number are bounded by the value of the function. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses effsumlt.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
effsumlt.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
effsumlt.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion effsumlt ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) < ( exp ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 effsumlt.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 effsumlt.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 effsumlt.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
6 1 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
8 2 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
9 reeftcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
10 8 9 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
11 7 10 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
12 4 5 11 serfre ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) : ℕ0 ⟶ ℝ )
13 12 3 ffvelcdmd ⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
14 eqid ⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) )
15 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
16 3 15 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
18 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
19 rpexpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ+ )
20 2 18 19 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ+ )
21 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
23 22 nnrpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℝ+ )
24 20 23 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ+ )
25 7 24 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
26 8 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
27 1 efcllem ⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
28 26 27 syl ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
29 4 14 16 17 25 28 isumrpcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
30 13 29 ltaddrpd ⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) < ( ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
31 1 efval2 ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) )
32 26 31 syl ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) )
33 11 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
34 4 14 16 17 33 28 isumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
35 3 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
36 ax-1cn ⊢ 1 ∈ ℂ
37 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
38 35 36 37 sylancl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
39 38 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
40 39 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) )
41 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
42 3 4 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
43 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
44 43 33 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
45 41 42 44 fsumser ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) )
46 40 45 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) )
47 46 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = ( ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
48 32 34 47 3eqtrd ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
49 30 48 breqtrrd ⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) < ( exp ‘ 𝐴 ) )