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

Theorem cantnflt 8112
Description: An upper bound on the partial sums of the function. Since each term dominates all previous terms, by induction we can bound the whole sum with any exponent where is larger than any exponent ( `x),xe. which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 29-Jun-2019.)
Hypotheses
Ref Expression
cantnfs.s
cantnfs.a
cantnfs.b
cantnfcl.g
cantnfcl.f
cantnfval.h
cantnflt.a
cantnflt.k
cantnflt.c
cantnflt.s
Assertion
Ref Expression
cantnflt
Distinct variable groups:   , ,   ,   , ,   , ,   S, ,   , ,   , ,   , ,

Proof of Theorem cantnflt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.a . . . 4
2 cantnflt.c . . . 4
3 cantnflt.a . . . 4
4 oen0 7254 . . . 4
51, 2, 3, 4syl21anc 1227 . . 3
6 fveq2 5871 . . . . 5
7 0ex 4582 . . . . . 6
8 cantnfval.h . . . . . . 7
98seqom0g 7140 . . . . . 6
107, 9ax-mp 5 . . . . 5
116, 10syl6eq 2514 . . . 4
1211eleq1d 2526 . . 3
135, 12syl5ibrcom 222 . 2
142adantr 465 . . . . . . 7
15 eloni 4893 . . . . . . 7
1614, 15syl 16 . . . . . 6
17 cantnflt.s . . . . . . . 8
1817adantr 465 . . . . . . 7
19 cantnfcl.g . . . . . . . . . 10
2019oif 7976 . . . . . . . . 9
21 ffn 5736 . . . . . . . . 9
2220, 21mp1i 12 . . . . . . . 8
23 cantnflt.k . . . . . . . . . 10
2419oicl 7975 . . . . . . . . . . . . 13
25 ordsuc 6649 . . . . . . . . . . . . 13
2624, 25mpbi 208 . . . . . . . . . . . 12
27 ordelon 4907 . . . . . . . . . . . 12
2826, 23, 27sylancr 663 . . . . . . . . . . 11
29 ordsssuc 4969 . . . . . . . . . . 11
3028, 24, 29sylancl 662 . . . . . . . . . 10
3123, 30mpbird 232 . . . . . . . . 9
3231adantr 465 . . . . . . . 8
33 vex 3112 . . . . . . . . . 10
3433sucid 4962 . . . . . . . . 9
35 simprr 757 . . . . . . . . 9
3634, 35syl5eleqr 2552 . . . . . . . 8
37 fnfvima 6150 . . . . . . . 8
3822, 32, 36, 37syl3anc 1228 . . . . . . 7
3918, 38sseldd 3504 . . . . . 6
40 ordsucss 6653 . . . . . 6
4116, 39, 40sylc 60 . . . . 5
42 suppssdm 6931 . . . . . . . . . . 11
43 cantnfcl.f . . . . . . . . . . . . . 14
44 cantnfs.s . . . . . . . . . . . . . . 15
45 cantnfs.b . . . . . . . . . . . . . . 15
4644, 1, 45cantnfs 8106 . . . . . . . . . . . . . 14
4743, 46mpbid 210 . . . . . . . . . . . . 13
4847simpld 459 . . . . . . . . . . . 12
49 fdm 5740 . . . . . . . . . . . 12
5048, 49syl 16 . . . . . . . . . . 11
5142, 50syl5sseq 3551 . . . . . . . . . 10
52 onss 6626 . . . . . . . . . . 11
5345, 52syl 16 . . . . . . . . . 10
5451, 53sstrd 3513 . . . . . . . . 9
5554adantr 465 . . . . . . . 8
5623adantr 465 . . . . . . . . . . 11
5735, 56eqeltrrd 2546 . . . . . . . . . 10
58 ordsucelsuc 6657 . . . . . . . . . . 11
5924, 58ax-mp 5 . . . . . . . . . 10
6057, 59sylibr 212 . . . . . . . . 9
6120ffvelrni 6030 . . . . . . . . 9
6260, 61syl 16 . . . . . . . 8
6355, 62sseldd 3504 . . . . . . 7
64 suceloni 6648 . . . . . . 7
6563, 64syl 16 . . . . . 6
661adantr 465 . . . . . 6
673adantr 465 . . . . . 6
68 oewordi 7259 . . . . . 6
6965, 14, 66, 67, 68syl31anc 1231 . . . . 5
7041, 69mpd 15 . . . 4
7135fveq2d 5875 . . . . 5
72 simprl 756 . . . . . 6
73 simpl 457 . . . . . 6
74 eleq1 2529 . . . . . . . 8
75 suceq 4948 . . . . . . . . . 10
7675fveq2d 5875 . . . . . . . . 9
77 fveq2 5871 . . . . . . . . . . 11
78 suceq 4948 . . . . . . . . . . 11
7977, 78syl 16 . . . . . . . . . 10
8079oveq2d 6312 . . . . . . . . 9
8176, 80eleq12d 2539 . . . . . . . 8
8274, 81imbi12d 320 . . . . . . 7
83 eleq1 2529 . . . . . . . 8
84 suceq 4948 . . . . . . . . . 10
8584fveq2d 5875 . . . . . . . . 9
86 fveq2 5871 . . . . . . . . . . 11
87 suceq 4948 . . . . . . . . . . 11
8886, 87syl 16 . . . . . . . . . 10
8988oveq2d 6312 . . . . . . . . 9
9085, 89eleq12d 2539 . . . . . . . 8
9183, 90imbi12d 320 . . . . . . 7
92 eleq1 2529 . . . . . . . 8
93 suceq 4948 . . . . . . . . . 10
9493fveq2d 5875 . . . . . . . . 9
95 fveq2 5871 . . . . . . . . . . 11
96 suceq 4948 . . . . . . . . . . 11
9795, 96syl 16 . . . . . . . . . 10
9897oveq2d 6312 . . . . . . . . 9
9994, 98eleq12d 2539 . . . . . . . 8
10092, 99imbi12d 320 . . . . . . 7
10148adantr 465 . . . . . . . . . . 11
10220ffvelrni 6030 . . . . . . . . . . . 12
10351sselda 3503 . . . . . . . . . . . 12
104102, 103sylan2 474 . . . . . . . . . . 11
105101, 104ffvelrnd 6032 . . . . . . . . . 10
1061adantr 465 . . . . . . . . . . . 12
107 onelon 4908 . . . . . . . . . . . 12
108106, 105, 107syl2anc 661 . . . . . . . . . . 11
10954sselda 3503 . . . . . . . . . . . . 13
110102, 109sylan2 474 . . . . . . . . . . . 12
111 oecl 7206 . . . . . . . . . . . 12
112106, 110, 111syl2anc 661 . . . . . . . . . . 11
1133adantr 465 . . . . . . . . . . . 12
114 oen0 7254 . . . . . . . . . . . 12
115106, 110, 113, 114syl21anc 1227 . . . . . . . . . . 11
116 omord2 7235 . . . . . . . . . . 11
117108, 106, 112, 115, 116syl31anc 1231 . . . . . . . . . 10
118105, 117mpbid 210 . . . . . . . . 9
119 peano1 6719 . . . . . . . . . . . 12
120119a1i 11 . . . . . . . . . . 11
12144, 1, 45, 19, 43, 8cantnfsuc 8110 . . . . . . . . . . 11
122120, 121sylan2 474 . . . . . . . . . 10
12310oveq2i 6307 . . . . . . . . . . 11
124 omcl 7205 . . . . . . . . . . . . 13
125112, 108, 124syl2anc 661 . . . . . . . . . . . 12
126 oa0 7185 . . . . . . . . . . . 12
127125, 126syl 16 . . . . . . . . . . 11
128123, 127syl5eq 2510 . . . . . . . . . 10
129122, 128eqtrd 2498 . . . . . . . . 9
130 oesuc 7196 . . . . . . . . . 10
131106, 110, 130syl2anc 661 . . . . . . . . 9
132118, 129, 1313eltr4d 2560 . . . . . . . 8
133132ex 434 . . . . . . 7
134 ordtr 4897 . . . . . . . . . . . 12
13524, 134ax-mp 5 . . . . . . . . . . 11
136 trsuc 4967 . . . . . . . . . . 11
137135, 136mpan 670 . . . . . . . . . 10
138137imim1i 58 . . . . . . . . 9
1391ad2antrr 725 . . . . . . . . . . . . . . . 16
140 eloni 4893 . . . . . . . . . . . . . . . 16
141139, 140syl 16 . . . . . . . . . . . . . . 15
14248ad2antrr 725 . . . . . . . . . . . . . . . 16
14351ad2antrr 725 . . . . . . . . . . . . . . . . 17
14420ffvelrni 6030 . . . . . . . . . . . . . . . . . 18
145144ad2antrl 727 . . . . . . . . . . . . . . . . 17
146143, 145sseldd 3504 . . . . . . . . . . . . . . . 16
147142, 146ffvelrnd 6032 . . . . . . . . . . . . . . 15
148 ordsucss 6653 . . . . . . . . . . . . . . 15
149141, 147, 148sylc 60 . . . . . . . . . . . . . 14
150 onelon 4908 . . . . . . . . . . . . . . . . 17
151139, 147, 150syl2anc 661 . . . . . . . . . . . . . . . 16
152 suceloni 6648 . . . . . . . . . . . . . . . 16
153151, 152syl 16 . . . . . . . . . . . . . . 15
15454ad2antrr 725 . . . . . . . . . . . . . . . . 17
155154, 145sseldd 3504 . . . . . . . . . . . . . . . 16
156 oecl 7206 . . . . . . . . . . . . . . . 16
157139, 155, 156syl2anc 661 . . . . . . . . . . . . . . 15
158 omwordi 7239 . . . . . . . . . . . . . . 15
159153, 139, 157, 158syl3anc 1228 . . . . . . . . . . . . . 14
160149, 159mpd 15 . . . . . . . . . . . . 13
161 oesuc 7196 . . . . . . . . . . . . . 14
162139, 155, 161syl2anc 661 . . . . . . . . . . . . 13
163160, 162sseqtr4d 3540 . . . . . . . . . . . 12
164 eloni 4893 . . . . . . . . . . . . . . . . . 18
165155, 164syl 16 . . . . . . . . . . . . . . . . 17
166 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
167166sucid 4962 . . . . . . . . . . . . . . . . . . . 20
168166sucex 6646 . . . . . . . . . . . . . . . . . . . . 21
169168epelc 4798 . . . . . . . . . . . . . . . . . . . 20
170167, 169mpbir 209 . . . . . . . . . . . . . . . . . . 19
17145, 51ssexd 4599 . . . . . . . . . . . . . . . . . . . . . 22
17244, 1, 45, 19, 43cantnfcl 8107 . . . . . . . . . . . . . . . . . . . . . . 23
173172simpld 459 . . . . . . . . . . . . . . . . . . . . . 22
17419oiiso 7983 . . . . . . . . . . . . . . . . . . . . . 22
175171, 173, 174syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
176175ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
177137ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20
178 simprl 756 . . . . . . . . . . . . . . . . . . . 20
179 isorel 6222 . . . . . . . . . . . . . . . . . . . 20
180176, 177, 178, 179syl12anc 1226 . . . . . . . . . . . . . . . . . . 19
181170, 180mpbii 211 . . . . . . . . . . . . . . . . . 18
182 fvex 5881 . . . . . . . . . . . . . . . . . . 19
183182epelc 4798 . . . . . . . . . . . . . . . . . 18
184181, 183sylib 196 . . . . . . . . . . . . . . . . 17
185 ordsucss 6653 . . . . . . . . . . . . . . . . 17
186165, 184, 185sylc 60 . . . . . . . . . . . . . . . 16
18720ffvelrni 6030 . . . . . . . . . . . . . . . . . . . 20
188177, 187syl 16 . . . . . . . . . . . . . . . . . . 19
189154, 188sseldd 3504 . . . . . . . . . . . . . . . . . 18
190 suceloni 6648 . . . . . . . . . . . . . . . . . 18
191189, 190syl 16 . . . . . . . . . . . . . . . . 17
1923ad2antrr 725 . . . . . . . . . . . . . . . . 17
193 oewordi 7259 . . . . . . . . . . . . . . . . 17
194191, 155, 139, 192, 193syl31anc 1231 . . . . . . . . . . . . . . . 16
195186, 194mpd 15 . . . . . . . . . . . . . . 15
196 simprr 757 . . . . . . . . . . . . . . 15
197195, 196sseldd 3504 . . . . . . . . . . . . . 14
198 peano2 6720 . . . . . . . . . . . . . . . . 17
199198ad2antlr 726 . . . . . . . . . . . . . . . 16
2008cantnfvalf 8105 . . . . . . . . . . . . . . . . 17
201200ffvelrni 6030 . . . . . . . . . . . . . . . 16
202199, 201syl 16 . . . . . . . . . . . . . . 15
203 omcl 7205 . . . . . . . . . . . . . . . 16
204157, 151, 203syl2anc 661 . . . . . . . . . . . . . . 15
205 oaord 7215 . . . . . . . . . . . . . . 15
206202, 157, 204, 205syl3anc 1228 . . . . . . . . . . . . . 14