Theorem ef0lem 7252

Description: The series defining the exponential function converges in the (trivial) case of a zero argument.

Hypothesis

Ref	Expression
ef0lem.1	|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}

Assertion

Ref	Expression
ef0lem	|- (A = 0 -> ( + seq0 F) ~~> 1)

Distinct variable group:   y,j,A

Proof of Theorem ef0lem

Step	Hyp	Ref	Expression
1		ef0lem.1	. . . . . . . . . . 11 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
2		oprex 3968	. . . . . . . . . . 11 |- ((A^(m + 1)) / (!` (m + 1))) e. V
3		opreq2 3954	. . . . . . . . . . . 12 |- (j = (m + 1) -> (A^j) = (A^(m + 1)))
4		fveq2 3709	. . . . . . . . . . . 12 |- (j = (m + 1) -> (!` j) = (!` (m + 1)))
5	3, 4	opreq12d 3963	. . . . . . . . . . 11 |- (j = (m + 1) -> ((A^j) / (!` j)) = ((A^(m + 1)) / (!` (m + 1))))
6	1, 2, 5	ser0p1 6499	. . . . . . . . . 10 |- (m e. NN0 -> (( + seq0 F)` (m + 1)) = ((( + seq0 F)` m) + ((A^(m + 1)) / (!` (m + 1)))))
7	6	ad2antrr 404	. . . . . . . . 9 |- (((m e. NN0 /\ A = 0) /\ (( + seq0 F)` m) = 1) -> (( + seq0 F)` (m + 1)) = ((( + seq0 F)` m) + ((A^(m + 1)) / (!` (m + 1)))))
8		opreq1 3953	. . . . . . . . . 10 |- ((( + seq0 F)` m) = 1 -> ((( + seq0 F)` m) + ((A^(m + 1)) / (!` (m + 1)))) = (1 + ((A^(m + 1)) / (!` (m + 1)))))
9		opreq1 3953	. . . . . . . . . . . . . . 15 |- (A = 0 -> (A^(m + 1)) = (0^(m + 1)))
10		nn0p1nnt 6122	. . . . . . . . . . . . . . . 16 |- (m e. NN0 -> (m + 1) e. NN)
11		0expt 6521	. . . . . . . . . . . . . . . 16 |- ((m + 1) e. NN -> (0^(m + 1)) = 0)
12	10, 11	syl 10	. . . . . . . . . . . . . . 15 |- (m e. NN0 -> (0^(m + 1)) = 0)
13	9, 12	sylan9eqr 1521	. . . . . . . . . . . . . 14 |- ((m e. NN0 /\ A = 0) -> (A^(m + 1)) = 0)
14	13	opreq1d 3960	. . . . . . . . . . . . 13 |- ((m e. NN0 /\ A = 0) -> ((A^(m + 1)) / (!` (m + 1))) = (0 / (!` (m + 1))))
15		div0t 5723	. . . . . . . . . . . . . . 15 |- (((!` (m + 1)) e. CC /\ (!` (m + 1)) =/= 0) -> (0 / (!` (m + 1))) = 0)
16		peano2nn0 6071	. . . . . . . . . . . . . . . 16 |- (m e. NN0 -> (m + 1) e. NN0)
17		facclt 6877	. . . . . . . . . . . . . . . . 17 |- ((m + 1) e. NN0 -> (!` (m + 1)) e. NN)
18		nncnt 5878	. . . . . . . . . . . . . . . . 17 |- ((!` (m + 1)) e. NN -> (!` (m + 1)) e. CC)
19	17, 18	syl 10	. . . . . . . . . . . . . . . 16 |- ((m + 1) e. NN0 -> (!` (m + 1)) e. CC)
20	16, 19	syl 10	. . . . . . . . . . . . . . 15 |- (m e. NN0 -> (!` (m + 1)) e. CC)
21		facne0t 6878	. . . . . . . . . . . . . . . 16 |- ((m + 1) e. NN0 -> (!` (m + 1)) =/= 0)
22	16, 21	syl 10	. . . . . . . . . . . . . . 15 |- (m e. NN0 -> (!` (m + 1)) =/= 0)
23	15, 20, 22	sylanc 471	. . . . . . . . . . . . . 14 |- (m e. NN0 -> (0 / (!` (m + 1))) = 0)
24	23	adantr 389	. . . . . . . . . . . . 13 |- ((m e. NN0 /\ A = 0) -> (0 / (!` (m + 1))) = 0)
25	14, 24	eqtrd 1499	. . . . . . . . . . . 12 |- ((m e. NN0 /\ A = 0) -> ((A^(m + 1)) / (!` (m + 1))) = 0)
26	25	opreq2d 3961	. . . . . . . . . . 11 |- ((m e. NN0 /\ A = 0) -> (1 + ((A^(m + 1)) / (!` (m + 1)))) = (1 + 0))
27		ax1cn 5241	. . . . . . . . . . . 12 |- 1 e. CC
28	27	addid1 5302	. . . . . . . . . . 11 |- (1 + 0) = 1
29	26, 28	syl6eq 1515	. . . . . . . . . 10 |- ((m e. NN0 /\ A = 0) -> (1 + ((A^(m + 1)) / (!` (m + 1)))) = 1)
30	8, 29	sylan9eqr 1521	. . . . . . . . 9 |- (((m e. NN0 /\ A = 0) /\ (( + seq0 F)` m) = 1) -> ((( + seq0 F)` m) + ((A^(m + 1)) / (!` (m + 1)))) = 1)
31	7, 30	eqtrd 1499	. . . . . . . 8 |- (((m e. NN0 /\ A = 0) /\ (( + seq0 F)` m) = 1) -> (( + seq0 F)` (m + 1)) = 1)
32	31	exp31 376	. . . . . . 7 |- (m e. NN0 -> (A = 0 -> ((( + seq0 F)` m) = 1 -> (( + seq0 F)` (m + 1)) = 1)))
33	32	a2d 13	. . . . . 6 |- (m e. NN0 -> ((A = 0 -> (( + seq0 F)` m) = 1) -> (A = 0 -> (( + seq0 F)` (m + 1)) = 1)))
34		addex 5289	. . . . . . . . 9 |- + e. V
35		nn0ex 6052	. . . . . . . . . 10 |- NN0 e. V
36	35, 1	fopabex2 3598	. . . . . . . . 9 |- F e. V
37	34, 36	seq00 6482	. . . . . . . 8 |- (( + seq0 F)` 0) = (F` 0)
38	37	a1i 8	. . . . . . 7 |- (A = 0 -> (( + seq0 F)` 0) = (F` 0))
39		0nn0 6060	. . . . . . . . 9 |- 0 e. NN0
40	39	a1i 8	. . . . . . . 8 |- (A = 0 -> 0 e. NN0)
41		opreq2 3954	. . . . . . . . . 10 |- (j = 0 -> (A^j) = (A^0))
42		fveq2 3709	. . . . . . . . . 10 |- (j = 0 -> (!` j) = (!` 0))
43	41, 42	opreq12d 3963	. . . . . . . . 9 |- (j = 0 -> ((A^j) / (!` j)) = ((A^0) / (!` 0)))
44		oprex 3968	. . . . . . . . 9 |- ((A^0) / (!` 0)) e. V
45	43, 1, 44	fvopab4 3765	. . . . . . . 8 |- (0 e. NN0 -> (F` 0) = ((A^0) / (!` 0)))
46	40, 45	syl 10	. . . . . . 7 |- (A = 0 -> (F` 0) = ((A^0) / (!` 0)))
47		opreq1 3953	. . . . . . . . . 10 |- (A = 0 -> (A^0) = (0^0))
48		0cn 5300	. . . . . . . . . . 11 |- 0 e. CC
49		exp0t 6503	. . . . . . . . . . 11 |- (0 e. CC -> (0^0) = 1)
50	48, 49	ax-mp 7	. . . . . . . . . 10 |- (0^0) = 1
51	47, 50	syl6eq 1515	. . . . . . . . 9 |- (A = 0 -> (A^0) = 1)
52	51	opreq1d 3960	. . . . . . . 8 |- (A = 0 -> ((A^0) / (!` 0)) = (1 / (!` 0)))
53		fac0 6871	. . . . . . . . . 10 |- (!` 0) = 1
54	53	opreq2i 3957	. . . . . . . . 9 |- (1 / (!` 0)) = (1 / 1)
55	27	div1 5728	. . . . . . . . 9 |- (1 / 1) = 1
56	54, 55	eqtr 1487	. . . . . . . 8 |- (1 / (!` 0)) = 1
57	52, 56	syl6eq 1515	. . . . . . 7 |- (A = 0 -> ((A^0) / (!` 0)) = 1)
58	38, 46, 57	3eqtrd 1503	. . . . . 6 |- (A = 0 -> (( + seq0 F)` 0) = 1)
59		fveq2 3709	. . . . . . . 8 |- (k = 0 -> (( + seq0 F)` k) = (( + seq0 F)` 0))
60	59	eqeq1d 1475	. . . . . . 7 |- (k = 0 -> ((( + seq0 F)` k) = 1 <-> (( + seq0 F)` 0) = 1))
61	60	imbi2d 610	. . . . . 6 |- (k = 0 -> ((A = 0 -> (( + seq0 F)` k) = 1) <-> (A = 0 -> (( + seq0 F)` 0) = 1)))
62		fveq2 3709	. . . . . . . 8 |- (k = m -> (( + seq0 F)` k) = (( + seq0 F)` m))
63	62	eqeq1d 1475	. . . . . . 7 |- (k = m -> ((( + seq0 F)` k) = 1 <-> (( + seq0 F)` m) = 1))
64	63	imbi2d 610	. . . . . 6 |- (k = m -> ((A = 0 -> (( + seq0 F)` k) = 1) <-> (A = 0 -> (( + seq0 F)` m) = 1)))
65		fveq2 3709	. . . . . . . 8 |- (k = (m + 1) -> (( + seq0 F)` k) = (( + seq0 F)` (m + 1)))
66	65	eqeq1d 1475	. . . . . . 7 |- (k = (m + 1) -> ((( + seq0 F)` k) = 1 <-> (( + seq0 F)` (m + 1)) = 1))
67	66	imbi2d 610	. . . . . 6 |- (k = (m + 1) -> ((A = 0 -> (( + seq0 F)` k) = 1) <-> (A = 0 -> (( + seq0 F)` (m + 1)) = 1)))
68	33, 58, 61, 64, 67, 64	nn0indALT 6161	. . . . 5 |- (m e. NN0 -> (A = 0 -> (( + seq0 F)` m) = 1))
69	68	impcom 351	. . . 4 |- ((A = 0 /\ m e. NN0) -> (( + seq0 F)` m) = 1)
70		elnn0uz 6373	. . . 4 |- (m e. NN0 <-> m e. (ZZ>` 0))
71	69, 70	sylan2br 453	. . 3 |- ((A = 0 /\ m e. (ZZ>` 0)) -> (( + seq0 F)` m) = 1)
72	71	r19.21aiva 1706	. 2 |- (A = 0 -> A.m e. (ZZ>` 0)(( + seq0 F)` m) = 1)
73		oprex 3968	. . . 4 |- ( + seq0 F) e. V
74		0z 6093	. . . 4 |- 0 e. ZZ
75	73, 74	climconst 7031	. . 3 |- ((1