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

Theorem vdwlem8 15017
 Description: Lemma for vdw 15023. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdwlem8.r
vdwlem8.k
vdwlem8.w
vdwlem8.f
vdwlem8.c
vdwlem8.a
vdwlem8.d
vdwlem8.s AP
vdwlem8.g
Assertion
Ref Expression
vdwlem8 PolyAP
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem vdwlem8
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwlem8.a . . . . . . . . . 10
21nncnd 10647 . . . . . . . . 9
3 vdwlem8.d . . . . . . . . . 10
43nncnd 10647 . . . . . . . . 9
52, 4addcomd 9853 . . . . . . . 8
65oveq2d 6324 . . . . . . 7
7 vdwlem8.w . . . . . . . . 9
87nncnd 10647 . . . . . . . 8
98, 4, 2subsub4d 10036 . . . . . . 7
106, 9eqtr4d 2508 . . . . . 6
1110oveq2d 6324 . . . . 5
128, 4subcld 10005 . . . . . 6
132, 2, 12ppncand 10045 . . . . 5
1411, 13eqtrd 2505 . . . 4
151, 1nnaddcld 10678 . . . . 5
16 vdwlem8.s . . . . . . . 8 AP
17 cnvimass 5194 . . . . . . . . 9
18 fvex 5889 . . . . . . . . . 10
19 vdwlem8.g . . . . . . . . . 10
2018, 19dmmpti 5717 . . . . . . . . 9
2117, 20sseqtri 3450 . . . . . . . 8
2216, 21syl6ss 3430 . . . . . . 7 AP
23 ssun2 3589 . . . . . . . . 9 AP AP
24 vdwlem8.k . . . . . . . . . . 11
25 uz2m1nn 11256 . . . . . . . . . . 11
2624, 25syl 17 . . . . . . . . . 10
271, 3nnaddcld 10678 . . . . . . . . . 10
28 vdwapid1 15004 . . . . . . . . . 10 AP
2926, 27, 3, 28syl3anc 1292 . . . . . . . . 9 AP
3023, 29sseldi 3416 . . . . . . . 8 AP
31 eluz2nn 11221 . . . . . . . . . . . . . 14
3224, 31syl 17 . . . . . . . . . . . . 13
3332nncnd 10647 . . . . . . . . . . . 12
34 ax-1cn 9615 . . . . . . . . . . . 12
35 npcan 9904 . . . . . . . . . . . 12
3633, 34, 35sylancl 675 . . . . . . . . . . 11
3736fveq2d 5883 . . . . . . . . . 10 AP AP
3837oveqd 6325 . . . . . . . . 9 AP AP
3926nnnn0d 10949 . . . . . . . . . 10
40 vdwapun 15003 . . . . . . . . . 10 AP AP
4139, 1, 3, 40syl3anc 1292 . . . . . . . . 9 AP AP
4238, 41eqtr3d 2507 . . . . . . . 8 AP AP
4330, 42eleqtrrd 2552 . . . . . . 7 AP
4422, 43sseldd 3419 . . . . . 6
45 elfzuz3 11823 . . . . . 6
46 uznn0sub 11214 . . . . . 6
4744, 45, 463syl 18 . . . . 5
48 nnnn0addcl 10924 . . . . 5
4915, 47, 48syl2anc 673 . . . 4
5014, 49eqeltrrd 2550 . . 3
51 1nn 10642 . . . . . . . 8
52 f1osng 5867 . . . . . . . 8
5351, 3, 52sylancr 676 . . . . . . 7
54 f1of 5828 . . . . . . 7
5553, 54syl 17 . . . . . 6
563snssd 4108 . . . . . 6
5755, 56fssd 5750 . . . . 5
58 1z 10991 . . . . . . 7
59 fzsn 11866 . . . . . . 7
6058, 59ax-mp 5 . . . . . 6
6160feq2i 5731 . . . . 5
6257, 61sylibr 217 . . . 4
63 nnex 10637 . . . . 5
64 ovex 6336 . . . . 5
6563, 64elmap 7518 . . . 4
6662, 65sylibr 217 . . 3
671, 7nnaddcld 10678 . . . . . . . . . . . . . 14
6867adantr 472 . . . . . . . . . . . . 13
69 elfznn0 11913 . . . . . . . . . . . . . 14
703nnnn0d 10949 . . . . . . . . . . . . . 14
71 nn0mulcl 10930 . . . . . . . . . . . . . 14
7269, 70, 71syl2anr 486 . . . . . . . . . . . . 13
73 nnnn0addcl 10924 . . . . . . . . . . . . 13
7468, 72, 73syl2anc 673 . . . . . . . . . . . 12
75 nnuz 11218 . . . . . . . . . . . 12
7674, 75syl6eleq 2559 . . . . . . . . . . 11
7716adantr 472 . . . . . . . . . . . . . . . 16 AP
78 eqid 2471 . . . . . . . . . . . . . . . . . 18
79 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
8079oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20
8180eqeq2d 2481 . . . . . . . . . . . . . . . . . . 19
8281rspcev 3136 . . . . . . . . . . . . . . . . . 18
8378, 82mpan2 685 . . . . . . . . . . . . . . . . 17
8432nnnn0d 10949 . . . . . . . . . . . . . . . . . . 19
85 vdwapval 15002 . . . . . . . . . . . . . . . . . . 19 AP
8684, 1, 3, 85syl3anc 1292 . . . . . . . . . . . . . . . . . 18 AP
8786biimpar 493 . . . . . . . . . . . . . . . . 17 AP
8883, 87sylan2 482 . . . . . . . . . . . . . . . 16 AP
8977, 88sseldd 3419 . . . . . . . . . . . . . . 15
9018, 19fnmpti 5716 . . . . . . . . . . . . . . . 16
91 fniniseg 6018 . . . . . . . . . . . . . . . 16
9290, 91ax-mp 5 . . . . . . . . . . . . . . 15
9389, 92sylib 201 . . . . . . . . . . . . . 14
9493simpld 466 . . . . . . . . . . . . 13
95 elfzuz3 11823 . . . . . . . . . . . . 13
96 eluzelz 11192 . . . . . . . . . . . . . 14
97 eluzadd 11211 . . . . . . . . . . . . . 14
9896, 97mpdan 681 . . . . . . . . . . . . 13
9994, 95, 983syl 18 . . . . . . . . . . . 12
10082timesd 10878 . . . . . . . . . . . . 13
101100adantr 472 . . . . . . . . . . . 12
1022adantr 472 . . . . . . . . . . . . . 14
1038adantr 472 . . . . . . . . . . . . . 14
10472nn0cnd 10951 . . . . . . . . . . . . . 14
105102, 103, 104add32d 9877 . . . . . . . . . . . . 13
106105fveq2d 5883 . . . . . . . . . . . 12
10799, 101, 1063eltr4d 2564 . . . . . . . . . . 11
108 elfzuzb 11820 . . . . . . . . . . 11
10976, 107, 108sylanbrc 677 . . . . . . . . . 10
110105fveq2d 5883 . . . . . . . . . . 11
111 oveq1 6315 . . . . . . . . . . . . . 14
112111fveq2d 5883 . . . . . . . . . . . . 13
113 fvex 5889 . . . . . . . . . . . . 13
114112, 19, 113fvmpt 5963 . . . . . . . . . . . 12
11594, 114syl 17 . . . . . . . . . . 11
11693simprd 470 . . . . . . . . . . 11
117110, 115, 1163eqtr2d 2511 . . . . . . . . . 10
118109, 117jca 541 . . . . . . . . 9
119 eleq1 2537 . . . . . . . . . 10
120 fveq2 5879 . . . . . . . . . . 11
121120eqeq1d 2473 . . . . . . . . . 10
122119, 121anbi12d 725 . . . . . . . . 9
123118, 122syl5ibrcom 230 . . . . . . . 8
124123rexlimdva 2871 . . . . . . 7
125 vdwapval 15002 . . . . . . . 8 AP
12684, 67, 3, 125syl3anc 1292 . . . . . . 7 AP
127 vdwlem8.f . . . . . . . 8
128 ffn 5739 . . . . . . . 8
129 fniniseg 6018 . . . . . . . 8
130127, 128, 1293syl 18 . . . . . . 7
131124, 126, 1303imtr4d 276 . . . . . 6 AP
132131ssrdv 3424 . . . . 5 AP
133 fvsng 6114 . . . . . . . . 9
13451, 3, 133sylancr 676 . . . . . . . 8
135134oveq2d 6324 . . . . . . 7
1362, 12, 4addassd 9683 . . . . . . 7
1378, 4npcand 10009 . . . . . . . 8
138137oveq2d 6324 . . . . . . 7
139135, 136, 1383eqtrd 2509 . . . . . 6
140139, 134oveq12d 6326 . . . . 5 AP AP
141139fveq2d 5883 . . . . . . . 8
142 vdwapid1 15004 . . . . . . . . . . . . 13 AP
14332, 1, 3, 142syl3anc 1292 . . . . . . . . . . . 12 AP
14416, 143sseldd 3419 . . . . . . . . . . 11
145 fniniseg 6018 . . . . . . . . . . . 12
14690, 145ax-mp 5 . . . . . . . . . . 11
147144, 146sylib 201 . . . . . . . . . 10
148147simpld 466 . . . . . . . . 9
149 oveq1 6315 . . . . . . . . . . 11
150149fveq2d 5883 . . . . . . . . . 10
151 fvex 5889 . . . . . . . . . 10
152150, 19, 151fvmpt 5963 . . . . . . . . 9
153148, 152syl 17 . . . . . . . 8
154147simprd 470 . . . . . . . 8
155141, 153, 1543eqtr2d 2511 . . . . . . 7
156155sneqd 3971 . . . . . 6
157156imaeq2d 5174 . . . . 5
158132, 140, 1573sstr4d 3461 . . . 4 AP
159158ralrimivw 2810 . . 3 AP
160155mpteq2dv 4483 . . . . . . . 8
161 fconstmpt 4883 . . . . . . . 8
162160, 161syl6eqr 2523 . . . . . . 7
163162rneqd 5068 . . . . . 6
164 elfz3 11835 . . . . . . . 8
165 ne0i 3728 . . . . . . . 8
16658, 164, 165mp2b 10 . . . . . . 7
167 rnxp 5273 . . . . . . 7
168166, 167ax-mp 5 . . . . . 6
169163, 168syl6eq 2521 . . . . 5
170169fveq2d 5883 . . . 4
171 vdwlem8.c . . . . 5
172 hashsng 12587 . . . . 5
173171, 172ax-mp 5 . . . 4
174170, 173syl6eq 2521 . . 3
175 oveq1 6315 . . . . . . . 8
176175oveq1d 6323 . . . . . . 7 AP AP
177175fveq2d 5883 . . . . . . . . 9
178177sneqd 3971 . . . . . . . 8
179178imaeq2d 5174 . . . . . . 7
180176, 179sseq12d 3447 . . . . . 6 AP AP
181180ralbidv 2829 . . . . 5 AP AP
182177mpteq2dv 4483 . . . . . . . 8
183182rneqd 5068 . . . . . . 7
184183fveq2d 5883 . . . . . 6
185184eqeq1d 2473 . . . . 5
186181, 185anbi12d 725 . . . 4 AP AP
187 fveq1 5878 . . . . . . . . . 10
188 elfz1eq 11836 . . . . . . . . . . 11
189188fveq2d 5883 . . . . . . . . . 10
190187, 189sylan9eq 2525 . . . . . . . . 9
191190oveq2d 6324 . . . . . . . 8
192191, 190oveq12d 6326 . . . . . . 7 AP AP
193191fveq2d 5883 . . . . . . . . 9
194193sneqd 3971 . . . . . . . 8
195194imaeq2d 5174 . . . . . . 7
196192, 195sseq12d 3447 . . . . . 6 AP AP
197196ralbidva 2828 . . . . 5 AP AP
198193mpteq2dva 4482 . . . . . . . 8
199198rneqd 5068 . . . . . . 7
200199fveq2d 5883 . . . . . 6
201200eqeq1d 2473 . . . . 5
202197, 201anbi12d 725 . . . 4 AP AP
203186, 202rspc2ev 3149 . . 3 AP AP
20450, 66, 159, 174, 203syl112anc 1296 . 2 AP
205 ovex 6336 . . 3
20651a1i 11 . . 3
207 eqid 2471 . . 3
208205, 84, 127, 206, 207vdwpc 15009 . 2 PolyAP AP
209204, 208mpbird 240 1 PolyAP
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757  cvv 3031   cun 3388   wss 3390  c0 3722  csn 3959  cop 3965   class class class wbr 4395   cmpt 4454   cxp 4837  ccnv 4838   cdm 4839   crn 4840  cima 4842   wfn 5584  wf 5585  wf1o 5588  cfv 5589  (class class class)co 6308   cmap 7490  cfn 7587  cc 9555  cc0 9557  c1 9558   caddc 9560   cmul 9562   cmin 9880  cn 10631  c2 10681  cn0 10893  cz 10961  cuz 11182  cfz 11810  chash 12553  APcvdwa 14994   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-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-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  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-fz 11811  df-hash 12554  df-vdwap 14997  df-vdwpc 14999 This theorem is referenced by:  vdwlem10  15019
 Copyright terms: Public domain W3C validator