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

Theorem cantnflt 7627
 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 6829 . . . 4
51, 2, 3, 4syl21anc 1183 . . 3
6 fveq2 5728 . . . . 5
7 0ex 4339 . . . . . 6
8 cantnfval.5 . . . . . . 7 seq𝜔
98seqom0g 6713 . . . . . 6
107, 9ax-mp 8 . . . . 5
116, 10syl6eq 2484 . . . 4
1211eleq1d 2502 . . 3
135, 12syl5ibrcom 214 . 2
142adantr 452 . . . . . . 7
15 eloni 4591 . . . . . . 7
1614, 15syl 16 . . . . . 6
17 cantnflt.3 . . . . . . . 8
1817adantr 452 . . . . . . 7
19 cantnfval.3 . . . . . . . . . 10 OrdIso
2019oif 7499 . . . . . . . . 9
21 ffn 5591 . . . . . . . . 9
2220, 21mp1i 12 . . . . . . . 8
23 cantnflt.1 . . . . . . . . . 10
2419oicl 7498 . . . . . . . . . . . . 13
25 ordsuc 4794 . . . . . . . . . . . . 13
2624, 25mpbi 200 . . . . . . . . . . . 12
27 ordelon 4605 . . . . . . . . . . . 12
2826, 23, 27sylancr 645 . . . . . . . . . . 11
29 ordsssuc 4668 . . . . . . . . . . 11
3028, 24, 29sylancl 644 . . . . . . . . . 10
3123, 30mpbird 224 . . . . . . . . 9
3231adantr 452 . . . . . . . 8
33 vex 2959 . . . . . . . . . 10
3433sucid 4660 . . . . . . . . 9
35 simprr 734 . . . . . . . . 9
3634, 35syl5eleqr 2523 . . . . . . . 8
37 fnfvima 5976 . . . . . . . 8
3822, 32, 36, 37syl3anc 1184 . . . . . . 7
3918, 38sseldd 3349 . . . . . 6
40 ordsucss 4798 . . . . . 6
4116, 39, 40sylc 58 . . . . 5
42 cnvimass 5224 . . . . . . . . . . 11
43 cantnfval.4 . . . . . . . . . . . . . 14
44 cantnfs.1 . . . . . . . . . . . . . . 15 CNF
45 cantnfs.3 . . . . . . . . . . . . . . 15
4644, 1, 45cantnfs 7621 . . . . . . . . . . . . . 14
4743, 46mpbid 202 . . . . . . . . . . . . 13
4847simpld 446 . . . . . . . . . . . 12
49 fdm 5595 . . . . . . . . . . . 12
5048, 49syl 16 . . . . . . . . . . 11
5142, 50syl5sseq 3396 . . . . . . . . . 10
52 onss 4771 . . . . . . . . . . 11
5345, 52syl 16 . . . . . . . . . 10
5451, 53sstrd 3358 . . . . . . . . 9
5554adantr 452 . . . . . . . 8
5623adantr 452 . . . . . . . . . . 11
5735, 56eqeltrrd 2511 . . . . . . . . . 10
58 ordsucelsuc 4802 . . . . . . . . . . 11
5924, 58ax-mp 8 . . . . . . . . . 10
6057, 59sylibr 204 . . . . . . . . 9
6120ffvelrni 5869 . . . . . . . . 9
6260, 61syl 16 . . . . . . . 8
6355, 62sseldd 3349 . . . . . . 7
64 suceloni 4793 . . . . . . 7
6563, 64syl 16 . . . . . 6
661adantr 452 . . . . . 6
673adantr 452 . . . . . 6
68 oewordi 6834 . . . . . 6
6965, 14, 66, 67, 68syl31anc 1187 . . . . 5
7041, 69mpd 15 . . . 4
7135fveq2d 5732 . . . . 5
72 simprl 733 . . . . . 6
73 simpl 444 . . . . . 6
74 eleq1 2496 . . . . . . . 8
75 suceq 4646 . . . . . . . . . 10
7675fveq2d 5732 . . . . . . . . 9
77 fveq2 5728 . . . . . . . . . . 11
78 suceq 4646 . . . . . . . . . . 11
7977, 78syl 16 . . . . . . . . . 10
8079oveq2d 6097 . . . . . . . . 9
8176, 80eleq12d 2504 . . . . . . . 8
8274, 81imbi12d 312 . . . . . . 7
83 eleq1 2496 . . . . . . . 8
84 suceq 4646 . . . . . . . . . 10
8584fveq2d 5732 . . . . . . . . 9
86 fveq2 5728 . . . . . . . . . . 11
87 suceq 4646 . . . . . . . . . . 11
8886, 87syl 16 . . . . . . . . . 10
8988oveq2d 6097 . . . . . . . . 9
9085, 89eleq12d 2504 . . . . . . . 8
9183, 90imbi12d 312 . . . . . . 7
92 eleq1 2496 . . . . . . . 8
93 suceq 4646 . . . . . . . . . 10
9493fveq2d 5732 . . . . . . . . 9
95 fveq2 5728 . . . . . . . . . . 11
96 suceq 4646 . . . . . . . . . . 11
9795, 96syl 16 . . . . . . . . . 10
9897oveq2d 6097 . . . . . . . . 9
9994, 98eleq12d 2504 . . . . . . . 8
10092, 99imbi12d 312 . . . . . . 7
10148adantr 452 . . . . . . . . . . 11
10220ffvelrni 5869 . . . . . . . . . . . 12
10351sselda 3348 . . . . . . . . . . . 12
104102, 103sylan2 461 . . . . . . . . . . 11
105101, 104ffvelrnd 5871 . . . . . . . . . 10
1061adantr 452 . . . . . . . . . . . 12
107 onelon 4606 . . . . . . . . . . . 12
108106, 105, 107syl2anc 643 . . . . . . . . . . 11
10954sselda 3348 . . . . . . . . . . . . 13
110102, 109sylan2 461 . . . . . . . . . . . 12
111 oecl 6781 . . . . . . . . . . . 12
112106, 110, 111syl2anc 643 . . . . . . . . . . 11
1133adantr 452 . . . . . . . . . . . 12
114 oen0 6829 . . . . . . . . . . . 12
115106, 110, 113, 114syl21anc 1183 . . . . . . . . . . 11
116 omord2 6810 . . . . . . . . . . 11
117108, 106, 112, 115, 116syl31anc 1187 . . . . . . . . . 10
118105, 117mpbid 202 . . . . . . . . 9
119 peano1 4864 . . . . . . . . . . . 12
120119a1i 11 . . . . . . . . . . 11
12144, 1, 45, 19, 43, 8cantnfsuc 7625 . . . . . . . . . . 11
122120, 121sylan2 461 . . . . . . . . . 10
12310oveq2i 6092 . . . . . . . . . . 11
124 omcl 6780 . . . . . . . . . . . . 13
125112, 108, 124syl2anc 643 . . . . . . . . . . . 12
126 oa0 6760 . . . . . . . . . . . 12
127125, 126syl 16 . . . . . . . . . . 11
128123, 127syl5eq 2480 . . . . . . . . . 10
129122, 128eqtrd 2468 . . . . . . . . 9
130 oesuc 6771 . . . . . . . . . 10
131106, 110, 130syl2anc 643 . . . . . . . . 9
132118, 129, 1313eltr4d 2517 . . . . . . . 8
133132ex 424 . . . . . . 7
134 ordtr 4595 . . . . . . . . . . . 12
13524, 134ax-mp 8 . . . . . . . . . . 11
136 trsuc 4666 . . . . . . . . . . 11
137135, 136mpan 652 . . . . . . . . . 10
138137imim1i 56 . . . . . . . . 9
1391ad2antrr 707 . . . . . . . . . . . . . . . 16
140 eloni 4591 . . . . . . . . . . . . . . . 16
141139, 140syl 16 . . . . . . . . . . . . . . 15
14248ad2antrr 707 . . . . . . . . . . . . . . . 16
14351ad2antrr 707 . . . . . . . . . . . . . . . . 17
14420ffvelrni 5869 . . . . . . . . . . . . . . . . . 18
145144ad2antrl 709 . . . . . . . . . . . . . . . . 17
146143, 145sseldd 3349 . . . . . . . . . . . . . . . 16
147142, 146ffvelrnd 5871 . . . . . . . . . . . . . . 15
148 ordsucss 4798 . . . . . . . . . . . . . . 15
149141, 147, 148sylc 58 . . . . . . . . . . . . . 14
150 onelon 4606 . . . . . . . . . . . . . . . . 17
151139, 147, 150syl2anc 643 . . . . . . . . . . . . . . . 16
152 suceloni 4793 . . . . . . . . . . . . . . . 16
153151, 152syl 16 . . . . . . . . . . . . . . 15
15454ad2antrr 707 . . . . . . . . . . . . . . . . 17
155154, 145sseldd 3349 . . . . . . . . . . . . . . . 16
156 oecl 6781 . . . . . . . . . . . . . . . 16
157139, 155, 156syl2anc 643 . . . . . . . . . . . . . . 15
158 omwordi 6814 . . . . . . . . . . . . . . 15
159153, 139, 157, 158syl3anc 1184 . . . . . . . . . . . . . 14
160149, 159mpd 15 . . . . . . . . . . . . 13
161 oesuc 6771 . . . . . . . . . . . . . 14
162139, 155, 161syl2anc 643 . . . . . . . . . . . . 13
163160, 162sseqtr4d 3385 . . . . . . . . . . . 12
164 eloni 4591 . . . . . . . . . . . . . . . . . 18
165155, 164syl 16 . . . . . . . . . . . . . . . . 17
166 vex 2959 . . . . . . . . . . . . . . . . . . . . 21
167166sucid 4660 . . . . . . . . . . . . . . . . . . . 20
168166sucex 4791 . . . . . . . . . . . . . . . . . . . . 21
169168epelc 4496 . . . . . . . . . . . . . . . . . . . 20
170167, 169mpbir 201 . . . . . . . . . . . . . . . . . . 19
17145, 51ssexd 4350 . . . . . . . . . . . . . . . . . . . . . 22
17244, 1, 45, 19, 43cantnfcl 7622 . . . . . . . . . . . . . . . . . . . . . . 23
173172simpld 446 . . . . . . . . . . . . . . . . . . . . . 22
17419oiiso 7506 . . . . . . . . . . . . . . . . . . . . . 22
175171, 173, 174syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
176175ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
177137ad2antrl 709 . . . . . . . . . . . . . . . . . . . 20
178 simprl 733 . . . . . . . . . . . . . . . . . . . 20
179 isorel 6046 . . . . . . . . . . . . . . . . . . . 20
180176, 177, 178, 179syl12anc 1182 . . . . . . . . . . . . . . . . . . 19
181170, 180mpbii 203 . . . . . . . . . . . . . . . . . 18
182 fvex 5742 . . . . . . . . . . . . . . . . . . 19
183182epelc 4496 . . . . . . . . . . . . . . . . . 18
184181, 183sylib 189 . . . . . . . . . . . . . . . . 17
185 ordsucss 4798 . . . . . . . . . . . . . . . . 17
186165, 184, 185sylc 58 . . . . . . . . . . . . . . . 16
18720ffvelrni 5869 . . . . . . . . . . . . . . . . . . . 20
188177, 187syl 16 . . . . . . . . . . . . . . . . . . 19
189154, 188sseldd 3349 . . . . . . . . . . . . . . . . . 18
190 suceloni 4793 . . . . . . . . . . . . . . . . . 18
191189, 190syl 16 . . . . . . . . . . . . . . . . 17
1923ad2antrr 707 . . . . . . . . . . . . . . . . 17
193 oewordi 6834 . . . . . . . . . . . . . . . . 17
194191, 155, 139, 192, 193syl31anc 1187 . . . . . . . . . . . . . . . 16
195186, 194mpd 15 . . . . . . . . . . . . . . 15
196 simprr 734 . . . . . . . . . . . . . . 15
197195, 196sseldd 3349 . . . . . . . . . . . . . 14
198 peano2 4865 . . . . . . . . . . . . . . . . 17
199198ad2antlr 708 . . . . . . . . . . . . . . . 16
2008cantnfvalf 7620 . . . . . . . . . . . . . . . . 17
201200ffvelrni 5869 . . . . . . . . . . . . . . . 16
202199, 201syl 16 . . . . . . . . . . . . . . 15
203 omcl 6780 . . . . . . . . . . . . . . . 16
204157, 151, 203syl2anc 643 . . . . . . . . . . . . . . 15
205 oaord 6790 . . . . . . . . . . . . . . 15
206202, 157, 204, 205syl3anc 1184 . . . . . . . . . . . . . 14
207197, 206mpbid 202 . . . . . . . . . . . . 13
20844, 1, 45, 19, 43, 8cantnfsuc 7625 . . . . . . . . . . . . . . 15
209198, 208sylan2 461 . . . . . . . . . . . . . 14
210209adantr 452 . . . . . . . . . . . . 13
211 omsuc 6770 . . . . . . . . . . . . . 14
212157, 151, 211syl2anc 643 . . . . . . . . . . . . 13
213207, 210, 2123eltr4d 2517 . . . . . . . . . . . 12
214163, 213sseldd 3349 . . . . . . . . . . 11
215214exp32 589 . . . . . . . . . 10
216215a2d 24 . . . . . . . . 9
217138, 216syl5 30 . . . . . . . 8
218217expcom 425 . . . . . . 7
21982, 91, 100, 133, 218finds2 4873 . . . . . 6
22072, 73, 60, 219syl3c 59 . . . . 5
22171, 220eqeltrd 2510 . . . 4
22270, 221sseldd 3349 . . 3
223222rexlimdvaa 2831 . 2
224172simprd 450 . . . . 5
225 peano2 4865 . . . . 5
226224, 225syl 16 . . . 4
227 elnn 4855 . . . 4
22823, 226, 227syl2anc 643 . . 3
229 nn0suc 4869 . . 3
230228, 229syl 16 . 2
23113, 223, 230mpjaod 371 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358   wa 359   wceq 1652   wcel 1725  wrex 2706  cvv 2956   cdif 3317   wss 3320  c0 3628   class class class wbr 4212   wtr 4302   cep 4492   wwe 4540   word 4580  con0 4581   csuc 4583  com 4845  ccnv 4877   cdm 4878  cima 4881   wfn 5449  wf 5450  cfv 5454   wiso 5455  (class class class)co 6081   cmpt2 6083  seq𝜔cseqom 6704  c1o 6717   coa 6721   comu 6722   coe 6723  cfn 7109  OrdIsocoi 7478   CNF ccnf 7616 This theorem is referenced by:  cantnflt2  7628  cnfcomlem  7656 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-se 4542  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-isom 5463  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-seqom 6705  df-1o 6724  df-2o 6725  df-oadd 6728  df-omul 6729  df-oexp 6730  df-er 6905  df-map 7020  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-oi 7479  df-cnf 7617
 Copyright terms: Public domain W3C validator