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

Theorem cantnflt 7373
 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.)
Hypotheses
Ref Expression
cantnfs.1 CNF
cantnfs.2
cantnfs.3
cantnfval.3 OrdIso
cantnfval.4
cantnfval.5 seq𝜔
cantnflt.a
cantnflt.1
cantnflt.2
cantnflt.3
Assertion
Ref Expression
cantnflt
Distinct variable groups:   ,,   ,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem cantnflt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.2 . . . 4
2 cantnflt.2 . . . 4
3 cantnflt.a . . . 4
4 oen0 6584 . . . 4
51, 2, 3, 4syl21anc 1181 . . 3
6 fveq2 5525 . . . . 5
7 0ex 4150 . . . . . 6
8 cantnfval.5 . . . . . . 7 seq𝜔
98seqom0g 6468 . . . . . 6
107, 9ax-mp 8 . . . . 5
116, 10syl6eq 2331 . . . 4
1211eleq1d 2349 . . 3
135, 12syl5ibrcom 213 . 2
142adantr 451 . . . . . . . 8
15 eloni 4402 . . . . . . . 8
1614, 15syl 15 . . . . . . 7
17 cantnflt.3 . . . . . . . . 9
1817adantr 451 . . . . . . . 8
19 cantnfval.3 . . . . . . . . . . 11 OrdIso
2019oif 7245 . . . . . . . . . 10
21 ffn 5389 . . . . . . . . . 10
2220, 21mp1i 11 . . . . . . . . 9
23 cantnflt.1 . . . . . . . . . . 11
2419oicl 7244 . . . . . . . . . . . . . 14
25 ordsuc 4605 . . . . . . . . . . . . . 14
2624, 25mpbi 199 . . . . . . . . . . . . 13
27 ordelon 4416 . . . . . . . . . . . . 13
2826, 23, 27sylancr 644 . . . . . . . . . . . 12
29 ordsssuc 4479 . . . . . . . . . . . 12
3028, 24, 29sylancl 643 . . . . . . . . . . 11
3123, 30mpbird 223 . . . . . . . . . 10
3231adantr 451 . . . . . . . . 9
33 vex 2791 . . . . . . . . . . 11
3433sucid 4471 . . . . . . . . . 10
35 simprr 733 . . . . . . . . . 10
3634, 35syl5eleqr 2370 . . . . . . . . 9
37 fnfvima 5756 . . . . . . . . 9
3822, 32, 36, 37syl3anc 1182 . . . . . . . 8
3918, 38sseldd 3181 . . . . . . 7
40 ordsucss 4609 . . . . . . 7
4116, 39, 40sylc 56 . . . . . 6
42 cnvimass 5033 . . . . . . . . . . . 12
43 cantnfval.4 . . . . . . . . . . . . . . 15
44 cantnfs.1 . . . . . . . . . . . . . . . 16 CNF
45 cantnfs.3 . . . . . . . . . . . . . . . 16
4644, 1, 45cantnfs 7367 . . . . . . . . . . . . . . 15
4743, 46mpbid 201 . . . . . . . . . . . . . 14
4847simpld 445 . . . . . . . . . . . . 13
49 fdm 5393 . . . . . . . . . . . . 13
5048, 49syl 15 . . . . . . . . . . . 12
5142, 50syl5sseq 3226 . . . . . . . . . . 11
52 onss 4582 . . . . . . . . . . . 12
5345, 52syl 15 . . . . . . . . . . 11
5451, 53sstrd 3189 . . . . . . . . . 10
5554adantr 451 . . . . . . . . 9
5623adantr 451 . . . . . . . . . . . 12
5735, 56eqeltrrd 2358 . . . . . . . . . . 11
58 ordsucelsuc 4613 . . . . . . . . . . . 12
5924, 58ax-mp 8 . . . . . . . . . . 11
6057, 59sylibr 203 . . . . . . . . . 10
6120ffvelrni 5664 . . . . . . . . . 10
6260, 61syl 15 . . . . . . . . 9
6355, 62sseldd 3181 . . . . . . . 8
64 suceloni 4604 . . . . . . . 8
6563, 64syl 15 . . . . . . 7
661adantr 451 . . . . . . 7
673adantr 451 . . . . . . 7
68 oewordi 6589 . . . . . . 7
6965, 14, 66, 67, 68syl31anc 1185 . . . . . 6
7041, 69mpd 14 . . . . 5
7135fveq2d 5529 . . . . . 6
72 simprl 732 . . . . . . 7
73 simpl 443 . . . . . . 7
74 eleq1 2343 . . . . . . . . 9
75 suceq 4457 . . . . . . . . . . 11
7675fveq2d 5529 . . . . . . . . . 10
77 fveq2 5525 . . . . . . . . . . . 12
78 suceq 4457 . . . . . . . . . . . 12
7977, 78syl 15 . . . . . . . . . . 11
8079oveq2d 5874 . . . . . . . . . 10
8176, 80eleq12d 2351 . . . . . . . . 9
8274, 81imbi12d 311 . . . . . . . 8
83 eleq1 2343 . . . . . . . . 9
84 suceq 4457 . . . . . . . . . . 11
8584fveq2d 5529 . . . . . . . . . 10
86 fveq2 5525 . . . . . . . . . . . 12
87 suceq 4457 . . . . . . . . . . . 12
8886, 87syl 15 . . . . . . . . . . 11
8988oveq2d 5874 . . . . . . . . . 10
9085, 89eleq12d 2351 . . . . . . . . 9
9183, 90imbi12d 311 . . . . . . . 8
92 eleq1 2343 . . . . . . . . 9
93 suceq 4457 . . . . . . . . . . 11
9493fveq2d 5529 . . . . . . . . . 10
95 fveq2 5525 . . . . . . . . . . . 12
96 suceq 4457 . . . . . . . . . . . 12
9795, 96syl 15 . . . . . . . . . . 11
9897oveq2d 5874 . . . . . . . . . 10
9994, 98eleq12d 2351 . . . . . . . . 9
10092, 99imbi12d 311 . . . . . . . 8
101 peano1 4675 . . . . . . . . . . . . 13
102101a1i 10 . . . . . . . . . . . 12
10344, 1, 45, 19, 43, 8cantnfsuc 7371 . . . . . . . . . . . 12
104102, 103sylan2 460 . . . . . . . . . . 11
10510oveq2i 5869 . . . . . . . . . . . 12
1061adantr 451 . . . . . . . . . . . . . . 15
10720ffvelrni 5664 . . . . . . . . . . . . . . . 16
10854sselda 3180 . . . . . . . . . . . . . . . 16
109107, 108sylan2 460 . . . . . . . . . . . . . . 15
110 oecl 6536 . . . . . . . . . . . . . . 15
111106, 109, 110syl2anc 642 . . . . . . . . . . . . . 14
11248adantr 451 . . . . . . . . . . . . . . . 16
11351sselda 3180 . . . . . . . . . . . . . . . . 17
114107, 113sylan2 460 . . . . . . . . . . . . . . . 16
115 ffvelrn 5663 . . . . . . . . . . . . . . . 16
116112, 114, 115syl2anc 642 . . . . . . . . . . . . . . 15
117 onelon 4417 . . . . . . . . . . . . . . 15
118106, 116, 117syl2anc 642 . . . . . . . . . . . . . 14
119 omcl 6535 . . . . . . . . . . . . . 14
120111, 118, 119syl2anc 642 . . . . . . . . . . . . 13
121 oa0 6515 . . . . . . . . . . . . 13
122120, 121syl 15 . . . . . . . . . . . 12
123105, 122syl5eq 2327 . . . . . . . . . . 11
124104, 123eqtrd 2315 . . . . . . . . . 10
1253adantr 451 . . . . . . . . . . . . . 14
126 oen0 6584 . . . . . . . . . . . . . 14
127106, 109, 125, 126syl21anc 1181 . . . . . . . . . . . . 13
128 omord2 6565 . . . . . . . . . . . . 13
129118, 106, 111, 127, 128syl31anc 1185 . . . . . . . . . . . 12
130116, 129mpbid 201 . . . . . . . . . . 11
131 oesuc 6526 . . . . . . . . . . . 12
132106, 109, 131syl2anc 642 . . . . . . . . . . 11
133130, 132eleqtrrd 2360 . . . . . . . . . 10
134124, 133eqeltrd 2357 . . . . . . . . 9
135134ex 423 . . . . . . . 8
136 ordtr 4406 . . . . . . . . . . . . 13
13724, 136ax-mp 8 . . . . . . . . . . . 12
138 trsuc 4476 . . . . . . . . . . . 12
139137, 138mpan 651 . . . . . . . . . . 11
140139imim1i 54 . . . . . . . . . 10
1411ad2antrr 706 . . . . . . . . . . . . . . . . 17
142 eloni 4402 . . . . . . . . . . . . . . . . 17
143141, 142syl 15 . . . . . . . . . . . . . . . 16
14448ad2antrr 706 . . . . . . . . . . . . . . . . 17
14551ad2antrr 706 . . . . . . . . . . . . . . . . . 18
14620ffvelrni 5664 . . . . . . . . . . . . . . . . . . 19
147146ad2antrl 708 . . . . . . . . . . . . . . . . . 18
148145, 147sseldd 3181 . . . . . . . . . . . . . . . . 17
149 ffvelrn 5663 . . . . . . . . . . . . . . . . 17
150144, 148, 149syl2anc 642 . . . . . . . . . . . . . . . 16
151 ordsucss 4609 . . . . . . . . . . . . . . . 16
152143, 150, 151sylc 56 . . . . . . . . . . . . . . 15
153 onelon 4417 . . . . . . . . . . . . . . . . . 18
154141, 150, 153syl2anc 642 . . . . . . . . . . . . . . . . 17
155 suceloni 4604 . . . . . . . . . . . . . . . . 17
156154, 155syl 15 . . . . . . . . . . . . . . . 16
15754ad2antrr 706 . . . . . . . . . . . . . . . . . 18
158157, 147sseldd 3181 . . . . . . . . . . . . . . . . 17
159 oecl 6536 . . . . . . . . . . . . . . . . 17
160141, 158, 159syl2anc 642 . . . . . . . . . . . . . . . 16
161 omwordi 6569 . . . . . . . . . . . . . . . 16
162156, 141, 160, 161syl3anc 1182 . . . . . . . . . . . . . . 15
163152, 162mpd 14 . . . . . . . . . . . . . 14
164 oesuc 6526 . . . . . . . . . . . . . . 15
165141, 158, 164syl2anc 642 . . . . . . . . . . . . . 14
166163, 165sseqtr4d 3215 . . . . . . . . . . . . 13
167 peano2 4676 . . . . . . . . . . . . . . . . 17
16844, 1, 45, 19, 43, 8cantnfsuc 7371 . . . . . . . . . . . . . . . . 17
169167, 168sylan2 460 . . . . . . . . . . . . . . . 16
170169adantr 451 . . . . . . . . . . . . . . 15
171 eloni 4402 . . . . . . . . . . . . . . . . . . . 20
172158, 171syl 15 . . . . . . . . . . . . . . . . . . 19
173 vex 2791 . . . . . . . . . . . . . . . . . . . . . . 23
174173sucid 4471 . . . . . . . . . . . . . . . . . . . . . 22
175173sucex 4602 . . . . . . . . . . . . . . . . . . . . . . 23
176175epelc 4307 . . . . . . . . . . . . . . . . . . . . . 22
177174, 176mpbir 200 . . . . . . . . . . . . . . . . . . . . 21
178 ssexg 4160 . . . . . . . . . . . . . . . . . . . . . . . . 25
17951, 45, 178syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24
18044, 1, 45, 19, 43cantnfcl 7368 . . . . . . . . . . . . . . . . . . . . . . . . 25
181180simpld 445 . . . . . . . . . . . . . . . . . . . . . . . 24
18219oiiso 7252 . . . . . . . . . . . . . . . . . . . . . . . 24
183179, 181, 182syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23
184183ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22
185139ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . 22
186 simprl 732 . . . . . . . . . . . . . . . . . . . . . 22
187 isorel 5823 . . . . . . . . . . . . . . . . . . . . . 22
188184, 185, 186, 187syl12anc 1180 . . . . . . . . . . . . . . . . . . . . 21
189177, 188mpbii 202 . . . . . . . . . . . . . . . . . . . 20
190 fvex 5539 . . . . . . . . . . . . . . . . . . . . 21
191190epelc 4307 . . . . . . . . . . . . . . . . . . . 20
192189, 191sylib 188 . . . . . . . . . . . . . . . . . . 19
193 ordsucss 4609 . . . . . . . . . . . . . . . . . . 19
194172, 192, 193sylc 56 . . . . . . . . . . . . . . . . . 18
19520ffvelrni 5664 . . . . . . . . . . . . . . . . . . . . . 22
196185, 195syl 15 . . . . . . . . . . . . . . . . . . . . 21
197157, 196sseldd 3181 . . . . . . . . . . . . . . . . . . . 20
198 suceloni 4604 . . . . . . . . . . . . . . . . . . . 20
199197, 198syl 15 . . . . . . . . . . . . . . . . . . 19
2003ad2antrr 706 . . . . . . . . . . . . . . . . . . 19
201 oewordi 6589 . . . . . . . . . . . . . . . . . . 19
202199, 158, 141, 200, 201syl31anc 1185 . . . . . . . . . . . . . . . . . 18
203194, 202mpd 14 . . . . . . . . . . . . . . . . 17
204 simprr 733 . . . . . . . . . . . . . . . . 17
205203, 204sseldd 3181 . . . . . . . . . . . . . . . 16
206167ad2antlr 707 . . . . . . . . . . . . . . . . . 18
2078cantnfvalf 7366 . . . . . . . . . . . . . . . . . . 19
208207ffvelrni 5664 . . . . . . . . . . . . . . . . . 18
209206, 208syl 15 . . . . . . . . . . . . . . . . 17
210 omcl 6535 . . . . . . . . . . . . . . . . . 18
211160, 154, 210syl2anc 642 . . . . . . . . . . . . . . . . 17
212 oaord 6545 . . . . . . . . . . . . . . . . 17
213209, 160, 211, 212syl3anc 1182 . . . . . . . . . . . . . . . 16
214205, 213mpbid 201 . . . . . . . . . . . . . . 15
215170, 214eqeltrd 2357 . . . . . . . . . . . . . 14
216 omsuc 6525 . . . . . . . . . . . . . . 15
217160, 154, 216syl2anc 642 . . . . . . . . . . . . . 14
218215, 217eleqtrrd 2360 . . . . . . . . . . . . 13
219166, 218sseldd 3181 . . . . . . . . . . . 12
220219exp32 588 . . . . . . . . . . 11
221220a2d 23 . . . . . . . . . 10
222140, 221syl5 28 . . . . . . . . 9
223222expcom 424 . . . . . . . 8
22482, 91, 100, 135, 223finds2 4684 . . . . . . 7
22572, 73, 60, 224syl3c 57 . . . . . 6
22671, 225eqeltrd 2357 . . . . 5
22770, 226sseldd 3181 . . . 4
228227expr 598 . . 3
229228rexlimdva 2667 . 2
230180simprd 449 . . . . 5
231 peano2 4676 . . . . 5
232230, 231syl 15 . . . 4
233 elnn 4666 . . . 4
23423, 232, 233syl2anc 642 . . 3
235 nn0suc 4680 . . 3
236234, 235syl 15 . 2
23713, 229, 236mpjaod 370 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wo 357   wa 358   wceq 1623   wcel 1684  wrex 2544  cvv 2788   cdif 3149   wss 3152  c0 3455   class class class wbr 4023   wtr 4113   cep 4303   wwe 4351   word 4391  con0 4392   csuc 4394  com 4656  ccnv 4688   cdm 4689  cima 4692   wfn 5250  wf 5251  cfv 5255   wiso 5256  (class class class)co 5858   cmpt2 5860  seq𝜔cseqom 6459  c1o 6472   coa 6476   comu 6477   coe 6478  cfn 6863  OrdIsocoi 7224   CNF ccnf 7362 This theorem is referenced by:  cantnflt2  7374  cnfcomlem  7402 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-seqom 6460  df-1o 6479  df-2o 6480  df-oadd 6483  df-omul 6484  df-oexp 6485  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-oi 7225  df-cnf 7363
 Copyright terms: Public domain W3C validator