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	syl6eq	⊢ ( 𝐴 = 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 )