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 )