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

Theorem vdwlem10 15019
 Description: Lemma for vdw 15023. Set up secondary induction on . (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdw.r
vdwlem9.k
vdwlem9.s MonoAP
vdwlem10.m
Assertion
Ref Expression
vdwlem10 PolyAP MonoAP
Distinct variable groups:   ,,   ,,,   ,,   ,,,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem vdwlem10
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwlem10.m . 2
2 opeq1 4158 . . . . . . 7
32breq1d 4405 . . . . . 6 PolyAP PolyAP
43orbi1d 717 . . . . 5 PolyAP MonoAP PolyAP MonoAP
54rexralbidv 2898 . . . 4 PolyAP MonoAP PolyAP MonoAP
65imbi2d 323 . . 3 PolyAP MonoAP PolyAP MonoAP
7 opeq1 4158 . . . . . . 7
87breq1d 4405 . . . . . 6 PolyAP PolyAP
98orbi1d 717 . . . . 5 PolyAP MonoAP PolyAP MonoAP
109rexralbidv 2898 . . . 4 PolyAP MonoAP PolyAP MonoAP
1110imbi2d 323 . . 3 PolyAP MonoAP PolyAP MonoAP
12 opeq1 4158 . . . . . . 7
1312breq1d 4405 . . . . . 6 PolyAP PolyAP
1413orbi1d 717 . . . . 5 PolyAP MonoAP PolyAP MonoAP
1514rexralbidv 2898 . . . 4 PolyAP MonoAP PolyAP MonoAP
1615imbi2d 323 . . 3 PolyAP MonoAP PolyAP MonoAP
17 opeq1 4158 . . . . . . 7
1817breq1d 4405 . . . . . 6 PolyAP PolyAP
1918orbi1d 717 . . . . 5 PolyAP MonoAP PolyAP MonoAP
2019rexralbidv 2898 . . . 4 PolyAP MonoAP PolyAP MonoAP
2120imbi2d 323 . . 3 PolyAP MonoAP PolyAP MonoAP
22 vdw.r . . . . . 6
23 vdwlem9.s . . . . . 6 MonoAP
24 oveq1 6315 . . . . . . . . 9
2524raleqdv 2979 . . . . . . . 8 MonoAP MonoAP
2625rexbidv 2892 . . . . . . 7 MonoAP MonoAP
2726rspcv 3132 . . . . . 6 MonoAP MonoAP
2822, 23, 27sylc 61 . . . . 5 MonoAP
29 oveq2 6316 . . . . . . . 8
3029oveq2d 6324 . . . . . . 7
3130raleqdv 2979 . . . . . 6 MonoAP MonoAP
3231cbvrexv 3006 . . . . 5 MonoAP MonoAP
3328, 32sylib 201 . . . 4 MonoAP
34 breq2 4399 . . . . . . 7 MonoAP MonoAP
3534cbvralv 3005 . . . . . 6 MonoAP MonoAP
36 2nn 10790 . . . . . . . 8
37 simpr 468 . . . . . . . 8
38 nnmulcl 10654 . . . . . . . 8
3936, 37, 38sylancr 676 . . . . . . 7
4022adantr 472 . . . . . . . . . . 11
41 ovex 6336 . . . . . . . . . . 11
42 elmapg 7503 . . . . . . . . . . 11
4340, 41, 42sylancl 675 . . . . . . . . . 10
4443biimpa 492 . . . . . . . . 9
45 simplr 770 . . . . . . . . . . . . . 14
46 elfznn 11854 . . . . . . . . . . . . . . . . . . 19
4746adantl 473 . . . . . . . . . . . . . . . . . 18
4847nnred 10646 . . . . . . . . . . . . . . . . 17
49 simpllr 777 . . . . . . . . . . . . . . . . . 18
5049nnred 10646 . . . . . . . . . . . . . . . . 17
51 elfzle2 11829 . . . . . . . . . . . . . . . . . 18
5251adantl 473 . . . . . . . . . . . . . . . . 17
5348, 50, 50, 52leadd1dd 10248 . . . . . . . . . . . . . . . 16
5449nncnd 10647 . . . . . . . . . . . . . . . . 17
55542timesd 10878 . . . . . . . . . . . . . . . 16
5653, 55breqtrrd 4422 . . . . . . . . . . . . . . 15
5747, 49nnaddcld 10678 . . . . . . . . . . . . . . . . 17
58 nnuz 11218 . . . . . . . . . . . . . . . . 17
5957, 58syl6eleq 2559 . . . . . . . . . . . . . . . 16
6039ad2antrr 740 . . . . . . . . . . . . . . . . 17
6160nnzd 11062 . . . . . . . . . . . . . . . 16
62 elfz5 11818 . . . . . . . . . . . . . . . 16
6359, 61, 62syl2anc 673 . . . . . . . . . . . . . . 15
6456, 63mpbird 240 . . . . . . . . . . . . . 14
6545, 64ffvelrnd 6038 . . . . . . . . . . . . 13
66 oveq1 6315 . . . . . . . . . . . . . . 15
6766fveq2d 5883 . . . . . . . . . . . . . 14
6867cbvmptv 4488 . . . . . . . . . . . . 13
6965, 68fmptd 6061 . . . . . . . . . . . 12
70 ovex 6336 . . . . . . . . . . . . . 14
71 elmapg 7503 . . . . . . . . . . . . . 14
7240, 70, 71sylancl 675 . . . . . . . . . . . . 13
7372biimpar 493 . . . . . . . . . . . 12
7469, 73syldan 478 . . . . . . . . . . 11
75 breq2 4399 . . . . . . . . . . . 12 MonoAP MonoAP
7675rspcv 3132 . . . . . . . . . . 11 MonoAP MonoAP
7774, 76syl 17 . . . . . . . . . 10 MonoAP MonoAP
78 2nn0 10910 . . . . . . . . . . . . 13
79 vdwlem9.k . . . . . . . . . . . . . 14
8079ad2antrr 740 . . . . . . . . . . . . 13
81 eluznn0 11251 . . . . . . . . . . . . 13
8278, 80, 81sylancr 676 . . . . . . . . . . . 12
8370, 82, 69vdwmc 15007 . . . . . . . . . . 11 MonoAP AP
8440ad2antrr 740 . . . . . . . . . . . . . . . 16 AP
8580adantr 472 . . . . . . . . . . . . . . . 16 AP
86 simpllr 777 . . . . . . . . . . . . . . . 16 AP
87 simplr 770 . . . . . . . . . . . . . . . 16 AP
88 vex 3034 . . . . . . . . . . . . . . . 16
89 simprll 780 . . . . . . . . . . . . . . . 16 AP
90 simprlr 781 . . . . . . . . . . . . . . . 16 AP
91 simprr 774 . . . . . . . . . . . . . . . 16 AP AP
9284, 85, 86, 87, 88, 89, 90, 91, 68vdwlem8 15017 . . . . . . . . . . . . . . 15 AP PolyAP
9392orcd 399 . . . . . . . . . . . . . 14 AP PolyAP MonoAP
9493expr 626 . . . . . . . . . . . . 13 AP PolyAP MonoAP
9594rexlimdvva 2878 . . . . . . . . . . . 12 AP PolyAP MonoAP
9695exlimdv 1787 . . . . . . . . . . 11 AP PolyAP MonoAP
9783, 96sylbid 223 . . . . . . . . . 10 MonoAP PolyAP MonoAP
9877, 97syld 44 . . . . . . . . 9 MonoAP PolyAP MonoAP
9944, 98syldan 478 . . . . . . . 8 MonoAP PolyAP MonoAP
10099ralrimdva 2812 . . . . . . 7 MonoAP PolyAP MonoAP
101 oveq2 6316 . . . . . . . . . 10
102101oveq2d 6324 . . . . . . . . 9
103102raleqdv 2979 . . . . . . . 8 PolyAP MonoAP PolyAP MonoAP
104103rspcev 3136 . . . . . . 7 PolyAP MonoAP PolyAP MonoAP
10539, 100, 104syl6an 554 . . . . . 6 MonoAP PolyAP MonoAP
10635, 105syl5bi 225 . . . . 5 MonoAP PolyAP MonoAP
107106rexlimdva 2871 . . . 4 MonoAP PolyAP MonoAP
10833, 107mpd 15 . . 3 PolyAP MonoAP
109 breq2 4399 . . . . . . . . . 10 PolyAP PolyAP
110 breq2 4399 . . . . . . . . . 10 MonoAP MonoAP
111109, 110orbi12d 724 . . . . . . . . 9 PolyAP MonoAP PolyAP MonoAP
112111cbvralv 3005 . . . . . . . 8 PolyAP MonoAP PolyAP MonoAP
11330raleqdv 2979 . . . . . . . 8 PolyAP MonoAP PolyAP MonoAP
114112, 113syl5bb 265 . . . . . . 7 PolyAP MonoAP PolyAP MonoAP
115114cbvrexv 3006 . . . . . 6 PolyAP MonoAP PolyAP MonoAP
11622ad2antrr 740 . . . . . . . . . 10 PolyAP MonoAP
117 fzfi 12223 . . . . . . . . . 10
118 mapfi 7888 . . . . . . . . . 10
119116, 117, 118sylancl 675 . . . . . . . . 9 PolyAP MonoAP
12023ad2antrr 740 . . . . . . . . 9 PolyAP MonoAP MonoAP
121 oveq2 6316 . . . . . . . . . . . . . 14
122121oveq2d 6324 . . . . . . . . . . . . 13
123122raleqdv 2979 . . . . . . . . . . . 12 MonoAP MonoAP
124123cbvrexv 3006 . . . . . . . . . . 11 MonoAP MonoAP
125 oveq1 6315 . . . . . . . . . . . . 13
126125raleqdv 2979 . . . . . . . . . . . 12 MonoAP MonoAP
127126rexbidv 2892 . . . . . . . . . . 11 MonoAP MonoAP
128124, 127syl5bb 265 . . . . . . . . . 10 MonoAP MonoAP
129128rspcv 3132 . . . . . . . . 9 MonoAP MonoAP
130119, 120, 129sylc 61 . . . . . . . 8 PolyAP MonoAP MonoAP
131 simprll 780 . . . . . . . . . . 11 PolyAP MonoAP MonoAP
132 simprrl 782 . . . . . . . . . . 11 PolyAP MonoAP MonoAP
133 nnmulcl 10654 . . . . . . . . . . . . 13
13436, 133mpan 684 . . . . . . . . . . . 12
135 nnmulcl 10654 . . . . . . . . . . . 12
136134, 135sylan2 482 . . . . . . . . . . 11
137131, 132, 136syl2anc 673 . . . . . . . . . 10 PolyAP MonoAP MonoAP
138 simp1l 1054 . . . . . . . . . . . . . 14 PolyAP MonoAP MonoAP
139138, 22syl 17 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP
140138, 79syl 17 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP
141138, 23syl 17 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP MonoAP
142 simp1r 1055 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP
143 simp2ll 1097 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP
144 simp2lr 1098 . . . . . . . . . . . . . 14 PolyAP MonoAP MonoAP PolyAP MonoAP
145 breq2 4399 . . . . . . . . . . . . . . . 16 PolyAP PolyAP
146 breq2 4399 . . . . . . . . . . . . . . . 16 MonoAP MonoAP
147145, 146orbi12d 724 . . . . . . . . . . . . . . 15 PolyAP MonoAP PolyAP MonoAP
148147cbvralv 3005 . . . . . . . . . . . . . 14 PolyAP MonoAP PolyAP MonoAP
149144, 148sylib 201 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP PolyAP MonoAP
150 simp2rl 1099 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP
151 simp2rr 1100 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP MonoAP
152 simp3 1032 . . . . . . . . . . . . . 14 PolyAP MonoAP MonoAP
153 ovex 6336 . . . . . . . . . . . . . . 15
154 elmapg 7503 . . . . . . . . . . . . . . 15
155139, 153, 154sylancl 675 . . . . . . . . . . . . . 14 PolyAP MonoAP MonoAP
156152, 155mpbid 215 . . . . . . . . . . . . 13 PolyAP MonoAP MonoAP
157 oveq1 6315 . . . . . . . . . . . . . . . . 17
158157fveq2d 5883 . . . . . . . . . . . . . . . 16
159158cbvmptv 4488 . . . . . . . . . . . . . . 15
160 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20
161160oveq1d 6323 . . . . . . . . . . . . . . . . . . 19
162161oveq2d 6324 . . . . . . . . . . . . . . . . . 18
163162oveq2d 6324 . . . . . . . . . . . . . . . . 17
164163fveq2d 5883 . . . . . . . . . . . . . . . 16
165164mpteq2dv 4483 . . . . . . . . . . . . . . 15
166159, 165syl5eq 2517 . . . . . . . . . . . . . 14
167166cbvmptv 4488 . . . . . . . . . . . . 13
168139, 140, 141, 142, 143, 149, 150, 151, 156, 167vdwlem9 15018 . . . . . . . . . . . 12 PolyAP MonoAP MonoAP PolyAP MonoAP
1691683expia 1233 . . . . . . . . . . 11 PolyAP MonoAP MonoAP PolyAP MonoAP
170169ralrimiv 2808 . . . . . . . . . 10 PolyAP MonoAP MonoAP PolyAP MonoAP
171 oveq2 6316 . . . . . . . . . . . . . 14
172171oveq2d 6324 . . . . . . . . . . . . 13
173172raleqdv 2979 . . . . . . . . . . . 12 PolyAP MonoAP PolyAP MonoAP
174 breq2 4399 . . . . . . . . . . . . . 14 PolyAP PolyAP
175 breq2 4399 . . . . . . . . . . . . . 14 MonoAP MonoAP
176174, 175orbi12d 724 . . . . . . . . . . . . 13 PolyAP MonoAP PolyAP MonoAP
177176cbvralv 3005 . . . . . . . . . . . 12 PolyAP MonoAP PolyAP MonoAP
178173, 177syl6bb 269 . . . . . . . . . . 11 PolyAP MonoAP PolyAP MonoAP
179178rspcev 3136 . . . . . . . . . 10 PolyAP MonoAP PolyAP MonoAP
180137, 170, 179syl2anc 673 . . . . . . . . 9 PolyAP MonoAP MonoAP PolyAP MonoAP
181180anassrs 660 . . . . . . . 8 PolyAP MonoAP MonoAP PolyAP MonoAP
182130, 181rexlimddv 2875 . . . . . . 7 PolyAP MonoAP PolyAP MonoAP
183182rexlimdvaa 2872 . . . . . 6 PolyAP MonoAP PolyAP MonoAP
184115, 183syl5bi 225 . . . . 5 PolyAP MonoAP PolyAP MonoAP
185184expcom 442 . . . 4 PolyAP MonoAP PolyAP MonoAP
186185a2d 28 . . 3 PolyAP MonoAP PolyAP MonoAP
1876, 11, 16, 21, 108, 186nnind 10649 . 2 PolyAP MonoAP
1881, 187mpcom 36 1 PolyAP MonoAP
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904  wral 2756  wrex 2757  cvv 3031   wss 3390  csn 3959  cop 3965   class class class wbr 4395   cmpt 4454  ccnv 4838  cima 4842  wf 5585  cfv 5589  (class class class)co 6308   cmap 7490  cfn 7587  c1 9558   caddc 9560   cmul 9562   cle 9694   cmin 9880  cn 10631  c2 10681  cn0 10893  cz 10961  cuz 11182  cfz 11810  APcvdwa 14994   MonoAP cvdwm 14995   PolyAP cvdwp 14996 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-fz 11811  df-hash 12554  df-vdwap 14997  df-vdwmc 14998  df-vdwpc 14999 This theorem is referenced by:  vdwlem11  15020
 Copyright terms: Public domain W3C validator