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

Theorem vdwlem6 13281
 Description: Lemma for vdw 13289. (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 AP
vdwlem6.b
vdwlem6.e
vdwlem6.s AP
vdwlem6.j
vdwlem6.r
vdwlem6.t
vdwlem6.p
Assertion
Ref Expression
vdwlem6 PolyAP MonoAP
Distinct variable groups:   ,,   ,,,,   ,,,,   ,,,   ,,   ,,,,   ,,,   ,,,,   ,,,   ,,,,   ,,,   ,,,,   ,,,,   ,,   ,,
Allowed substitution hints:   (,)   ()   (,)   ()   (,)   (,,,)   ()   ()   (,)

Proof of Theorem vdwlem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5682 . . . . . . 7
2 vdwlem6.j . . . . . . 7
31, 2fnmpti 5513 . . . . . 6
4 fvelrnb 5713 . . . . . 6
53, 4ax-mp 8 . . . . 5
6 vdwlem4.r . . . . . . . 8
76adantr 452 . . . . . . 7
8 vdwlem7.k . . . . . . . . 9
9 eluz2b2 10480 . . . . . . . . . 10
109simplbi 447 . . . . . . . . 9
118, 10syl 16 . . . . . . . 8
1211adantr 452 . . . . . . 7
13 vdwlem3.w . . . . . . . 8
1413adantr 452 . . . . . . 7
15 vdwlem7.g . . . . . . . 8
1615adantr 452 . . . . . . 7
17 vdwlem6.b . . . . . . . 8
1817adantr 452 . . . . . . 7
19 vdwlem7.m . . . . . . . 8
2019adantr 452 . . . . . . 7
21 vdwlem6.e . . . . . . . 8
2221adantr 452 . . . . . . 7
23 vdwlem6.s . . . . . . . 8 AP
2423adantr 452 . . . . . . 7 AP
25 simprl 733 . . . . . . 7
26 simprr 734 . . . . . . . 8
27 fveq2 5668 . . . . . . . . . . . 12
2827oveq2d 6036 . . . . . . . . . . 11
2928fveq2d 5672 . . . . . . . . . 10
30 fvex 5682 . . . . . . . . . 10
3129, 2, 30fvmpt 5745 . . . . . . . . 9
3225, 31syl 16 . . . . . . . 8
3326, 32eqtr3d 2421 . . . . . . 7
347, 12, 14, 16, 18, 20, 22, 24, 25, 33vdwlem1 13276 . . . . . 6 MonoAP
3534rexlimdvaa 2774 . . . . 5 MonoAP
365, 35syl5bi 209 . . . 4 MonoAP
3736imp 419 . . 3 MonoAP
3837olcd 383 . 2 PolyAP MonoAP
39 vdwlem3.v . . . . . . 7
40 vdwlem4.h . . . . . . 7
41 vdwlem4.f . . . . . . 7
42 vdwlem7.a . . . . . . 7
43 vdwlem7.d . . . . . . 7
44 vdwlem7.s . . . . . . 7 AP
45 vdwlem6.r . . . . . . 7
46 vdwlem6.t . . . . . . 7
47 vdwlem6.p . . . . . . 7
4839, 13, 6, 40, 41, 19, 15, 8, 42, 43, 44, 17, 21, 23, 2, 45, 46, 47vdwlem5 13280 . . . . . 6
4948adantr 452 . . . . 5
50 0nn0 10168 . . . . . . . . . 10
5150a1i 11 . . . . . . . . 9
52 nnuz 10453 . . . . . . . . . . . . . . . . 17
5319, 52syl6eleq 2477 . . . . . . . . . . . . . . . 16
5453adantr 452 . . . . . . . . . . . . . . 15
55 elfzp1 11029 . . . . . . . . . . . . . . 15
5654, 55syl 16 . . . . . . . . . . . . . 14
5756biimpa 471 . . . . . . . . . . . . 13
5857ord 367 . . . . . . . . . . . 12
5958con1d 118 . . . . . . . . . . 11
6059imp 419 . . . . . . . . . 10
6121ad2antrr 707 . . . . . . . . . . . 12
6261ffvelrnda 5809 . . . . . . . . . . 11
6362nnnn0d 10206 . . . . . . . . . 10
6460, 63syldan 457 . . . . . . . . 9
6551, 64ifclda 3709 . . . . . . . 8
6613, 43nnmulcld 9979 . . . . . . . . 9
6766ad2antrr 707 . . . . . . . 8
68 nn0nnaddcl 10184 . . . . . . . 8
6965, 67, 68syl2anc 643 . . . . . . 7
7069, 47fmptd 5832 . . . . . 6
71 nnex 9938 . . . . . . 7
72 ovex 6045 . . . . . . 7
7371, 72elmap 6978 . . . . . 6
7470, 73sylibr 204 . . . . 5
75 elfzp1 11029 . . . . . . . . . 10
7653, 75syl 16 . . . . . . . . 9
7717adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
7877nncnd 9948 . . . . . . . . . . . . . . . . . . . . . 22
7978adantr 452 . . . . . . . . . . . . . . . . . . . . 21
8021ffvelrnda 5809 . . . . . . . . . . . . . . . . . . . . . . 23
8180nncnd 9948 . . . . . . . . . . . . . . . . . . . . . 22
8281adantr 452 . . . . . . . . . . . . . . . . . . . . 21
8379, 82addcld 9040 . . . . . . . . . . . . . . . . . . . 20
84 nnm1nn0 10193 . . . . . . . . . . . . . . . . . . . . . . . . 25
8542, 84syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
86 nn0nnaddcl 10184 . . . . . . . . . . . . . . . . . . . . . . . 24
8785, 39, 86syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
8813, 87nnmulcld 9979 . . . . . . . . . . . . . . . . . . . . . 22
8988nncnd 9948 . . . . . . . . . . . . . . . . . . . . 21
9089ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
91 elfznn0 11015 . . . . . . . . . . . . . . . . . . . . . . . 24
9291adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
9392nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . 22
9493adantlr 696 . . . . . . . . . . . . . . . . . . . . 21
9594, 82mulcld 9041 . . . . . . . . . . . . . . . . . . . 20
9666nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . 24
9796adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
9892, 97nn0mulcld 10211 . . . . . . . . . . . . . . . . . . . . . 22
9998nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . 21
10099adantlr 696 . . . . . . . . . . . . . . . . . . . 20
10183, 90, 95, 100add4d 9221 . . . . . . . . . . . . . . . . . . 19
10266nncnd 9948 . . . . . . . . . . . . . . . . . . . . . 22
103102ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
10494, 82, 103adddid 9045 . . . . . . . . . . . . . . . . . . . 20
105104oveq2d 6036 . . . . . . . . . . . . . . . . . . 19
10613nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . 24
107106adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
10887nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . 24
109108adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
11043nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . 25
111110adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24
11293, 111mulcld 9041 . . . . . . . . . . . . . . . . . . . . . . 23
113107, 109, 112adddid 9045 . . . . . . . . . . . . . . . . . . . . . 22
11442nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
115114adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
116 ax-1cn 8981 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
118115, 112, 117addsubd 9364 . . . . . . . . . . . . . . . . . . . . . . . . 25
119118oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . 24
12085nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121120adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
12239nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123122adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
124121, 112, 123add32d 9220 . . . . . . . . . . . . . . . . . . . . . . . 24
125119, 124eqtrd 2419 . . . . . . . . . . . . . . . . . . . . . . 23
126125oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22
12793, 107, 111mul12d 9207 . . . . . . . . . . . . . . . . . . . . . . 23
128127oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22
129113, 126, 1283eqtr4d 2429 . . . . . . . . . . . . . . . . . . . . 21
130129adantlr 696 . . . . . . . . . . . . . . . . . . . 20
131130oveq2d 6036 . . . . . . . . . . . . . . . . . . 19
132101, 105, 1313eqtr4d 2429 . . . . . . . . . . . . . . . . . 18
13339ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
13413ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
13544adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23 AP
136 eqid 2387 . . . . . . . . . . . . . . . . . . . . . . . . 25
137 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138137oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
139138eqeq2d 2398 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140139rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . . 25
141136, 140mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . 24
14211nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . . 26
143 vdwapval 13268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 AP
144142, 42, 43, 143syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25 AP
145144biimpar 472 . . . . . . . . . . . . . . . . . . . . . . . 24 AP
146141, 145sylan2 461 . . . . . . . . . . . . . . . . . . . . . . 23 AP
147135, 146sseldd 3292 . . . . . . . . . . . . . . . . . . . . . 22
14839, 13, 6, 40, 41vdwlem4 13279 . . . . . . . . . . . . . . . . . . . . . . . . 25
149 ffn 5531 . . . . . . . . . . . . . . . . . . . . . . . . 25
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
151 fniniseg 5790 . . . . . . . . . . . . . . . . . . . . . . . 24
152150, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
153152biimpa 471 . . . . . . . . . . . . . . . . . . . . . 22
154147, 153syldan 457 . . . . . . . . . . . . . . . . . . . . 21
155154simpld 446 . . . . . . . . . . . . . . . . . . . 20
156155adantlr 696 . . . . . . . . . . . . . . . . . . 19
15723r19.21bi 2747 . . . . . . . . . . . . . . . . . . . . . . 23 AP
158157adantr 452 . . . . . . . . . . . . . . . . . . . . . 22 AP
159 eqid 2387 . . . . . . . . . . . . . . . . . . . . . . . 24
160 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
161160oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . 26
162161eqeq2d 2398 . . . . . . . . . . . . . . . . . . . . . . . . 25
163162rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . 24
164159, 163mpan2 653 . . . . . . . . . . . . . . . . . . . . . . 23
16511adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166165nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . 25
16777, 80nnaddcld 9978 . . . . . . . . . . . . . . . . . . . . . . . . 25
168 vdwapval 13268 . . . . . . . . . . . . . . . . . . . . . . . . 25 AP
169166, 167, 80, 168syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24 AP
170169biimpar 472 . . . . . . . . . . . . . . . . . . . . . . 23 AP
171164, 170sylan2 461 . . . . . . . . . . . . . . . . . . . . . 22 AP
172158, 171sseldd 3292 . . . . . . . . . . . . . . . . . . . . 21
173 ffn 5531 . . . . . . . . . . . . . . . . . . . . . . . . 25
17415, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
175174adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
176 fniniseg 5790 . . . . . . . . . . . . . . . . . . . . . . 23
177175, 176syl 16 . . . . . . . . . . . . . . . . . . . . . 22
178177biimpa 471 . . . . . . . . . . . . . . . . . . . . 21
179172, 178syldan 457 . . . . . . . . . . . . . . . . . . . 20
180179simpld 446 . . . . . . . . . . . . . . . . . . 19
181133, 134, 156, 180vdwlem3 13278 . . . . . . . . . . . . . . . . . 18
182132, 181eqeltrd 2461 . . . . . . . . . . . . . . . . 17
183 oveq1 6027 . . . . . . . . . . . . . . . . . . . . 21
184183fveq2d 5672 . . . . . . . . . . . . . . . . . . . 20
185 eqid 2387 . . . . . . . . . . . . . . . . . . . 20
186 fvex 5682 . . . . . . . . . . . . . . . . . . . 20
187184, 185, 186fvmpt 5745 . . . . . . . . . . . . . . . . . . 19
188180, 187syl 16 . . . . . . . . . . . . . . . . . 18
189179simprd 450 . . . . . . . . . . . . . . . . . . 19
190154simprd 450 . . . . . . . . . . . . . . . . . . . . . 22
191 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
192191oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
193192oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
194193oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . 26
195194fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . . . . 25
196195mpteq2dv 4237 . . . . . . . . . . . . . . . . . . . . . . . 24
197 ovex 6045 . . . . . . . . . . . . . . . . . . . . . . . . 25
198197mptex 5905 . . . . . . . . . . . . . . . . . . . . . . . 24
199196, 41, 198fvmpt 5745 . . . . . . . . . . . . . . . . . . . . . . 23
200155, 199syl 16 . . . . . . . . . . . . . . . . . . . . . 22
201190, 200eqtr3d 2421 . . . . . . . . . . . . . . . . . . . . 21
202201adantlr 696 . . . . . . . . . . . . . . . . . . . 20
203202fveq1d 5670 . . . . . . . . . . . . . . . . . . 19
204189, 203eqtr3d 2421 . . . . . . . . . . . . . . . . . 18
205132fveq2d 5672 . . . . . . . . . . . . . . . . . 18
206188, 204, 2053eqtr4rd 2430 . . . . . . . . . . . . . . . . 17
207182, 206jca 519 . . . . . . . . . . . . . . . 16
208 eleq1 2447 . . . . . . . . . . . . . . . . 17
209 fveq2 5668 . . . . . . . . . . . . . . . . . 18
210209eqeq1d 2395 . . . . . . . . . . . . . . . . 17
211208, 210anbi12d 692 . . . . . . . . . . . . . . . 16
212207, 211syl5ibrcom 214 . . . . . . . . . . . . . . 15
213212rexlimdva 2773 . . . . . . . . . . . . . 14
21488adantr 452 . . . . . . . . . . . . . . . 16
215167, 214nnaddcld 9978 . . . . . . . . . . . . . . 15
21666adantr 452 . . . . . . . . . . . . . . . 16
21780, 216nnaddcld 9978 . . . . . . . . . . . . . . 15
218 vdwapval 13268 . . . . . . . . . . . . . . 15 AP
219166, 215, 217, 218syl3anc 1184 . . . . . . . . . . . . . 14 AP
220 ffn 5531 . . . . . . . . . . . . . . . . 17
22140, 220syl 16 . . . . . . . . . . . . . . . 16
222221adantr 452 . . . . . . . . . . . . . . 15
223 fniniseg 5790 . . . . . . . . . . . . . . 15
224222, 223syl 16 . . . . . . . . . . . . . 14
225213, 219, 2243imtr4d 260 . . . . . . . . . . . . 13 AP
226225ssrdv 3297 . . . . . . . . . . . 12 AP
227 ssun1 3453 . . . . . . . . . . . . . . . . . . 19
228 fzsuc 11028 . . . . . . . . . . . . . . . . . . . 20
22953, 228syl 16 . . . . . . . . . . . . . . . . . . 19
230227, 229syl5sseqr 3340 . . . . . . . . . . . . . . . . . 18
231230sselda 3291 . . . . . . . . . . . . . . . . 17
232 eqeq1 2393 . . . . . . . . . . . . . . . . . . . 20
233 fveq2 5668 . . . . . . . . . . . . . . . . . . . 20
234232, 233ifbieq2d 3702 . . . . . . . . . . . . . . . . . . 19
235234oveq1d 6035 . . . . . . . . . . . . . . . . . 18
236 ovex 6045 . . . . . . . . . . . . . . . . . 18
237235, 47, 236fvmpt 5745 . . . . . . . . . . . . . . . . 17
238231, 237syl 16 . . . . . . . . . . . . . . . 16
239 elfzle2 10993 . . . . . . . . . . . . . . . . . . 19
24019nnred 9947 . . . . . . . . . . . . . . . . . . . . . . 23
241240ltp1d 9873 . . . . . . . . . . . . . . . . . . . . . 22
242 peano2re 9171 . . . . . . . . . . . . . . . . . . . . . . . 24
243240, 242syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
244240, 243ltnled 9152 . . . . . . . . . . . . . . . . . . . . . 22
245241, 244mpbid 202 . . . . . . . . . . . . . . . . . . . . 21
246 breq1 4156 . . . . . . . . . . . . . . . . . . . . . 22
247246notbid 286 . . . . . . . . . . . . . . . . . . . . 21
248245, 247syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . 20
249248con2d 109 . . . . . . . . . . . . . . . . . . 19
250239, 249syl5 30 . . . . . . . . . . . . . . . . . 18
251250imp 419 . . . . . . . . . . . . . . . . 17
252 iffalse 3689 . . . . . . . . . . . . . . . . . 18
253252oveq1d 6035 . . . . . . . . . . . . . . . . 17
254251, 253syl 16 . . . . . . . . . . . . . . . 16
255238, 254eqtrd 2419 . . . . . . . . . . . . . . 15
256255oveq2d 6036 . . . . . . . . . . . . . 14
25748nncnd 9948 . . . . . . . . . . . . . . . 16
258257adantr 452 . . . . . . . . . . . . . . 15
259102adantr 452 . . . . . . . . . . . . . . 15
260258, 81, 259add12d 9219 . . . . . . . . . . . . . 14
26146oveq1i 6030 . . . . . . . . . . . . . . . . . 18
26217nncnd 9948 . . . . . . . . . . . . . . . . . . . 20
263122, 110subcld 9343 . . . . . . . . . . . . . . . . . . . . . . 23
264114, 263addcld 9040 . . . . . . . . . . . . . . . . . . . . . 22
265 subcl 9237 . . . . . . . . . . . . . . . . . . . . . 22
266264, 116, 265sylancl 644 . . . . . . . . . . . . . . . . . . . . 21
267106, 266mulcld 9041 . . . . . . . . . . . . . . . . . . . 20
268262, 267, 102addassd 9043 . . . . . . . . . . . . . . . . . . 19
269106, 266, 110adddid 9045 . . . . . . . . . . . . . . . . . . . . 21
270114, 263, 110addassd 9043 . . . . . . . . . . . . . . . . . . . . . . . . 25
271122, 110npcand 9347 . . . . . . . . . . . . . . . . . . . . . . . . . 26
272271oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . 25
273270, 272eqtrd 2419 . . . . . . . . . . . . . . . . . . . . . . . 24
274273oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . 23
275116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
276264, 110, 275addsubd 9364 . . . . . . . . . . . . . . . . . . . . . . 23
277114, 122, 275addsubd 9364 . . . . . . . . . . . . . . . . . . . . . . 23
278274, 276, 2773eqtr3d 2427 . . . . . . . . . . . . . . . . . . . . . 22
279278oveq2d 6036 . . . . . . . . . . . . . . . . . . . . 21
280269, 279eqtr3d 2421 . . . . . . . . . . . . . . . . . . . 20
281280oveq2d 6036 . . . . . . . . . . . . . . . . . . 19
282268, 281eqtrd 2419 . . . . . . . . . . . . . . . . . 18
283261, 282syl5eq 2431 . . . . . . . . . . . . . . . . 17
284283oveq2d 6036 . . . . . . . . . . . . . . . 16
285284adantr 452 . . . . . . . . . . . . . . 15
28689adantr 452 . . . . . . . . . . . . . . . 16
28781, 78, 286addassd 9043 . . . . . . . . . . . . . . 15
28881, 78addcomd 9200 . . . . . . . . . . . . . . . 16
289288oveq1d 6035 . . . . . . . . . . . . . . 15
290285, 287, 2893eqtr2d 2425 . . . . . . . . . . . . . 14
291256, 260, 2903eqtrd 2423 . . . . . . . . . . . . 13
292291, 255oveq12d 6038 . . . . . . . . . . . 12 AP AP
293 cnvimass 5164 . . . . . . . . . . . . . . . . . . 19
294 fdm 5535 . . . . . . . . . . . . . . . . . . . 20
29515, 294syl 16 . . . . . . . . . . . . . . . . . . 19
296293, 295syl5sseq 3339 . . . . . . . . . . . . . . . . . 18
297296adantr 452 . . . . . . . . . . . . . . . . 17
298 vdwapid1 13270 . . . . . . . . . . . . . . . . . . 19 AP
299165, 167, 80, 298syl3anc 1184 . . . . . . . . . . . . . . . . . 18 AP
300157, 299sseldd 3292 . . . . . . . . . . . . . . . . 17
301297, 300sseldd 3292 . . . . . . . . . . . . . . . 16
302 oveq1 6027 . . . . . . . . . . . . . . . . . 18
303302fveq2d 5672 . . . . . . . . . . . . . . . . 17
304 eqid 2387 . . . . . . . . . . . . . . . . 17
305 fvex 5682 . . . . . . . . . . . . . . . . 17
306303, 304, 305fvmpt 5745 . . . . . . . . . . . . . . . 16
307301, 306syl 16 . . . . . . . . . . . . . . 15
308 vdwapid1 13270 . . . . . . . . . . . . . . . . . . . . . 22 AP
30911, 42, 43, 308syl3anc 1184 . . . . . . . . . . . . . . . . . . . . 21 AP
31044, 309sseldd 3292 . . . . . . . . . . . . . . . . . . . 20
311 fniniseg 5790 . . . . . . . . . . . . . . . . . . . . 21
312150, 311syl 16 . . . . . . . . . . . . . . . . . . . 20
313310, 312mpbid 202 . . . . . . . . . . . . . . . . . . 19
314313simprd 450 . . . . . . . . . . . . . . . . . 18
315313simpld 446 . . . . . . . . . . . . . . . . . . 19
316 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . 25
317316oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . 24
318317oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . 23
319318oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22
320319fveq2d 5672 . . . . . . . . . . . . . . . . . . . . 21
321320mpteq2dv 4237 . . . . . . . . . . . . . . . . . . . 20
322197mptex 5905 . . . . . . . . . . . . . . . . . . . 20
323321, 41, 322fvmpt 5745 . . . . . . . . . . . . . . . . . . 19
324315, 323syl 16 . . . . . . . . . . . . . . . . . 18
325314, 324eqtr3d 2421 . . . . . . . . . . . . . . . . 17
326325fveq1d 5670 . . . . . . . . . . . . . . . 16
327326adantr 452 . . . . . . . . . . . . . . 15
328291fveq2d 5672 . . . . . . . . . . . . . . 15
329307, 327, 3283eqtr4rd 2430 . . . . . . . . . . . . . 14
330329sneqd 3770 . . . . . . . . . . . . 13
331330imaeq2d 5143 . . . . . . . . . . . 12
332226, 292, 3313sstr4d 3334 . . . . . . . . . . 11 AP
333332ex 424 . . . . . . . . . 10 AP
334262adantr 452 . . . . . . . . . . . . . . . . . . . 20
33589adantr 452 . . . . . . . . . . . . . . . . . . . 20
336334, 335, 99addassd 9043 . . . . . . . . . . . . . . . . . . 19
337129oveq2d 6036 . . . . . . . . . . . . . . . . . . 19
338336, 337eqtr4d 2422 . . . . . . . . . . . . . . . . . 18
33939adantr 452 . . . . . . . . . . . . . . . . . . 19
34013adantr 452 . . . . . . . . . . . . . . . . . . 19
341 eluzfz1 10996 . . . . . . . . . . . . . . . . . . . . . . . . 25
34253, 341syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
343 ne0i 3577 . . . . . . . . . . . . . . . . . . . . . . . 24
344342, 343syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
345 elfzuz3 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
346301, 345syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
34717nnzd 10306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
348 uzid 10432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
349347, 348syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
350349adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
35180nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
352 uzaddcl 10465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
353350, 351, 352syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
354 uztrn 10434 . . . . . . . . . . . . . . . . . . . . . . . . . 26
355346, 353, 354syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
356 eluzle 10430 . . . . . . . . . . . . . . . . . . . . . . . . 25
357355, 356syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
358357ralrimiva 2732 . . . . . . . . . . . . . . . . . . . . . . 23
359 r19.2z 3660 . . . . . . . . . . . . . . . . . . . . . . 23
360344, 358, 359syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
361 idd 22 . . . . . . . . . . . . . . . . . . . . . . 23
362361rexlimiv 2767 . . . . . . . . . . . . . . . . . . . . . 22
363360, 362syl 16 . . . . . . . . . . . . . . . . . . . . 21
36413nnzd 10306 . . . . . . . . . . . . . . . . . . . . . 22
365 fznn 11045 . . . . . . . . . . . . . . . . . . . . . 22
366364, 365syl 16 . . . . . . . . . . . . . . . . . . . . 21
36717, 363, 366mpbir2and 889 . . . . . . . . . . . . . . . . . . . 20
368367adantr 452 . . . . . . . . . . . . . . . . . . 19
369339, 340, 155, 368