Theorem efseq0ex 7253

Description: The series defining the exponential function converges.

Hypothesis

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

Assertion

Ref	Expression
efseq0ex	|- (A e. CC -> E.x( + seq0 F) ~~> x)

Distinct variable groups:   x,j,y,A   x,F

Proof of Theorem efseq0ex

Step	Hyp	Ref	Expression
1		ef0lem.1	. . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
2		reseq1 3352	. . . . . 6 |- (F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} -> (F |` NN) = ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN))
3	1, 2	ax-mp 7	. . . . 5 |- (F |` NN) = ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN)
4		nnssnn0 6049	. . . . . 6 |- NN (_ NN0
5		resopab2 3382	. . . . . 6 |- (NN (_ NN0 -> ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))})
6	4, 5	ax-mp 7	. . . . 5 |- ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
7	3, 6	eqtr 1487	. . . 4 |- (F |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
8	7	efseq1ex 7248	. . 3 |- (A e. CC -> E.w( + seq1 (F |` NN)) ~~> w)
9		addex 5289	. . . . . 6 |- + e. V
10		nn0ex 6052	. . . . . . 7 |- NN0 e. V
11	10, 1	fopabex2 3598	. . . . . 6 |- F e. V
12	9, 11	seq1res 6264	. . . . 5 |- ( + seq1 (F |` NN)) = ( + seq1 F)
13	12	breq1i 2616	. . . 4 |- (( + seq1 (F |` NN)) ~~> w <-> ( + seq1 F) ~~> w)
14	13	exbii 1047	. . 3 |- (E.w( + seq1 (F |` NN)) ~~> w <-> E.w( + seq1 F) ~~> w)
15	8, 14	sylib 198	. 2 |- (A e. CC -> E.w( + seq1 F) ~~> w)
16		oprex 3968	. . . . . . . 8 |- (<.1, + >. seq F) e. V
17		oprex 3968	. . . . . . . 8 |- (<.0, + >. seq F) e. V
18		visset 1804	. . . . . . . 8 |- w e. V
19		fvex 3717	. . . . . . . 8 |- (F` 0) e. V
20	16, 17, 18, 19	climaddc2 7055	. . . . . . 7 |- ((((<.1, + >. seq F) ~~> w /\ (F` 0) e. CC) /\ (1 e. ZZ /\ A.k e. (ZZ>` 1)(((<.1, + >. seq F)` k) e. CC /\ ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k))))) -> (<.0, + >. seq F) ~~> ((F` 0) + w))
21		pm3.27 323	. . . . . . . 8 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> (<.1, + >. seq F) ~~> w)
22		eftclt 7245	. . . . . . . . . . . 12 |- ((A e. CC /\ j e. NN0) -> ((A^j) / (!` j)) e. CC)
23	22	r19.21aiva 1706	. . . . . . . . . . 11 |- (A e. CC -> A.j e. NN0 ((A^j) / (!` j)) e. CC)
24	1	fopab2 3808	. . . . . . . . . . 11 |- (A.j e. NN0 ((A^j) / (!` j)) e. CC <-> F:NN0-->CC)
25	23, 24	sylib 198	. . . . . . . . . 10 |- (A e. CC -> F:NN0-->CC)
26		0nn0 6060	. . . . . . . . . . 11 |- 0 e. NN0
27		ffvelrn 3799	. . . . . . . . . . 11 |- ((F:NN0-->CC /\ 0 e. NN0) -> (F` 0) e. CC)
28	26, 27	mpan2 694	. . . . . . . . . 10 |- (F:NN0-->CC -> (F` 0) e. CC)
29	25, 28	syl 10	. . . . . . . . 9 |- (A e. CC -> (F` 0) e. CC)
30	29	adantr 389	. . . . . . . 8 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> (F` 0) e. CC)
31	21, 30	jca 288	. . . . . . 7 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> ((<.1, + >. seq F) ~~> w /\ (F` 0) e. CC))
32	11	serzclt 6983	. . . . . . . . . . . 12 |- ((k e. (ZZ>` 1) /\ A.m e. (1...k)(F` m) e. CC) -> ((<.1, + >. seq F)` k) e. CC)
33		pm3.27 323	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. (ZZ>` 1)) -> k e. (ZZ>` 1))
34		ffvelrn 3799	. . . . . . . . . . . . . . 15 |- ((F:NN0-->CC /\ m e. NN0) -> (F` m) e. CC)
35		elfznnt 6426	. . . . . . . . . . . . . . . 16 |- (m e. (1...k) -> m e. NN)
36		nnnn0t 6053	. . . . . . . . . . . . . . . 16 |- (m e. NN -> m e. NN0)
37	35, 36	syl 10	. . . . . . . . . . . . . . 15 |- (m e. (1...k) -> m e. NN0)
38	34, 25, 37	syl2an 454	. . . . . . . . . . . . . 14 |- ((A e. CC /\ m e. (1...k)) -> (F` m) e. CC)
39	38	r19.21aiva 1706	. . . . . . . . . . . . 13 |- (A e. CC -> A.m e. (1...k)(F` m) e. CC)
40	39	adantr 389	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. (ZZ>` 1)) -> A.m e. (1...k)(F` m) e. CC)
41	32, 33, 40	sylanc 471	. . . . . . . . . . 11 |- ((A e. CC /\ k e. (ZZ>` 1)) -> ((<.1, + >. seq F)` k) e. CC)
42	11	serz1p 6990	. . . . . . . . . . . . 13 |- ((k e. (ZZ>` 0) /\ 0 < k /\ A.m e. (0...k)(F` m) e. CC) -> ((<.0, + >. seq F)` k) = ((F` 0) + ((<.(0 + 1), + >. seq F)` k)))
43		nnnn0t 6053	. . . . . . . . . . . . . . 15 |- (k e. NN -> k e. NN0)
44		elnnuz 6372	. . . . . . . . . . . . . . 15 |- (k e. NN <-> k e. (ZZ>` 1))
45		elnn0uz 6373	. . . . . . . . . . . . . . 15 |- (k e. NN0 <-> k e. (ZZ>` 0))
46	43, 44, 45	3imtr3 218	. . . . . . . . . . . . . 14 |- (k e. (ZZ>` 1) -> k e. (ZZ>` 0))
47	46	adantl 388	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. (ZZ>` 1)) -> k e. (ZZ>` 0))
48		nngt0t 5894	. . . . . . . . . . . . . . 15 |- (k e. NN -> 0 < k)
49	44, 48	sylbir 201	. . . . . . . . . . . . . 14 |- (k e. (ZZ>` 1) -> 0 < k)
50	49	adantl 388	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. (ZZ>` 1)) -> 0 < k)
51		elfznn0t 6428	. . . . . . . . . . . . . . . 16 |- (m e. (0...k) -> m e. NN0)
52	34, 25, 51	syl2an 454	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ m e. (0...k)) -> (F` m) e. CC)
53	52	r19.21aiva 1706	. . . . . . . . . . . . . 14 |- (A e. CC -> A.m e. (0...k)(F` m) e. CC)
54	53	adantr 389	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. (ZZ>` 1)) -> A.m e. (0...k)(F` m) e. CC)
55	42, 47, 50, 54	syl3anc 856	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. (ZZ>` 1)) -> ((<.0, + >. seq F)` k) = ((F` 0) + ((<.(0 + 1), + >. seq F)` k)))
56		ax1cn 5241	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
57	56	addid2 5303	. . . . . . . . . . . . . . . 16 |- (0 + 1) = 1
58	57	opeq1i 2481	. . . . . . . . . . . . . . 15 |- <.(0 + 1), + >. = <.1, + >.
59	58	opreq1i 3956	. . . . . . . . . . . . . 14 |- (<.(0 + 1), + >. seq F) = (<.1, + >. seq F)
60	59	fveq1i 3710	. . . . . . . . . . . . 13 |- ((<.(0 + 1), + >. seq F)` k) = ((<.1, + >. seq F)` k)
61	60	opreq2i 3957	. . . . . . . . . . . 12 |- ((F` 0) + ((<.(0 + 1), + >. seq F)` k)) = ((F` 0) + ((<.1, + >. seq F)` k))
62	55, 61	syl6eq 1515	. . . . . . . . . . 11 |- ((A e. CC /\ k e. (ZZ>` 1)) -> ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k)))
63	41, 62	jca 288	. . . . . . . . . 10 |- ((A e. CC /\ k e. (ZZ>` 1)) -> (((<.1, + >. seq F)` k) e. CC /\ ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k))))
64	63	r19.21aiva 1706	. . . . . . . . 9 |- (A e. CC -> A.k e. (ZZ>` 1)(((<.1, + >. seq F)` k) e. CC /\ ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k))))
65	64	adantr 389	. . . . . . . 8 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> A.k e. (ZZ>` 1)(((<.1, + >. seq F)` k) e. CC /\ ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k))))
66		1z 6106	. . . . . . . 8 |- 1 e. ZZ
67	65, 66	jctil 292	. . . . . . 7 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> (1 e. ZZ /\ A.k e. (ZZ>` 1)(((<.1, + >. seq F)` k) e. CC /\ ((<.0, + >. seq F)` k) = ((F` 0) + (