HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ser1f0 7106
Description: If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 1/2 megabyte in size.
Hypotheses
Ref Expression
ser1f0.1 |- F:NN-->CC
ser1f0.2 |- A e. CC
ser1f0.3 |- ( + seq1 F) ~~> A
Assertion
Ref Expression
ser1f0 |- F ~~> 0
Proof of Theorem ser1f0
StepHypRef Expression
1 0cn 5300 . . 3 |- 0 e. CC
2 inss2 2221 . . . . . . 7 |- (ZZ i^i (ZZ>` 2)) (_ (ZZ>` 2)
3 1z 6106 . . . . . . . . . . 11 |- 1 e. ZZ
43eluz1 6354 . . . . . . . . . 10 |- (2 e. (ZZ>` 1) <-> (2 e. ZZ /\ 1 <_ 2))
5 2z 6107 . . . . . . . . . 10 |- 2 e. ZZ
6 1re 5407 . . . . . . . . . . 11 |- 1 e. RR
7 2re 5926 . . . . . . . . . . 11 |- 2 e. RR
8 1lt2 5975 . . . . . . . . . . 11 |- 1 < 2
96, 7, 8ltlei 5554 . . . . . . . . . 10 |- 1 <_ 2
104, 5, 9mpbir2an 728 . . . . . . . . 9 |- 2 e. (ZZ>` 1)
11 uzss 6363 . . . . . . . . 9 |- (2 e. (ZZ>` 1) -> (ZZ>` 2) (_ (ZZ>` 1))
1210, 11ax-mp 7 . . . . . . . 8 |- (ZZ>` 2) (_ (ZZ>` 1)
13 nnuz 6371 . . . . . . . 8 |- NN = (ZZ>` 1)
1412, 13sseqtr4 2084 . . . . . . 7 |- (ZZ>` 2) (_ NN
152, 14sstri 2063 . . . . . 6 |- (ZZ i^i (ZZ>` 2)) (_ NN
1615sseli 2055 . . . . 5 |- (k e. (ZZ i^i (ZZ>` 2)) -> k e. NN)
17 ser1f0.1 . . . . . 6 |- F:NN-->CC
1817ffvelrni 3800 . . . . 5 |- (k e. NN -> (F` k) e. CC)
1916, 18syl 10 . . . 4 |- (k e. (ZZ i^i (ZZ>` 2)) -> (F` k) e. CC)
2019rgen 1690 . . 3 |- A.k e. (ZZ i^i (ZZ>` 2))(F` k) e. CC
21 uzssz 6362 . . . 4 |- (ZZ>` 2) (_ ZZ
22 ssid 2070 . . . 4 |- ZZ (_ ZZ
23 ssid 2070 . . . 4 |- (ZZ>` 2) (_ (ZZ>` 2)
24 nnex 5881 . . . . 5 |- NN e. V
25 fex 3637 . . . . 5 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
2617, 24, 25mp2an 695 . . . 4 |- F e. V
275, 21, 22, 5, 23, 21, 26clm4 7018 . . 3 |- ((0 e. CC /\ A.k e. (ZZ i^i (ZZ>` 2))(F` k) e. CC) -> (F ~~> 0 <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x))))
281, 20, 27mp2an 695 . 2 |- (F ~~> 0 <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x)))
29 ser1f0.2 . . . . . 6 |- A e. CC
30 ser1f0.3 . . . . . 6 |- ( + seq1 F) ~~> A
31 0z 6093 . . . . . . 7 |- 0 e. ZZ
32 uzssz 6362 . . . . . . 7 |- (ZZ>` 0) (_ ZZ
3331, 32, 22clmi2 7025 . . . . . 6 |- (((A e. CC /\ ( + seq1 F) ~~> A) /\ ((x / 2) e. RR /\ 0 < (x / 2))) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))
3429, 30, 33mpanl12 706 . . . . 5 |- (((x / 2) e. RR /\ 0 < (x / 2)) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))
35 rehalfclt 5981 . . . . . 6 |- (x e. RR -> (x / 2) e. RR)
3635adantr 389 . . . . 5 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
37 halfpos2t 5984 . . . . . 6 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
3837biimpa 416 . . . . 5 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
3934, 36, 38sylanc 471 . . . 4 |- ((x e. RR /\ 0 < x) -> E.m e. ZZ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))
40 breq1 2612 . . . . . . . . . . 11 |- (j = (m + 1) -> (j <_ k <-> (m + 1) <_ k))
4140imbi1d 611 . . . . . . . . . 10 |- (j = (m + 1) -> ((j <_ k -> (abs` ((F` k) - 0)) < x) <-> ((m + 1) <_ k -> (abs` ((F` k) - 0)) < x)))
4241ralbidv 1655 . . . . . . . . 9 |- (j = (m + 1) -> (A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x) <-> A.k e. (ZZ>` 2)((m + 1) <_ k -> (abs` ((F` k) - 0)) < x)))
4342rcla4ev 1868 . . . . . . . 8 |- (((m + 1) e. ZZ /\ A.k e. (ZZ>` 2)((m + 1) <_ k -> (abs` ((F` k) - 0)) < x)) -> E.j e. ZZ A.k e. (ZZ>` 2)(j <_ k -> (abs` ((F` k) - 0)) < x))
44 peano2z 6113 . . . . . . . . 9 |- (m e. ZZ -> (m + 1) e. ZZ)
4544ad2antrl 406 . . . . . . . 8 |- ((x e. RR /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> (m + 1) e. ZZ)
46 p1let 5773 . . . . . . . . . . . . . . . . . . 19 |- ((m e. RR /\ k e. RR /\ (m + 1) <_ k) -> m <_ k)
47463expia 833 . . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ k e. RR) -> ((m + 1) <_ k -> m <_ k))
48 zret 6086 . . . . . . . . . . . . . . . . . 18 |- (m e. ZZ -> m e. RR)
49 zret 6086 . . . . . . . . . . . . . . . . . 18 |- (k e. ZZ -> k e. RR)
5047, 48, 49syl2an 454 . . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ k e. ZZ) -> ((m + 1) <_ k -> m <_ k))
5150ancoms 436 . . . . . . . . . . . . . . . 16 |- ((k e. ZZ /\ m e. ZZ) -> ((m + 1) <_ k -> m <_ k))
5251adantrr 395 . . . . . . . . . . . . . . 15 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ k -> m <_ k))
53 breq2 2613 . . . . . . . . . . . . . . . . . 18 |- (n = k -> (m <_ n <-> m <_ k))
54 fveq2 3709 . . . . . . . . . . . . . . . . . . . . 21 |- (n = k -> (( + seq1 F)` n) = (( + seq1 F)` k))
5554opreq1d 3960 . . . . . . . . . . . . . . . . . . . 20 |- (n = k -> ((( + seq1 F)` n) - A) = ((( + seq1 F)` k) - A))
5655fveq2d 3713 . . . . . . . . . . . . . . . . . . 19 |- (n = k -> (abs` ((( + seq1 F)` n) - A)) = (abs` ((( + seq1 F)` k) - A)))
5756breq1d 2619 . . . . . . . . . . . . . . . . . 18 |- (n = k -> ((abs` ((( + seq1 F)` n) - A)) < (x / 2) <-> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
5853, 57imbi12d 624 . . . . . . . . . . . . . . . . 17 |- (n = k -> ((m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)) <-> (m <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2))))
5958rcla4va 1866 . . . . . . . . . . . . . . . 16 |- ((k e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2))) -> (m <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
6059adantrl 394 . . . . . . . . . . . . . . 15 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> (m <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
6152, 60syld 27 . . . . . . . . . . . . . 14 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ k -> (abs` ((( + seq1 F)` k) - A)) < (x / 2)))
62 leaddsubt 5607 . . . . . . . . . . . . . . . . . . 19 |- ((m e. RR /\ 1 e. RR /\ k e. RR) -> ((m + 1) <_ k <-> m <_ (k - 1)))
636, 62mp3an2 901 . . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ k e. RR) -> ((m + 1) <_ k <-> m <_ (k - 1)))
6463, 48, 49syl2an 454 . . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ k e. ZZ) -> ((m + 1) <_ k <-> m <_ (k - 1)))
6564ancoms 436 . . . . . . . . . . . . . . . 16 |- ((k e. ZZ /\ m e. ZZ) -> ((m + 1) <_ k <-> m <_ (k - 1)))
6665adantrr 395 . . . . . . . . . . . . . . 15 |- ((k e. ZZ /\ (m e. ZZ /\ A.n e. ZZ (m <_ n -> (abs` ((( + seq1 F)` n) - A)) < (x / 2)))) -> ((m + 1) <_ k <-> m <_ (k - 1)))
67 peano2zm 6116 . . . . . . . . . . . . . . . . . 18 |- (k e. ZZ -> (k - 1) e. ZZ)
68 breq2 2613 . . . . . . . . . . . . . . . . . . . 20 |- (n = (k - 1) -> (m <_ n <-> m <_ (k - 1)))
69 fveq2 3709 . . . . . . . . . . . . . . . . . . . . . . 23 |- (n = (k - 1) -> (( + seq1 F)` n) = (( + seq1 F)` (k - 1)))
7069opreq1d 3960 . . . . . . . . . . . . . . . . . . . . . 22 |- (n = (k - 1) -> ((( + seq1 F)` n) - A) = ((( + seq1 F)` (k - 1)