HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem efseq0ex 7434
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
StepHypRef Expression
1 ef0lem.1 . . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
2 reseq1 3428 . . . . . 6 |- (F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} -> (F |` NN) = ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN))
31, 2ax-mp 7 . . . . 5 |- (F |` NN) = ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN)
4 nnssnn0 6212 . . . . . 6 |- NN (_ NN0
5 resopab2 3459 . . . . . 6 |- (NN (_ NN0 -> ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))})
64, 5ax-mp 7 . . . . 5 |- ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
73, 6eqtri 1532 . . . 4 |- (F |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
87efseq1ex 7429 . . 3 |- (A e. CC -> E.w( + seq1 (F |` NN)) ~~> w)
9 addex 5406 . . . . . 6 |- + e. V
10 nn0ex 6215 . . . . . . 7 |- NN0 e. V
1110, 1fopabex2 3687 . . . . . 6 |- F e. V
129, 11seq1res 6620 . . . . 5 |- ( + seq1 (F |` NN)) = ( + seq1 F)
1312breq1i 2676 . . . 4 |- (( + seq1 (F |` NN)) ~~> w <-> ( + seq1 F) ~~> w)
1413exbii 1083 . . 3 |- (E.w( + seq1 (F |` NN)) ~~> w <-> E.w( + seq1 F) ~~> w)
158, 14sylib 196 . 2 |- (A e. CC -> E.w( + seq1 F) ~~> w)
16 oprex 4059 . . . . . . . 8 |- (<.1, + >. seq F) e. V
17 oprex 4059 . . . . . . . 8 |- (<.0, + >. seq F) e. V
18 visset 1851 . . . . . . . 8 |- w e. V
19 fvex 3808 . . . . . . . 8 |- (F` 0) e. V
2016, 17, 18, 19climaddc2 7242 . . . . . . 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 321 . . . . . . . 8 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> (<.1, + >. seq F) ~~> w)
22 eftcl 7426 . . . . . . . . . . . 12 |- ((A e. CC /\ j e. NN0) -> ((A^j) / (!` j)) e. CC)
2322r19.21aiva 1752 . . . . . . . . . . 11 |- (A e. CC -> A.j e. NN0 ((A^j) / (!` j)) e. CC)
241fopab2 3899 . . . . . . . . . . 11 |- (A.j e. NN0 ((A^j) / (!` j)) e. CC <-> F:NN0-->CC)
2523, 24sylib 196 . . . . . . . . . 10 |- (A e. CC -> F:NN0-->CC)
26 0nn0 6223 . . . . . . . . . . 11 |- 0 e. NN0
27 ffvelrn 3890 . . . . . . . . . . 11 |- ((F:NN0-->CC /\ 0 e. NN0) -> (F` 0) e. CC)
2826, 27mpan2 699 . . . . . . . . . 10 |- (F:NN0-->CC -> (F` 0) e. CC)
2925, 28syl 10 . . . . . . . . 9 |- (A e. CC -> (F` 0) e. CC)
3029adantr 389 . . . . . . . 8 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> (F` 0) e. CC)
3121, 30jca 286 . . . . . . 7 |- ((A e. CC /\ (<.1, + >. seq F) ~~> w) -> ((<.1, + >. seq F) ~~> w /\ (F` 0) e. CC))
3211serzcl 7168 . . . . . . . . . . . 12 |- ((k e. (ZZ>` 1) /\ A.m e. (1...k)(F` m) e. CC) -> ((<.1, + >. seq F)` k) e. CC)
33 pm3.27 321 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. (ZZ>` 1)) -> k e. (ZZ>` 1))
34 ffvelrn 3890 . . . . . . . . . . . . . . 15 |- ((F:NN0-->CC /\ m e. NN0) -> (F` m) e. CC)
35 elfznn 6554 . . . . . . . . . . . . . . . 16 |- (m e. (1...k) -> m e. NN)
36 nnnn0 6216 . . . . . . . . . . . . . . . 16 |- (m e. NN -> m e. NN0)
3735, 36syl 10 . . . . . . . . . . . . . . 15 |- (m e. (1...k) -> m e. NN0)
3834, 25, 37syl2an 456 . . . . . . . . . . . . . 14 |- ((A e. CC /\ m e. (1...k)) -> (F` m) e. CC)
3938r19.21aiva 1752 . . . . . . . . . . . . 13 |- (A e. CC -> A.m e. (1...k)(F` m) e. CC)
4039adantr 389 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. (ZZ>` 1)) -> A.m e. (1...k)(F` m) e. CC)
4132, 33, 40sylanc 473 . . . . . . . . . . 11 |- ((A e. CC /\ k e. (ZZ>` 1)) -> ((<.1, + >. seq F)` k) e. CC)
4211serz1p 7175 . . . . . . . . . . . . 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 nnnn0 6216 . . . . . . . . . . . . . . 15 |- (k e. NN -> k e. NN0)
44 elnnuz 6500 . . . . . . . . . . . . . . 15 |- (k e. NN <-> k e. (ZZ>` 1))
45 elnn0uz 6501 . . . . . . . . . . . . . . 15 |- (k e. NN0 <-> k e. (ZZ>` 0))
4643, 44, 453imtr3i 216 . . . . . . . . . . . . . 14 |- (k e. (ZZ>` 1) -> k e. (ZZ>` 0))
4746adantl 388 . . . . . . . . . . . . 13 |- ((A e. CC /\ k e. (ZZ>` 1)) -> k e. (ZZ>` 0))
48 nngt0 6033 . . . . . . . . . . . . . . 15 |- (k e. NN -> 0 < k)
4944, 48sylbir 199 . . . . . . . . . . . . . 14 |- (k e. (ZZ>` 1) -> 0 < k)
5049adantl 388 . . . . . . . . . . . . 13 |- ((A e. CC /\ k e. (ZZ>` 1)) -> 0 < k)
51 elfznn0 6556 . . . . . . . . . . . . . . . 16 |- (m e. (0...k) -> m e. NN0)
5234, 25, 51syl2an 456 . . . . . . . . . . . . . . 15 |- ((A e. CC /\ m e. (0...k)) -> (F` m) e. CC)
5352r19.21aiva 1752 . . . . . . . . . . . . . 14 |- (A e. CC -> A.m e. (0...k)(F` m) e. CC)
5453adantr 389 . . . . . . . . . . . . 13 |- ((A e. CC /\ k e. (ZZ>` 1)) -> A.m e. (0...k)(F` m) e. CC)
5542, 47, 50, 54syl3anc 861 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. (ZZ>` 1)) -> ((<.0, + >. seq F)` k) = ((F` 0) + ((<.(0 + 1), + >. seq F)` k)))
56 ax1cn 5358 . . . . . . . . . . . . . . . . 17 |- 1 e. CC
5756addid2i 5420 . . . . . . . . . . . . . . . 16 |- (0 + 1) = 1
5857opeq1i 2538 . . . . . . . . . . . . . . 15 |- <.(0 + 1), + >. = <.1, + >.
5958opreq1i 4047 . . . . . . . . . . . . . 14 |- (<.(0 + 1), + >. seq F) = (<.1, + >. seq F)
6059fveq1i 3801 . . . . . . . . . . . . 13 |- ((<.(0 + 1), + >. seq F)` k) = ((<.1, + >. seq F)` k)
6160opreq2i 4048 . . . . . . . . . . . 12 |- ((F` 0) + ((<.(0 + 1), + >. seq F)` k)) = ((F` 0) + ((<.1, + >. seq F)` k))
6255, 61syl6eq 1560 . . . . . . . . . . 11 |- ((A e. CC /\ k e. (ZZ>` 1)) -> ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k)))
6341, 62jca 286 . . . . . . . . . 10 |- ((A e. CC /\ k e. (ZZ>` 1)) -> (((<.1, + >. seq F)` k) e. CC /\ ((<.0, + >. seq F)` k) = ((F` 0) + ((<.1, + >. seq F)` k))))
6463r19.21aiva 1752 . . . . . . . . 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))))
6564adantr 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 6269 . . . . . . . 8 |- 1 e. ZZ
6765, 66jctil 290 . . . . . . 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) +