MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cvgcmp Unicode version

Theorem cvgcmp 13630
Description: A comparison test for convergence of a real infinite series. Exercise 3 of [Gleason] p. 182. (Contributed by NM, 1-May-2005.) (Revised by Mario Carneiro, 24-Mar-2014.)
Hypotheses
Ref Expression
cvgcmp.1
cvgcmp.2
cvgcmp.3
cvgcmp.4
cvgcmp.5
cvgcmp.6
cvgcmp.7
Assertion
Ref Expression
cvgcmp
Distinct variable groups:   ,   ,   ,   ,M   ,N   ,

Proof of Theorem cvgcmp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgcmp.1 . 2
2 seqex 12109 . . 3
32a1i 11 . 2
4 cvgcmp.2 . . . . . . . 8
54, 1syl6eleq 2555 . . . . . . 7
6 eluzel2 11115 . . . . . . 7
75, 6syl 16 . . . . . 6
8 cvgcmp.5 . . . . . 6
91climcau 13493 . . . . . 6
107, 8, 9syl2anc 661 . . . . 5
11 cvgcmp.3 . . . . . . . . . . 11
121, 7, 11serfre 12136 . . . . . . . . . 10
1312ffvelrnda 6031 . . . . . . . . 9
1413recnd 9643 . . . . . . . 8
1514ralrimiva 2871 . . . . . . 7
161r19.29uz 13183 . . . . . . . 8
1716ex 434 . . . . . . 7
1815, 17syl 16 . . . . . 6
1918ralimdv 2867 . . . . 5
2010, 19mpd 15 . . . 4
211uztrn2 11127 . . . . . . . . . . 11
224, 21sylan 471 . . . . . . . . . 10
23 cvgcmp.4 . . . . . . . . . . . . 13
241, 7, 23serfre 12136 . . . . . . . . . . . 12
2524ffvelrnda 6031 . . . . . . . . . . 11
2625recnd 9643 . . . . . . . . . 10
2722, 26syldan 470 . . . . . . . . 9
2827ralrimiva 2871 . . . . . . . 8
2928adantr 465 . . . . . . 7
30 simpll 753 . . . . . . . . . . . . . . . 16
3130, 12syl 16 . . . . . . . . . . . . . . 15
3230, 4syl 16 . . . . . . . . . . . . . . . 16
33 simprl 756 . . . . . . . . . . . . . . . 16
341uztrn2 11127 . . . . . . . . . . . . . . . 16
3532, 33, 34syl2anc 661 . . . . . . . . . . . . . . 15
3631, 35ffvelrnd 6032 . . . . . . . . . . . . . 14
37 eqid 2457 . . . . . . . . . . . . . . . . . 18
3837uztrn2 11127 . . . . . . . . . . . . . . . . 17
3938adantl 466 . . . . . . . . . . . . . . . 16
4032, 39, 21syl2anc 661 . . . . . . . . . . . . . . 15
4130, 40, 13syl2anc 661 . . . . . . . . . . . . . 14
4230, 40, 25syl2anc 661 . . . . . . . . . . . . . . 15
4330, 24syl 16 . . . . . . . . . . . . . . . 16
4443, 35ffvelrnd 6032 . . . . . . . . . . . . . . 15
4542, 44resubcld 10012 . . . . . . . . . . . . . 14
4635, 1syl6eleq 2555 . . . . . . . . . . . . . . . . . 18
47 simprr 757 . . . . . . . . . . . . . . . . . 18
48 elfzuz 11713 . . . . . . . . . . . . . . . . . . . 20
4948, 1syl6eleqr 2556 . . . . . . . . . . . . . . . . . . 19
50 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . 23
51 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . 23
5250, 51oveq12d 6314 . . . . . . . . . . . . . . . . . . . . . 22
53 eqid 2457 . . . . . . . . . . . . . . . . . . . . . 22
54 ovex 6324 . . . . . . . . . . . . . . . . . . . . . 22
5552, 53, 54fvmpt 5956 . . . . . . . . . . . . . . . . . . . . 21
5655adantl 466 . . . . . . . . . . . . . . . . . . . 20
5711, 23resubcld 10012 . . . . . . . . . . . . . . . . . . . 20
5856, 57eqeltrd 2545 . . . . . . . . . . . . . . . . . . 19
5930, 49, 58syl2an 477 . . . . . . . . . . . . . . . . . 18
60 elfzuz 11713 . . . . . . . . . . . . . . . . . . 19
61 peano2uz 11163 . . . . . . . . . . . . . . . . . . . . . 22
6233, 61syl 16 . . . . . . . . . . . . . . . . . . . . 21
6337uztrn2 11127 . . . . . . . . . . . . . . . . . . . . 21
6462, 63sylan 471 . . . . . . . . . . . . . . . . . . . 20
65 cvgcmp.7 . . . . . . . . . . . . . . . . . . . . . . 23
661uztrn2 11127 . . . . . . . . . . . . . . . . . . . . . . . . 25
674, 66sylan 471 . . . . . . . . . . . . . . . . . . . . . . . 24
6811, 23subge0d 10167 . . . . . . . . . . . . . . . . . . . . . . . 24
6967, 68syldan 470 . . . . . . . . . . . . . . . . . . . . . . 23
7065, 69mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22
7167, 55syl 16 . . . . . . . . . . . . . . . . . . . . . 22
7270, 71breqtrrd 4478 . . . . . . . . . . . . . . . . . . . . 21
7330, 72sylan 471 . . . . . . . . . . . . . . . . . . . 20
7464, 73syldan 470 . . . . . . . . . . . . . . . . . . 19
7560, 74sylan2 474 . . . . . . . . . . . . . . . . . 18
7646, 47, 59, 75sermono 12139 . . . . . . . . . . . . . . . . 17
77 elfzuz 11713 . . . . . . . . . . . . . . . . . . . 20
7877, 1syl6eleqr 2556 . . . . . . . . . . . . . . . . . . 19
7911recnd 9643 . . . . . . . . . . . . . . . . . . 19
8030, 78, 79syl2an 477 . . . . . . . . . . . . . . . . . 18
8123recnd 9643 . . . . . . . . . . . . . . . . . . 19
8230, 78, 81syl2an 477 . . . . . . . . . . . . . . . . . 18
8330, 78, 56syl2an 477 . . . . . . . . . . . . . . . . . 18
8446, 80, 82, 83sersub 12150 . . . . . . . . . . . . . . . . 17
8540, 1syl6eleq 2555 . . . . . . . . . . . . . . . . . 18
8630, 49, 79syl2an 477 . . . . . . . . . . . . . . . . . 18
8730, 49, 81syl2an 477 . . . . . . . . . . . . . . . . . 18
8830, 49, 56syl2an 477 . . . . . . . . . . . . . . . . . 18
8985, 86, 87, 88sersub 12150 . . . . . . . . . . . . . . . . 17
9076, 84, 893brtr3d 4481 . . . . . . . . . . . . . . . 16
9141, 42resubcld 10012 . . . . . . . . . . . . . . . . 17
9236, 44, 91lesubaddd 10174 . . . . . . . . . . . . . . . 16
9390, 92mpbid 210 . . . . . . . . . . . . . . 15
9441recnd 9643 . . . . . . . . . . . . . . . 16
9542recnd 9643 . . . . . . . . . . . . . . . 16
9644recnd 9643 . . . . . . . . . . . . . . . 16
9794, 95, 96subsubd 9982 . . . . . . . . . . . . . . 15
9893, 97breqtrrd 4478 . . . . . . . . . . . . . 14
9936, 41, 45, 98lesubd 10181 . . . . . . . . . . . . 13
10041, 36resubcld 10012 . . . . . . . . . . . . . 14
101 rpre 11255 . . . . . . . . . . . . . . 15
102101ad2antlr 726 . . . . . . . . . . . . . 14
103 lelttr 9696 . . . . . . . . . . . . . 14
10445, 100, 102, 103syl3anc 1228 . . . . . . . . . . . . 13
10599, 104mpand 675 . . . . . . . . . . . 12
10630, 49, 11syl2an 477 . . . . . . . . . . . . . . 15
10760, 64sylan2 474 . . . . . . . . . . . . . . . 16
108 0red 9618 . . . . . . . . . . . . . . . . . 18
10967, 23syldan 470 . . . . . . . . . . . . . . . . . 18
11067, 11syldan 470 . . . . . . . . . . . . . . . . . 18
111 cvgcmp.6 . . . . . . . . . . . . . . . . . 18
112108, 109, 110, 111, 65letrd 9760 . . . . . . . . . . . . . . . . 17
11330, 112sylan 471 . . . . . . . . . . . . . . . 16
114107, 113syldan 470 . . . . . . . . . . . . . . 15
11546, 47, 106, 114sermono 12139 . . . . . . . . . . . . . 14
11636, 41, 115abssubge0d 13263 . . . . . . . . . . . . 13
117116breq1d 4462 . . . . . . . . . . . 12
11830, 49, 23syl2an 477 . . . . . . . . . . . . . . 15
11930, 111sylan 471 . . . . . . . . . . . . . . . . 17
12064, 119syldan 470 . . . . . . . . . . . . . . . 16
12160, 120sylan2 474 . . . . . . . . . . . . . . 15
12246, 47, 118, 121sermono 12139 . . . . . . . . . . . . . 14
12344, 42, 122abssubge0d 13263 . . . . . . . . . . . . 13
124123breq1d 4462 . . . . . . . . . . . 12
125105, 117, 1243imtr4d 268 . . . . . . . . . . 11
126125anassrs 648 . . . . . . . . . 10
127126adantld 467 . . . . . . . . 9
128127ralimdva 2865 . . . . . . . 8
129128reximdva 2932 . . . . . . 7
13037r19.29uz 13183 . . . . . . 7
13129, 129, 130syl6an 545 . . . . . 6
132131ralimdva 2865 . . . . 5
1331, 37cau4 13189 . . . . . 6
1344, 133syl 16 . . . . 5
1351, 37cau4 13189 . . . . . 6
1364, 135syl 16 . . . . 5
137132, 134, 1363imtr4d 268 . . . 4
13820, 137mpd 15 . . 3
1391uztrn2 11127 . . . . . . . 8
140 simpr 461 . . . . . . . . 9
14125biantrurd 508 . . . . . . . . 9