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

Theorem cantnfltOLD 8153
 Description: An upper bound on the partial sums of the CNF 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 which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015.) Obsolete version of cantnflt 8123 as of 29-Jun-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1 CNF
cantnfsOLD.2
cantnfsOLD.3
cantnfvalOLD.3 OrdIso
cantnfvalOLD.4
cantnfvalOLD.5 seq𝜔
cantnfltOLD.a
cantnfltOLD.1
cantnfltOLD.2
cantnfltOLD.3
Assertion
Ref Expression
cantnfltOLD
Distinct variable groups:   ,,   ,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem cantnfltOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfsOLD.2 . . . 4
2 cantnfltOLD.2 . . . 4
3 cantnfltOLD.a . . . 4
4 oen0 7272 . . . 4
51, 2, 3, 4syl21anc 1229 . . 3
6 fveq2 5849 . . . . 5
7 0ex 4526 . . . . . 6
8 cantnfvalOLD.5 . . . . . . 7 seq𝜔
98seqom0g 7158 . . . . . 6
107, 9ax-mp 5 . . . . 5
116, 10syl6eq 2459 . . . 4
1211eleq1d 2471 . . 3
135, 12syl5ibrcom 222 . 2
142adantr 463 . . . . . . 7
15 eloni 5420 . . . . . . 7
1614, 15syl 17 . . . . . 6
17 cantnfltOLD.3 . . . . . . . 8
1817adantr 463 . . . . . . 7
19 cantnfvalOLD.3 . . . . . . . . . 10 OrdIso
2019oif 7989 . . . . . . . . 9
21 ffn 5714 . . . . . . . . 9
2220, 21mp1i 13 . . . . . . . 8
23 cantnfltOLD.1 . . . . . . . . . 10
2419oicl 7988 . . . . . . . . . . . . 13
25 ordsuc 6632 . . . . . . . . . . . . 13
2624, 25mpbi 208 . . . . . . . . . . . 12
27 ordelon 5434 . . . . . . . . . . . 12
2826, 23, 27sylancr 661 . . . . . . . . . . 11
29 ordsssuc 5496 . . . . . . . . . . 11
3028, 24, 29sylancl 660 . . . . . . . . . 10
3123, 30mpbird 232 . . . . . . . . 9
3231adantr 463 . . . . . . . 8
33 vex 3062 . . . . . . . . . 10
3433sucid 5489 . . . . . . . . 9
35 simprr 758 . . . . . . . . 9
3634, 35syl5eleqr 2497 . . . . . . . 8
37 fnfvima 6131 . . . . . . . 8
3822, 32, 36, 37syl3anc 1230 . . . . . . 7
3918, 38sseldd 3443 . . . . . 6
40 ordsucss 6636 . . . . . 6
4116, 39, 40sylc 59 . . . . 5
42 cnvimass 5177 . . . . . . . . . . 11
43 cantnfvalOLD.4 . . . . . . . . . . . . . 14
44 cantnfsOLD.1 . . . . . . . . . . . . . . 15 CNF
45 cantnfsOLD.3 . . . . . . . . . . . . . . 15
4644, 1, 45cantnfsOLD 8147 . . . . . . . . . . . . . 14
4743, 46mpbid 210 . . . . . . . . . . . . 13
4847simpld 457 . . . . . . . . . . . 12
49 fdm 5718 . . . . . . . . . . . 12
5048, 49syl 17 . . . . . . . . . . 11
5142, 50syl5sseq 3490 . . . . . . . . . 10
52 onss 6608 . . . . . . . . . . 11
5345, 52syl 17 . . . . . . . . . 10
5451, 53sstrd 3452 . . . . . . . . 9
5554adantr 463 . . . . . . . 8
5623adantr 463 . . . . . . . . . . 11
5735, 56eqeltrrd 2491 . . . . . . . . . 10
58 ordsucelsuc 6640 . . . . . . . . . . 11
5924, 58ax-mp 5 . . . . . . . . . 10
6057, 59sylibr 212 . . . . . . . . 9
6120ffvelrni 6008 . . . . . . . . 9
6260, 61syl 17 . . . . . . . 8
6355, 62sseldd 3443 . . . . . . 7
64 suceloni 6631 . . . . . . 7
6563, 64syl 17 . . . . . 6
661adantr 463 . . . . . 6
673adantr 463 . . . . . 6
68 oewordi 7277 . . . . . 6
6965, 14, 66, 67, 68syl31anc 1233 . . . . 5
7041, 69mpd 15 . . . 4
7135fveq2d 5853 . . . . 5
72 simprl 756 . . . . . 6
73 simpl 455 . . . . . 6
74 eleq1 2474 . . . . . . . 8
75 suceq 5475 . . . . . . . . . 10
7675fveq2d 5853 . . . . . . . . 9
77 fveq2 5849 . . . . . . . . . . 11
78 suceq 5475 . . . . . . . . . . 11
7977, 78syl 17 . . . . . . . . . 10
8079oveq2d 6294 . . . . . . . . 9
8176, 80eleq12d 2484 . . . . . . . 8
8274, 81imbi12d 318 . . . . . . 7
83 eleq1 2474 . . . . . . . 8
84 suceq 5475 . . . . . . . . . 10
8584fveq2d 5853 . . . . . . . . 9
86 fveq2 5849 . . . . . . . . . . 11
87 suceq 5475 . . . . . . . . . . 11
8886, 87syl 17 . . . . . . . . . 10
8988oveq2d 6294 . . . . . . . . 9
9085, 89eleq12d 2484 . . . . . . . 8
9183, 90imbi12d 318 . . . . . . 7
92 eleq1 2474 . . . . . . . 8
93 suceq 5475 . . . . . . . . . 10
9493fveq2d 5853 . . . . . . . . 9
95 fveq2 5849 . . . . . . . . . . 11
96 suceq 5475 . . . . . . . . . . 11
9795, 96syl 17 . . . . . . . . . 10
9897oveq2d 6294 . . . . . . . . 9
9994, 98eleq12d 2484 . . . . . . . 8
10092, 99imbi12d 318 . . . . . . 7
10148adantr 463 . . . . . . . . . . 11
10220ffvelrni 6008 . . . . . . . . . . . 12
10351sselda 3442 . . . . . . . . . . . 12
104102, 103sylan2 472 . . . . . . . . . . 11
105101, 104ffvelrnd 6010 . . . . . . . . . 10
1061adantr 463 . . . . . . . . . . . 12
107 onelon 5435 . . . . . . . . . . . 12
108106, 105, 107syl2anc 659 . . . . . . . . . . 11
10954sselda 3442 . . . . . . . . . . . . 13
110102, 109sylan2 472 . . . . . . . . . . . 12
111 oecl 7224 . . . . . . . . . . . 12
112106, 110, 111syl2anc 659 . . . . . . . . . . 11
1133adantr 463 . . . . . . . . . . . 12
114 oen0 7272 . . . . . . . . . . . 12
115106, 110, 113, 114syl21anc 1229 . . . . . . . . . . 11
116 omord2 7253 . . . . . . . . . . 11
117108, 106, 112, 115, 116syl31anc 1233 . . . . . . . . . 10
118105, 117mpbid 210 . . . . . . . . 9
119 peano1 6703 . . . . . . . . . . . 12
120119a1i 11 . . . . . . . . . . 11
12144, 1, 45, 19, 43, 8cantnfsucOLD 8151 . . . . . . . . . . 11
122120, 121sylan2 472 . . . . . . . . . 10
12310oveq2i 6289 . . . . . . . . . . 11
124 omcl 7223 . . . . . . . . . . . . 13
125112, 108, 124syl2anc 659 . . . . . . . . . . . 12
126 oa0 7203 . . . . . . . . . . . 12
127125, 126syl 17 . . . . . . . . . . 11
128123, 127syl5eq 2455 . . . . . . . . . 10
129122, 128eqtrd 2443 . . . . . . . . 9
130 oesuc 7214 . . . . . . . . . 10
131106, 110, 130syl2anc 659 . . . . . . . . 9
132118, 129, 1313eltr4d 2505 . . . . . . . 8
133132ex 432 . . . . . . 7
134 ordtr 5424 . . . . . . . . . . . 12
13524, 134ax-mp 5 . . . . . . . . . . 11
136 trsuc 5494 . . . . . . . . . . 11
137135, 136mpan 668 . . . . . . . . . 10
138137imim1i 57 . . . . . . . . 9
1391ad2antrr 724 . . . . . . . . . . . . . . . 16
140 eloni 5420 . . . . . . . . . . . . . . . 16
141139, 140syl 17 . . . . . . . . . . . . . . 15
14248ad2antrr 724 . . . . . . . . . . . . . . . 16
14351ad2antrr 724 . . . . . . . . . . . . . . . . 17
14420ffvelrni 6008 . . . . . . . . . . . . . . . . . 18
145144ad2antrl 726 . . . . . . . . . . . . . . . . 17
146143, 145sseldd 3443 . . . . . . . . . . . . . . . 16
147142, 146ffvelrnd 6010 . . . . . . . . . . . . . . 15
148 ordsucss 6636 . . . . . . . . . . . . . . 15
149141, 147, 148sylc 59 . . . . . . . . . . . . . 14
150 onelon 5435 . . . . . . . . . . . . . . . . 17
151139, 147, 150syl2anc 659 . . . . . . . . . . . . . . . 16
152 suceloni 6631 . . . . . . . . . . . . . . . 16
153151, 152syl 17 . . . . . . . . . . . . . . 15
15454ad2antrr 724 . . . . . . . . . . . . . . . . 17
155154, 145sseldd 3443 . . . . . . . . . . . . . . . 16
156 oecl 7224 . . . . . . . . . . . . . . . 16
157139, 155, 156syl2anc 659 . . . . . . . . . . . . . . 15
158 omwordi 7257 . . . . . . . . . . . . . . 15
159153, 139, 157, 158syl3anc 1230 . . . . . . . . . . . . . 14
160149, 159mpd 15 . . . . . . . . . . . . 13
161 oesuc 7214 . . . . . . . . . . . . . 14
162139, 155, 161syl2anc 659 . . . . . . . . . . . . 13
163160, 162sseqtr4d 3479 . . . . . . . . . . . 12
164 eloni 5420 . . . . . . . . . . . . . . . . . 18
165155, 164syl 17 . . . . . . . . . . . . . . . . 17
166 vex 3062 . . . . . . . . . . . . . . . . . . . . 21
167166sucid 5489 . . . . . . . . . . . . . . . . . . . 20
168166sucex 6629 . . . . . . . . . . . . . . . . . . . . 21
169168epelc 4736 . . . . . . . . . . . . . . . . . . . 20
170167, 169mpbir 209 . . . . . . . . . . . . . . . . . . 19
17145, 51ssexd 4541 . . . . . . . . . . . . . . . . . . . . . 22
17244, 1, 45, 19, 43cantnfclOLD 8148 . . . . . . . . . . . . . . . . . . . . . . 23
173172simpld 457 . . . . . . . . . . . . . . . . . . . . . 22
17419oiiso 7996 . . . . . . . . . . . . . . . . . . . . . 22
175171, 173, 174syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21
176175ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20
177137ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20
178 simprl 756 . . . . . . . . . . . . . . . . . . . 20
179 isorel 6205 . . . . . . . . . . . . . . . . . . . 20
180176, 177, 178, 179syl12anc 1228 . . . . . . . . . . . . . . . . . . 19
181170, 180mpbii 211 . . . . . . . . . . . . . . . . . 18
182 fvex 5859 . . . . . . . . . . . . . . . . . . 19
183182epelc 4736 . . . . . . . . . . . . . . . . . 18
184181, 183sylib 196 . . . . . . . . . . . . . . . . 17
185 ordsucss 6636 . . . . . . . . . . . . . . . . 17
186165, 184, 185sylc 59 . . . . . . . . . . . . . . . 16
18720ffvelrni 6008 . . . . . . . . . . . . . . . . . . . 20
188177, 187syl 17 . . . . . . . . . . . . . . . . . . 19
189154, 188sseldd 3443 . . . . . . . . . . . . . . . . . 18
190 suceloni 6631 . . . . . . . . . . . . . . . . . 18
191189, 190syl 17 . . . . . . . . . . . . . . . . 17
1923ad2antrr 724 . . . . . . . . . . . . . . . . 17
193 oewordi 7277 . . . . . . . . . . . . . . . . 17
194191, 155, 139, 192, 193syl31anc 1233 . . . . . . . . . . . . . . . 16
195186, 194mpd 15 . . . . . . . . . . . . . . 15
196 simprr 758 . . . . . . . . . . . . . . 15
197195, 196sseldd 3443 . . . . . . . . . . . . . 14
198 peano2 6704 . . . . . . . . . . . . . . . . 17
199198ad2antlr 725 . . . . . . . . . . . . . . . 16
2008cantnfvalf 8116 . . . . . . . . . . . . . . . . 17
201200ffvelrni 6008 . . . . . . . . . . . . . . . 16
202199, 201syl 17 . . . . . . . . . . . . . . 15
203 omcl 7223 . . . . . . . . . . . . . . . 16
204157, 151, 203syl2anc 659 . . . . . . . . . . . . . . 15
205 oaord 7233 . . . . . . . . . . . . . . 15
206202, 157, 204, 205syl3anc 1230 . . . . . . . . . . . . . 14
207197, 206mpbid 210 . . . . . . . . . . . . 13
20844, 1, 45, 19, 43, 8cantnfsucOLD 8151 . . . . . . . . . . . . . . 15
209198, 208sylan2 472 . . . . . . . . . . . . . 14
210209adantr 463 . . . . . . . . . . . . 13
211 omsuc 7213 . . . . . . . . . . . . . 14
212157, 151, 211syl2anc 659 . . . . . . . . . . . . 13
213207, 210, 2123eltr4d 2505 . . . . . . . . . . . 12
214163, 213sseldd 3443 . . . . . . . . . . 11
215214exp32 603 . . . . . . . . . 10
216215a2d 26 . . . . . . . . 9
217138, 216syl5 30 . . . . . . . 8
218217expcom 433 . . . . . . 7
21982, 91, 100, 133, 218finds2 6712 . . . . . 6
22072, 73, 60, 219syl3c 60 . . . . 5
22171, 220eqeltrd 2490 . . . 4
22270, 221sseldd 3443 . . 3
223222rexlimdvaa 2897 . 2
224172simprd 461 . . . . 5
225 peano2 6704 . . . . 5
226224, 225syl 17 . . . 4
227 elnn 6693 . . . 4
22823, 226, 227syl2anc 659 . . 3
229 nn0suc 6708 . . 3
230228, 229syl 17 . 2
23113, 223, 230mpjaod 379 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wo 366   wa 367   wceq 1405   wcel 1842  wrex 2755  cvv 3059   cdif 3411   wss 3414  c0 3738   class class class wbr 4395   wtr 4489   cep 4732   wwe 4781  ccnv 4822   cdm 4823  cima 4826   word 5409  con0 5410   csuc 5412   wfn 5564  wf 5565  cfv 5569   wiso 5570  (class class class)co 6278   cmpt2 6280  com 6683  seq𝜔cseqom 7149  c1o 7160   coa 7164   comu 7165   coe 7166  cfn 7554  OrdIsocoi 7968   CNF ccnf 8110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-1st 6784  df-2nd 6785  df-supp 6903  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-seqom 7150  df-1o 7167  df-2o 7168  df-oadd 7171  df-omul 7172  df-oexp 7173  df-er 7348  df-map 7459  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-fsupp 7864  df-oi 7969  df-cnf 8111 This theorem is referenced by:  cantnflt2OLD  8154  cnfcomlemOLD  8183
 Copyright terms: Public domain W3C validator