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

Metamath Proof Explorer

Theorem ef0lem

Description: The series defining the exponential function converges in the (trivial) case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis eftval.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion ef0lem ( 𝐴 = 0 → seq 0 ( + , 𝐹 ) ⇝ 1 )

Proof

Step Hyp Ref Expression
1 eftval.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 simpr ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
3 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4 2 3 eleqtrrdi ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ) → 𝑘 ∈ ℕ0 )
5 elnn0 ⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
6 4 5 sylib ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ) → ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
7 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
8 7 adantl ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
9 1 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
10 8 9 syl ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
11 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑘 ) = ( 0 ↑ 𝑘 ) )
12 0exp ⊢ ( 𝑘 ∈ ℕ → ( 0 ↑ 𝑘 ) = 0 )
13 11 12 sylan9eq ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) = 0 )
14 13 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( 0 / ( ! ‘ 𝑘 ) ) )
15 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
16 nncn ⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
17 nnne0 ⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ 𝑘 ) ≠ 0 )
18 16 17 div0d ⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( 0 / ( ! ‘ 𝑘 ) ) = 0 )
19 8 15 18 3syl ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ( 0 / ( ! ‘ 𝑘 ) ) = 0 )
20 10 14 19 3eqtrd ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 0 )
21 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
22 velsn ⊢ ( 𝑘 ∈ { 0 } ↔ 𝑘 = 0 )
23 22 necon3bbii ⊢ ( ¬ 𝑘 ∈ { 0 } ↔ 𝑘 ≠ 0 )
24 21 23 sylibr ⊢ ( 𝑘 ∈ ℕ → ¬ 𝑘 ∈ { 0 } )
25 24 adantl ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ¬ 𝑘 ∈ { 0 } )
26 25 iffalsed ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → if ( 𝑘 ∈ { 0 } , 1 , 0 ) = 0 )
27 20 26 eqtr4d ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ { 0 } , 1 , 0 ) )
28 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
29 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 0 ) = ( 0 ↑ 0 ) )
30 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
31 29 30 eqtrdi ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 0 ) = 1 )
32 31 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = ( 1 / ( ! ‘ 0 ) ) )
33 0nn0 ⊢ 0 ∈ ℕ0
34 1 eftval ⊢ ( 0 ∈ ℕ0 → ( 𝐹 ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) )
35 33 34 ax-mp ⊢ ( 𝐹 ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) )
36 fac0 ⊢ ( ! ‘ 0 ) = 1
37 36 oveq2i ⊢ ( 1 / ( ! ‘ 0 ) ) = ( 1 / 1 )
38 1div1e1 ⊢ ( 1 / 1 ) = 1
39 37 38 eqtr2i ⊢ 1 = ( 1 / ( ! ‘ 0 ) )
40 32 35 39 3eqtr4g ⊢ ( 𝐴 = 0 → ( 𝐹 ‘ 0 ) = 1 )
41 28 40 sylan9eqr ⊢ ( ( 𝐴 = 0 ∧ 𝑘 = 0 ) → ( 𝐹 ‘ 𝑘 ) = 1 )
42 simpr ⊢ ( ( 𝐴 = 0 ∧ 𝑘 = 0 ) → 𝑘 = 0 )
43 42 22 sylibr ⊢ ( ( 𝐴 = 0 ∧ 𝑘 = 0 ) → 𝑘 ∈ { 0 } )
44 43 iftrued ⊢ ( ( 𝐴 = 0 ∧ 𝑘 = 0 ) → if ( 𝑘 ∈ { 0 } , 1 , 0 ) = 1 )
45 41 44 eqtr4d ⊢ ( ( 𝐴 = 0 ∧ 𝑘 = 0 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ { 0 } , 1 , 0 ) )
46 27 45 jaodan ⊢ ( ( 𝐴 = 0 ∧ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ { 0 } , 1 , 0 ) )
47 6 46 syldan ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ { 0 } , 1 , 0 ) )
48 33 3 eleqtri ⊢ 0 ∈ ( ℤ≥ ‘ 0 )
49 48 a1i ⊢ ( 𝐴 = 0 → 0 ∈ ( ℤ≥ ‘ 0 ) )
50 1cnd ⊢ ( ( 𝐴 = 0 ∧ 𝑘 ∈ { 0 } ) → 1 ∈ ℂ )
51 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
52 51 eqimss2i ⊢ { 0 } ⊆ ( 0 ... 0 )
53 52 a1i ⊢ ( 𝐴 = 0 → { 0 } ⊆ ( 0 ... 0 ) )
54 47 49 50 53 fsumcvg2 ⊢ ( 𝐴 = 0 → seq 0 ( + , 𝐹 ) ⇝ ( seq 0 ( + , 𝐹 ) ‘ 0 ) )
55 0z ⊢ 0 ∈ ℤ
56 55 40 seq1i ⊢ ( 𝐴 = 0 → ( seq 0 ( + , 𝐹 ) ‘ 0 ) = 1 )
57 54 56 breqtrd ⊢ ( 𝐴 = 0 → seq 0 ( + , 𝐹 ) ⇝ 1 )