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

Theorem vdwlem6 14504
Description: Lemma for vdw 14512. (Contributed by Mario Carneiro, 13-Sep-2014.)
Hypotheses
Ref Expression
vdwlem3.v
vdwlem3.w
vdwlem4.r
vdwlem4.h
vdwlem4.f
vdwlem7.m
vdwlem7.g
vdwlem7.k
vdwlem7.a
vdwlem7.d
vdwlem7.s
vdwlem6.b
vdwlem6.e
vdwlem6.s
vdwlem6.j
vdwlem6.r
vdwlem6.t
vdwlem6.p
Assertion
Ref Expression
vdwlem6
Distinct variable groups:   , ,   , , , ,   , , , ,   ,J, ,   P, ,   , , , ,   , , ,   , , , ,   , , ,   ,M, , ,   , , ,   , , , ,   , , , ,   , ,   , ,

Proof of Theorem vdwlem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5881 . . . . . . 7
2 vdwlem6.j . . . . . . 7
31, 2fnmpti 5714 . . . . . 6
4 fvelrnb 5920 . . . . . 6
53, 4ax-mp 5 . . . . 5
6 vdwlem4.r . . . . . . . 8
76adantr 465 . . . . . . 7
8 vdwlem7.k . . . . . . . . 9
9 eluz2nn 11148 . . . . . . . . 9
108, 9syl 16 . . . . . . . 8
1110adantr 465 . . . . . . 7
12 vdwlem3.w . . . . . . . 8
1312adantr 465 . . . . . . 7
14 vdwlem7.g . . . . . . . 8
1514adantr 465 . . . . . . 7
16 vdwlem6.b . . . . . . . 8
1716adantr 465 . . . . . . 7
18 vdwlem7.m . . . . . . . 8
1918adantr 465 . . . . . . 7
20 vdwlem6.e . . . . . . . 8
2120adantr 465 . . . . . . 7
22 vdwlem6.s . . . . . . . 8
2322adantr 465 . . . . . . 7
24 simprl 756 . . . . . . 7
25 simprr 757 . . . . . . . 8
26 fveq2 5871 . . . . . . . . . . . 12
2726oveq2d 6312 . . . . . . . . . . 11
2827fveq2d 5875 . . . . . . . . . 10
29 fvex 5881 . . . . . . . . . 10
3028, 2, 29fvmpt 5956 . . . . . . . . 9
3124, 30syl 16 . . . . . . . 8
3225, 31eqtr3d 2500 . . . . . . 7
337, 11, 13, 15, 17, 19, 21, 23, 24, 32vdwlem1 14499 . . . . . 6
3433rexlimdvaa 2950 . . . . 5
355, 34syl5bi 217 . . . 4
3635imp 429 . . 3
3736olcd 393 . 2
38 vdwlem3.v . . . . . . 7
39 vdwlem4.h . . . . . . 7
40 vdwlem4.f . . . . . . 7
41 vdwlem7.a . . . . . . 7
42 vdwlem7.d . . . . . . 7
43 vdwlem7.s . . . . . . 7
44 vdwlem6.r . . . . . . 7
45 vdwlem6.t . . . . . . 7
46 vdwlem6.p . . . . . . 7
4738, 12, 6, 39, 40, 18, 14, 8, 41, 42, 43, 16, 20, 22, 2, 44, 45, 46vdwlem5 14503 . . . . . 6
4847adantr 465 . . . . 5
49 0nn0 10835 . . . . . . . . . 10
5049a1i 11 . . . . . . . . 9
51 nnuz 11145 . . . . . . . . . . . . . . . . 17
5218, 51syl6eleq 2555 . . . . . . . . . . . . . . . 16
5352adantr 465 . . . . . . . . . . . . . . 15
54 elfzp1 11759 . . . . . . . . . . . . . . 15
5553, 54syl 16 . . . . . . . . . . . . . 14
5655biimpa 484 . . . . . . . . . . . . 13
5756ord 377 . . . . . . . . . . . 12
5857con1d 124 . . . . . . . . . . 11
5958imp 429 . . . . . . . . . 10
6020ad2antrr 725 . . . . . . . . . . . 12
6160ffvelrnda 6031 . . . . . . . . . . 11
6261nnnn0d 10877 . . . . . . . . . 10
6359, 62syldan 470 . . . . . . . . 9
6450, 63ifclda 3973 . . . . . . . 8
6512, 42nnmulcld 10608 . . . . . . . . 9
6665ad2antrr 725 . . . . . . . 8
67 nn0nnaddcl 10852 . . . . . . . 8
6864, 66, 67syl2anc 661 . . . . . . 7
6968, 46fmptd 6055 . . . . . 6
70 nnex 10567 . . . . . . 7
71 ovex 6324 . . . . . . 7
7270, 71elmap 7467 . . . . . 6
7369, 72sylibr 212 . . . . 5
74 elfzp1 11759 . . . . . . . . . 10
7552, 74syl 16 . . . . . . . . 9
7616adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
7776nncnd 10577 . . . . . . . . . . . . . . . . . . . . . 22
7877adantr 465 . . . . . . . . . . . . . . . . . . . . 21
7920ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . . . 23
8079nncnd 10577 . . . . . . . . . . . . . . . . . . . . . 22
8180adantr 465 . . . . . . . . . . . . . . . . . . . . 21
8278, 81addcld 9636 . . . . . . . . . . . . . . . . . . . 20
83 nnm1nn0 10862 . . . . . . . . . . . . . . . . . . . . . . . . 25
8441, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
85 nn0nnaddcl 10852 . . . . . . . . . . . . . . . . . . . . . . . 24
8684, 38, 85syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
8712, 86nnmulcld 10608 . . . . . . . . . . . . . . . . . . . . . 22
8887nncnd 10577 . . . . . . . . . . . . . . . . . . . . 21
8988ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
90 elfznn0 11800 . . . . . . . . . . . . . . . . . . . . . . . 24
9190adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
9291nn0cnd 10879 . . . . . . . . . . . . . . . . . . . . . 22
9392adantlr 714 . . . . . . . . . . . . . . . . . . . . 21
9493, 81mulcld 9637 . . . . . . . . . . . . . . . . . . . 20
9565nnnn0d 10877 . . . . . . . . . . . . . . . . . . . . . . . 24
9695adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
9791, 96nn0mulcld 10882 . . . . . . . . . . . . . . . . . . . . . 22
9897nn0cnd 10879 . . . . . . . . . . . . . . . . . . . . 21
9998adantlr 714 . . . . . . . . . . . . . . . . . . . 20
10082, 89, 94, 99add4d 9826 . . . . . . . . . . . . . . . . . . 19
10165nncnd 10577 . . . . . . . . . . . . . . . . . . . . . 22
102101ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
10393, 81, 102adddid 9641 . . . . . . . . . . . . . . . . . . . 20
104103oveq2d 6312 . . . . . . . . . . . . . . . . . . 19
10512nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . 24
106105adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
10786nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . 24
108107adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
10942nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . . 25
110109adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
11192, 110mulcld 9637 . . . . . . . . . . . . . . . . . . . . . . 23
112106, 108, 111adddid 9641 . . . . . . . . . . . . . . . . . . . . . 22
11341nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
114113adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
115 1cnd 9633 . . . . . . . . . . . . . . . . . . . . . . . . . 26
116114, 111, 115addsubd 9975 . . . . . . . . . . . . . . . . . . . . . . . . 25
117116oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . 24
11884nn0cnd 10879 . . . . . . . . . . . . . . . . . . . . . . . . . 26
119118adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
12038nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121120adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
122119, 111, 121add32d 9825 . . . . . . . . . . . . . . . . . . . . . . . 24
123117, 122eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . 23
124123oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . 22
12592, 106, 110mul12d 9810 . . . . . . . . . . . . . . . . . . . . . . 23
126125oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . 22
127112, 124, 1263eqtr4d 2508 . . . . . . . . . . . . . . . . . . . . 21
128127adantlr 714 . . . . . . . . . . . . . . . . . . . 20
129128oveq2d 6312 . . . . . . . . . . . . . . . . . . 19
130100, 104, 1293eqtr4d 2508 . . . . . . . . . . . . . . . . . 18
13138ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
13212ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
13343adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
134 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . 25
135 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136135oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
137136eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . 26
138137rspcev 3210 . . . . . . . . . . . . . . . . . . . . . . . . 25
139134, 138mpan2 671 . . . . . . . . . . . . . . . . . . . . . . . 24
14010nnnn0d 10877 . . . . . . . . . . . . . . . . . . . . . . . . . 26
141 vdwapval 14491 . . . . . . . . . . . . . . . . . . . . . . . . . 26
142140, 41, 42, 141syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
143142biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . 24
144139, 143sylan2 474 . . . . . . . . . . . . . . . . . . . . . . 23
145133, 144sseldd 3504 . . . . . . . . . . . . . . . . . . . . . 22
14638, 12, 6, 39, 40vdwlem4 14502 . . . . . . . . . . . . . . . . . . . . . . . . 25
147 ffn 5736 . . . . . . . . . . . . . . . . . . . . . . . . 25
148146, 147syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
149 fniniseg 6008 . . . . . . . . . . . . . . . . . . . . . . . 24
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
151150biimpa 484 . . . . . . . . . . . . . . . . . . . . . 22
152145, 151syldan 470 . . . . . . . . . . . . . . . . . . . . 21
153152simpld 459 . . . . . . . . . . . . . . . . . . . 20
154153adantlr 714 . . . . . . . . . . . . . . . . . . 19
15522r19.21bi 2826 . . . . . . . . . . . . . . . . . . . . . . 23
156155adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
157 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . 24
158 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
159158oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . 26
160159eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25
161160rspcev 3210 . . . . . . . . . . . . . . . . . . . . . . . 24
162157, 161mpan2 671 . . . . . . . . . . . . . . . . . . . . . . 23
16310adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
164163nnnn0d 10877 . . . . . . . . . . . . . . . . . . . . . . . . 25
16576, 79nnaddcld 10607 . . . . . . . . . . . . . . . . . . . . . . . . 25
166 vdwapval 14491 . . . . . . . . . . . . . . . . . . . . . . . . 25
167164, 165, 79, 166syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24
168167biimpar 485 . . . . . . . . . . . . . . . . . . . . . . 23
169162, 168sylan2 474 . . . . . . . . . . . . . . . . . . . . . 22
170156, 169sseldd 3504 . . . . . . . . . . . . . . . . . . . . 21
171 ffn 5736 . . . . . . . . . . . . . . . . . . . . . . . . 25
17214, 171syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
173172adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
174 fniniseg 6008 . . . . . . . . . . . . . . . . . . . . . . 23
175173, 174syl 16 . . . . . . . . . . . . . . . . . . . . . 22
176175biimpa 484 . . . . . . . . . . . . . . . . . . . . 21
177170, 176syldan 470 . . . . . . . . . . . . . . . . . . . 20
178177simpld 459 . . . . . . . . . . . . . . . . . . 19
179131, 132, 154, 178vdwlem3 14501 . . . . . . . . . . . . . . . . . 18
180130, 179eqeltrd 2545 . . . . . . . . . . . . . . . . 17
181 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
182181fveq2d 5875 . . . . . . . . . . . . . . . . . . . 20
183 eqid 2457 . . . . . . . . . . . . . . . . . . . 20
184 fvex 5881 . . . . . . . . . . . . . . . . . . . 20
185182, 183, 184fvmpt 5956 . . . . . . . . . . . . . . . . . . 19
186178, 185syl 16 . . . . . . . . . . . . . . . . . 18
187177simprd 463 . . . . . . . . . . . . . . . . . . 19
188152simprd 463 . . . . . . . . . . . . . . . . . . . . . 22
189 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
190189oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
191190oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
192191oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . 26
193192fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . 25
194193mpteq2dv 4539 . . . . . . . . . . . . . . . . . . . . . . . 24
195 ovex 6324 . . . . . . . . . . . . . . . . . . . . . . . . 25
196195mptex 6143 . . . . . . . . . . . . . . . . . . . . . . . 24
197194, 40, 196fvmpt 5956 . . . . . . . . . . . . . . . . . . . . . . 23
198153, 197syl 16 . . . . . . . . . . . . . . . . . . . . . 22
199188, 198eqtr3d 2500 . . . . . . . . . . . . . . . . . . . . 21
200199adantlr 714 . . . . . . . . . . . . . . . . . . . 20
201200fveq1d 5873 . . . . . . . . . . . . . . . . . . 19
202187, 201eqtr3d 2500 . . . . . . . . . . . . . . . . . 18
203130fveq2d 5875 . . . . . . . . . . . . . . . . . 18
204186, 202, 2033eqtr4rd 2509 . . . . . . . . . . . . . . . . 17