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

Theorem imasdsf1olem 21466
 Description: Lemma for imasdsf1o 21467. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)
Hypotheses
Ref Expression
imasdsf1o.u s
imasdsf1o.v
imasdsf1o.f
imasdsf1o.r
imasdsf1o.e
imasdsf1o.d
imasdsf1o.m
imasdsf1o.x
imasdsf1o.y
imasdsf1o.w s
imasdsf1o.s
imasdsf1o.t g
Assertion
Ref Expression
imasdsf1olem
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,   ,,,,   ,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)   (,,,)   (,,)   (,,,)   (,,,)   ()   (,,,)   (,,,)

Proof of Theorem imasdsf1olem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasdsf1o.u . . . 4 s
2 imasdsf1o.v . . . 4
3 imasdsf1o.f . . . . 5
4 f1ofo 5835 . . . . 5
53, 4syl 17 . . . 4
6 imasdsf1o.r . . . 4
7 eqid 2471 . . . 4
8 imasdsf1o.d . . . 4
9 f1of 5828 . . . . . 6
103, 9syl 17 . . . . 5
11 imasdsf1o.x . . . . 5
1210, 11ffvelrnd 6038 . . . 4
13 imasdsf1o.y . . . . 5
1410, 13ffvelrnd 6038 . . . 4
15 imasdsf1o.s . . . 4
16 imasdsf1o.e . . . 4
171, 2, 5, 6, 7, 8, 12, 14, 15, 16imasdsval2 15495 . . 3 inf g
18 imasdsf1o.t . . . 4 g
1918infeq1i 8012 . . 3 inf inf g
2017, 19syl6eqr 2523 . 2 inf
21 xrsbas 19061 . . . . . . . . . . . 12
22 xrsadd 19062 . . . . . . . . . . . 12
23 imasdsf1o.w . . . . . . . . . . . 12 s
24 xrsex 19060 . . . . . . . . . . . . 13
2524a1i 11 . . . . . . . . . . . 12
26 fzfid 12224 . . . . . . . . . . . 12
27 difss 3549 . . . . . . . . . . . . 13
2827a1i 11 . . . . . . . . . . . 12
29 imasdsf1o.m . . . . . . . . . . . . . . . 16
30 xmetf 21422 . . . . . . . . . . . . . . . 16
31 ffn 5739 . . . . . . . . . . . . . . . 16
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15
33 xmetcl 21424 . . . . . . . . . . . . . . . . . . 19
34 xmetge0 21437 . . . . . . . . . . . . . . . . . . . 20
35 ge0nemnf 11491 . . . . . . . . . . . . . . . . . . . 20
3633, 34, 35syl2anc 673 . . . . . . . . . . . . . . . . . . 19
37 eldifsn 4088 . . . . . . . . . . . . . . . . . . 19
3833, 36, 37sylanbrc 677 . . . . . . . . . . . . . . . . . 18
39383expb 1232 . . . . . . . . . . . . . . . . 17
4029, 39sylan 479 . . . . . . . . . . . . . . . 16
4140ralrimivva 2814 . . . . . . . . . . . . . . 15
42 ffnov 6419 . . . . . . . . . . . . . . 15
4332, 41, 42sylanbrc 677 . . . . . . . . . . . . . 14
4443ad2antrr 740 . . . . . . . . . . . . 13
45 ssrab2 3500 . . . . . . . . . . . . . . . . 17
4615, 45eqsstri 3448 . . . . . . . . . . . . . . . 16
4746a1i 11 . . . . . . . . . . . . . . 15
4847sselda 3418 . . . . . . . . . . . . . 14
49 elmapi 7511 . . . . . . . . . . . . . 14
5048, 49syl 17 . . . . . . . . . . . . 13
51 fco 5751 . . . . . . . . . . . . 13
5244, 50, 51syl2anc 673 . . . . . . . . . . . 12
53 0re 9661 . . . . . . . . . . . . 13
54 rexr 9704 . . . . . . . . . . . . . 14
55 renemnf 9707 . . . . . . . . . . . . . 14
56 eldifsn 4088 . . . . . . . . . . . . . 14
5754, 55, 56sylanbrc 677 . . . . . . . . . . . . 13
5853, 57mp1i 13 . . . . . . . . . . . 12
59 xaddid2 11557 . . . . . . . . . . . . . 14
60 xaddid1 11556 . . . . . . . . . . . . . 14
6159, 60jca 541 . . . . . . . . . . . . 13
6261adantl 473 . . . . . . . . . . . 12
6321, 22, 23, 25, 26, 28, 52, 58, 62gsumress 16597 . . . . . . . . . . 11 g g
6423, 21ressbas2 15258 . . . . . . . . . . . . 13
6527, 64ax-mp 5 . . . . . . . . . . . 12
6623xrs10 19084 . . . . . . . . . . . 12
6723xrs1cmn 19085 . . . . . . . . . . . . 13 CMnd
6867a1i 11 . . . . . . . . . . . 12 CMnd
69 c0ex 9655 . . . . . . . . . . . . . 14
7069a1i 11 . . . . . . . . . . . . 13
7152, 26, 70fdmfifsupp 7911 . . . . . . . . . . . 12 finSupp
7265, 66, 68, 26, 52, 71gsumcl 17627 . . . . . . . . . . 11 g
7363, 72eqeltrd 2549 . . . . . . . . . 10 g
7473eldifad 3402 . . . . . . . . 9 g
75 eqid 2471 . . . . . . . . 9 g g
7674, 75fmptd 6061 . . . . . . . 8 g
77 frn 5747 . . . . . . . 8 g g
7876, 77syl 17 . . . . . . 7 g
7978ralrimiva 2809 . . . . . 6 g
80 iunss 4310 . . . . . 6 g g
8179, 80sylibr 217 . . . . 5 g
8218, 81syl5eqss 3462 . . . 4
83 infxrcl 11644 . . . 4 inf
8482, 83syl 17 . . 3 inf
85 xmetcl 21424 . . . 4
8629, 11, 13, 85syl3anc 1292 . . 3
87 1nn 10642 . . . . . . 7
88 1ex 9656 . . . . . . . . . . . 12
89 opex 4664 . . . . . . . . . . . 12
9088, 89f1osn 5866 . . . . . . . . . . 11
91 f1of 5828 . . . . . . . . . . 11
9290, 91ax-mp 5 . . . . . . . . . 10
93 opelxpi 4871 . . . . . . . . . . . 12
9411, 13, 93syl2anc 673 . . . . . . . . . . 11
9594snssd 4108 . . . . . . . . . 10
96 fss 5749 . . . . . . . . . 10
9792, 95, 96sylancr 676 . . . . . . . . 9
9829elfvexd 5907 . . . . . . . . . . 11
99 xpexg 6612 . . . . . . . . . . 11
10098, 98, 99syl2anc 673 . . . . . . . . . 10
101 snex 4641 . . . . . . . . . 10
102 elmapg 7503 . . . . . . . . . 10
103100, 101, 102sylancl 675 . . . . . . . . 9
10497, 103mpbird 240 . . . . . . . 8
105 op1stg 6824 . . . . . . . . . . 11
10611, 13, 105syl2anc 673 . . . . . . . . . 10
107106fveq2d 5883 . . . . . . . . 9
108 op2ndg 6825 . . . . . . . . . . 11
10911, 13, 108syl2anc 673 . . . . . . . . . 10
110109fveq2d 5883 . . . . . . . . 9
111107, 110jca 541 . . . . . . . 8
11224a1i 11 . . . . . . . . . 10
113 snfi 7668 . . . . . . . . . . 11
114113a1i 11 . . . . . . . . . 10
11527a1i 11 . . . . . . . . . 10
116 xmetge0 21437 . . . . . . . . . . . . . . 15
11729, 11, 13, 116syl3anc 1292 . . . . . . . . . . . . . 14
118 ge0nemnf 11491 . . . . . . . . . . . . . 14
11986, 117, 118syl2anc 673 . . . . . . . . . . . . 13
120 eldifsn 4088 . . . . . . . . . . . . 13
12186, 119, 120sylanbrc 677 . . . . . . . . . . . 12
122 fconst6g 5785 . . . . . . . . . . . 12
123121, 122syl 17 . . . . . . . . . . 11
124 fcoconst 6076 . . . . . . . . . . . . . 14
12532, 94, 124syl2anc 673 . . . . . . . . . . . . 13
12688, 89xpsn 6082 . . . . . . . . . . . . . 14
127126coeq2i 5000 . . . . . . . . . . . . 13
128 df-ov 6311 . . . . . . . . . . . . . . . 16
129128eqcomi 2480 . . . . . . . . . . . . . . 15
130129sneqi 3970 . . . . . . . . . . . . . 14
131130xpeq2i 4860 . . . . . . . . . . . . 13
132125, 127, 1313eqtr3g 2528 . . . . . . . . . . . 12
133132feq1d 5724 . . . . . . . . . . 11
134123, 133mpbird 240 . . . . . . . . . 10
13553, 57mp1i 13 . . . . . . . . . 10
13661adantl 473 . . . . . . . . . 10
13721, 22, 23, 112, 114, 115, 134, 135, 136gsumress 16597 . . . . . . . . 9 g g
138 fconstmpt 4883 . . . . . . . . . . 11
139132, 138syl6eq 2521 . . . . . . . . . 10
140139oveq2d 6324 . . . . . . . . 9 g g
141 cmnmnd 17523 . . . . . . . . . . 11 CMnd
14267, 141mp1i 13 . . . . . . . . . 10
14387a1i 11 . . . . . . . . . 10
144 eqidd 2472 . . . . . . . . . . 11
14565, 144gsumsn 17665 . . . . . . . . . 10 g
146142, 143, 121, 145syl3anc 1292 . . . . . . . . 9 g
147137, 140, 1463eqtrrd 2510 . . . . . . . 8 g
148 fveq1 5878 . . . . . . . . . . . . . . 15
14988, 89fvsn 6113 . . . . . . . . . . . . . . 15
150148, 149syl6eq 2521 . . . . . . . . . . . . . 14
151150fveq2d 5883 . . . . . . . . . . . . 13
152151fveq2d 5883 . . . . . . . . . . . 12
153152eqeq1d 2473 . . . . . . . . . . 11
154150fveq2d 5883 . . . . . . . . . . . . 13
155154fveq2d 5883 . . . . . . . . . . . 12
156155eqeq1d 2473 . . . . . . . . . . 11
157153, 156anbi12d 725 . . . . . . . . . 10
158 coeq2 4998 . . . . . . . . . . . 12
159158oveq2d 6324 . . . . . . . . . . 11 g g
160159eqeq2d 2481 . . . . . . . . . 10 g g
161157, 160anbi12d 725 . . . . . . . . 9 g g
162161rspcev 3136 . . . . . . . 8 g g
163104, 111, 147, 162syl12anc 1290 . . . . . . 7 g
164 ovex 6336 . . . . . . . . . 10
16575elrnmpt 5087 . . . . . . . . . 10 g g
166164, 165ax-mp 5 . . . . . . . . 9 g g
16715rexeqi 2978 . . . . . . . . . . 11 g g
168 fveq1 5878 . . . . . . . . . . . . . . . 16
169168fveq2d 5883 . . . . . . . . . . . . . . 15
170169fveq2d 5883 . . . . . . . . . . . . . 14
171170eqeq1d 2473 . . . . . . . . . . . . 13
172 fveq1 5878 . . . . . . . . . . . . . . . 16
173172fveq2d 5883 . . . . . . . . . . . . . . 15
174173fveq2d 5883 . . . . . . . . . . . . . 14
175174eqeq1d 2473 . . . . . . . . . . . . 13
176 fveq1 5878 . . . . . . . . . . . . . . . . 17
177176fveq2d 5883 . . . . . . . . . . . . . . . 16
178177fveq2d 5883 . . . . . . . . . . . . . . 15
179 fveq1 5878 . . . . . . . . . . . . . . . . 17
180179fveq2d 5883 . . . . . . . . . . . . . . . 16
181180fveq2d 5883 . . . . . . . . . . . . . . 15
182178, 181eqeq12d 2486 . . . . . . . . . . . . . 14
183182ralbidv 2829 . . . . . . . . . . . . 13
184171, 175, 1833anbi123d 1365 . . . . . . . . . . . 12
185184rexrab 3190 . . . . . . . . . . 11 g g
186167, 185bitri 257 . . . . . . . . . 10 g g
187 oveq2 6316 . . . . . . . . . . . . 13
188 1z 10991 . . . . . . . . . . . . . 14
189 fzsn 11866 . . . . . . . . . . . . . 14
190188, 189ax-mp 5 . . . . . . . . . . . . 13
191187, 190syl6eq 2521 . . . . . . . . . . . 12
192191oveq2d 6324 . . . . . . . . . . 11
193 df-3an 1009 . . . . . . . . . . . . 13
194 ral0 3865 . . . . . . . . . . . . . . . 16
195 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20
196 1m1e0 10700 . . . . . . . . . . . . . . . . . . . 20
197195, 196syl6eq 2521 . . . . . . . . . . . . . . . . . . 19
198197oveq2d 6324 . . . . . . . . . . . . . . . . . 18
199 fz10 11846 . . . . . . . . . . . . . . . . . 18
200198, 199syl6eq 2521 . . . . . . . . . . . . . . . . 17
201200raleqdv 2979 . . . . . . . . . . . . . . . 16
202194, 201mpbiri 241 . . . . . . . . . . . . . . 15
203202biantrud 515 . . . . . . . . . . . . . 14
204 fveq2 5879 . . . . . . . . . . . . . . . . . 18
205204fveq2d 5883 . . . . . . . . . . . . . . . . 17
206205fveq2d 5883 . . . . . . . . . . . . . . . 16
207206eqeq1d 2473 . . . . . . . . . . . . . . 15
208207anbi2d 718 . . . . . . . . . . . . . 14
209203, 208bitr3d 263 . . . . . . . . . . . . 13
210193, 209syl5bb 265 . . . . . . . . . . . 12
211210anbi1d 719 . . . . . . . . . . 11 g g
212192, 211rexeqbidv 2988 . . . . . . . . . 10 g g
213186, 212syl5bb 265 . . . . . . . . 9 g g
214166, 213syl5bb 265 . . . . . . . 8 g g
215214rspcev 3136 . . . . . . 7 g g
21687, 163, 215sylancr 676 . . . . . 6 g
217 eliun 4274 . . . . . 6 g g
218216, 217sylibr 217 . . . . 5 g
219218, 18syl6eleqr 2560 . . . 4
220 infxrlb 11645 . . . 4 inf
22182, 219, 220syl2anc 673 . . 3 inf
22218eleq2i 2541 . . . . . . 7 g
223 eliun 4274 . . . . . . 7 g g
224222, 223bitri 257 . . . . . 6 g
225 vex 3034 . . . . . . . . 9
22675elrnmpt 5087 . . . . . . . . 9 g g
227225, 226ax-mp 5 . . . . . . . 8 g g
228184, 15elrab2 3186 . . . . . . . . . . . . . . . . 17
229228simprbi 471 . . . . . . . . . . . . . . . 16
230229adantl 473 . . . . . . . . . . . . . . 15
231230simp2d 1043 . . . . . . . . . . . . . 14
2323ad2antrr 740 . . . . . . . . . . . . . . . 16
233 f1of1 5827 . . . . . . . . . . . . . . . 16
234232, 233syl 17 . . . . . . . . . . . . . . 15
235 simplr 770 . . . . . . . . . . . . . . . . . 18
236 elfz1end 11855 . . . . . . . . . . . . . . . . . 18
237235, 236sylib 201 . . . . . . . . . . . . . . . . 17
23850, 237ffvelrnd 6038 . . . . . . . . . . . . . . . 16
239 xp2nd 6843 . . . . . . . . . . . . . . . 16
240238, 239syl 17 . . . . . . . . . . . . . . 15
24113ad2antrr 740 . . . . . . . . . . . . . . 15
242 f1fveq 6181 . . . . . . . . . . . . . . 15
243234, 240, 241, 242syl12anc 1290 . . . . . . . . . . . . . 14
244231, 243mpbid 215 . . . . . . . . . . . . 13
245244oveq2d 6324 . . . . . . . . . . . 12
246 eleq1 2537 . . . . . . . . . . . . . . . . 17
247 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
248247fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
249248oveq2d 6324 . . . . . . . . . . . . . . . . . 18
250 oveq2 6316 . . . . . . . . . . . . . . . . . . . . 21
251250, 190syl6eq 2521 . . . . . . . . . . . . . . . . . . . 20
252251reseq2d 5111 . . . . . . . . . . . . . . . . . . 19
253252oveq2d 6324 . . . . . . . . . . . . . . . . . 18 g g
254249, 253breq12d 4408 . . . . . . . . . . . . . . . . 17 g g
255246, 254imbi12d 327 . . . . . . . . . . . . . . . 16 g g
256255imbi2d 323 . . . . . . . . . . . . . . 15 g g
257 eleq1 2537 . . . . . . . . . . . . . . . . 17
258 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
259258fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
260259oveq2d 6324 . . . . . . . . . . . . . . . . . 18
261 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
262261reseq2d 5111 . . . . . . . . . . . . . . . . . . 19
263262oveq2d 6324 . . . . . . . . . . . . . . . . . 18 g g
264260, 263breq12d 4408 . . . . . . . . . . . . . . . . 17 g g
265257, 264imbi12d 327 . . . . . . . . . . . . . . . 16 g g
266265imbi2d 323 . . . . . . . . . . . . . . 15 g g
267 eleq1 2537 . . . . . . . . . . . . . . . . 17
268 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
269268fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
270269oveq2d 6324 . . . . . . . . . . . . . . . . . 18
271 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
272271reseq2d 5111 . . . . . . . . . . . . . . . . . . 19
273272oveq2d 6324 . . . . . . . . . . . . . . . . . 18 g g
274270, 273breq12d 4408 . . . . . . . . . . . . . . . . 17 g g
275267, 274imbi12d 327 . . . . . . . . . . . . . . . 16 g g
276275imbi2d 323 . . . . . . . . . . . . . . 15 g g
277 eleq1 2537 . . . . . . . . . . . . . . . . 17
278 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
279278fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
280279oveq2d 6324 . . . . . . . . . . . . . . . . . 18
281 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
282281reseq2d 5111 . . . . . . . . . . . . . . . . . . 19
283282oveq2d 6324 . . . . . . . . . . . . . . . . . 18 g g
284280, 283breq12d 4408 . . . . . . . . . . . . . . . . 17 g g
285277, 284imbi12d 327 . . . . . . . . . . . . . . . 16 g g
286285imbi2d 323 . . . . . . . . . . . . . . 15 g g
28729ad2antrr 740 . . . . . . . . . . . . . . . . . . 19
28811ad2antrr 740 . . . . . . . . . . . . . . . . . . 19
289 nnuz 11218 . . . . . . . . . . . . . . . . . . . . . . 23
290235, 289syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . . 22
291 eluzfz1 11832 . . . . . . . . . . . . . . . . . . . . . 22
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21
29350, 292ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . 20
294 xp2nd 6843 . . . . . . . . . . . . . . . . . . . 20
295293, 294syl 17 . . . . . . . . . . . . . . . . . . 19
296 xmetcl 21424 . . . . . . . . . . . . . . . . . . 19
297287, 288, 295, 296syl3anc 1292 . . . . . . . . . . . . . . . . . 18
298 xrleid 11472 . . . . . . . . . . . . . . . . . 18
299297, 298syl 17 . . . . . . . . . . . . . . . . 17
300142ad2antrr 740 . . . . . . . . . . . . . . . . . . 19
30187a1i 11 . . . . . . . . . . . . . . . . . . 19
30244, 293ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19
303 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
304303fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
30565, 304gsumsn 17665 . . . . . . . . . . . . . . . . . . 19 g
306300, 301, 302, 305syl3anc 1292 . . . . . . . . . . . . . . . . . 18 g
307287, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22
308 fcompt 6075 . . . . . . . . . . . . . . . . . . . . . 22
309307, 50, 308syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
310309reseq1d 5110 . . . . . . . . . . . . . . . . . . . 20
311292snssd 4108 . . . . . . . . . . . . . . . . . . . . 21
312311resmptd 5162 . . . . . . . . . . . . . . . . . . . 20
313310, 312eqtrd 2505 . . . . . . . . . . . . . . . . . . 19
314313oveq2d 6324 . . . . . . . . . . . . . . . . . 18 g g
315 df-ov 6311 . . . . . . . . . . . . . . . . . . 19
316 1st2nd2 6849 . . . . . . . . . . . . . . . . . . . . . 22
317293, 316syl 17 . . . . . . . . . . . . . . . . . . . . 21
318230simp1d 1042 . . . . . . . . . . . . . . . . . . . . . . 23
319 xp1st 6842 . . . . . . . . . . . . . . . . . . . . . . . . 25
320293, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
321 f1fveq 6181 . . . . . . . . . . . . . . . . . . . . . . . 24
322234, 320, 288, 321syl12anc 1290 . . . . . . . . . . . . . . . . . . . . . . 23
323318, 322mpbid 215 . . . . . . . . . . . . . . . . . . . . . 22
324323opeq1d 4164 . . . . . . . . . . . . . . . . . . . . 21
325317, 324eqtr2d 2506 . . . . . . . . . . . . . . . . . . . 20
326325fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
327315, 326syl5eq 2517 . . . . . . . . . . . . . . . . . 18
328306, 314, 3273eqtr4d 2515 . . . . . . . . . . . . . . . . 17 g
329299, 328breqtrrd 4422 . . . . . . . . . . . . . . . 16 g
330329a1d 25 . . . . . . . . . . . . . . 15 g
331 simprl 772 . . . . . . . . . . . . . . . . . . . . . 22
332331, 289syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . 21
333 simprr 774 . . . . . . . . . . . . . . . . . . . . 21
334 peano2fzr 11838 . . . . . . . . . . . . . . . . . . . . 21
335332, 333, 334syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
336335expr 626 . . . . . . . . . . . . . . . . . . 19
337336imim1d 77 . . . . . . . . . . . . . . . . . 18 g g
338287adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
339288adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
34050adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
341340, 335ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . 25
342 xp2nd 6843 . . . . . . . . . . . . . . . . . . . . . . . . 25
343341, 342syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
344 xmetcl 21424 . . . . . . . . . . . . . . . . . . . . . . . 24
345338, 339, 343, 344syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . 23
34667a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 CMnd
347 fzfid 12224 . . . . . . . . . . . . . . . . . . . . . . . . 25
34852adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
349 fzsuc 11869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
350332, 349syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
351 elfzuz3 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
352351ad2antll 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
353 fzss2 11864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
354352, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
355350, 354eqsstr3d 3453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
356355unssad 3602 . . . . . . . . . . . . . . . . . . . . . . . . . 26
357348, 356fssresd 5762 . . . . . . . . . . . . . . . . . . . . . . . . 25
35869a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
359357, 347, 358fdmfifsupp 7911 . . . . . . . . . . . . . . . . . . . . . . . . 25 finSupp
36065, 66, 346, 347, 357, 359gsumcl 17627 . . . . . . . . . . . . . . . . . . . . . . . 24 g
361360eldifad 3402 . . . . . . . . . . . . . . . . . . . . . . 23 g
362338, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
363340, 333ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . 24
364362, 363ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23
365 xleadd1a 11564 . . . . . . . . . . . . . . . . . . . . . . . 24 g g g
366365ex 441 . . . . . . . . . . . . . . . . . . . . . . 23 g g g
367345, 361, 364, 366syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22 g g
368 xp2nd 6843 . . . . . . . . . . . . . . . . . . . . . . . . . 26
369363, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
370 xmettri 21444 . . . . . . . . . . . . . . . . . . . . . . . . 25
371338, 339, 369, 343, 370syl13anc 1294 . . . . . . . . . . . . . . . . . . . . . . . 24
372 1st2nd2 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
373363, 372syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
374 nnz 10983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
375374ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
376 eluzp1m1 11206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
377375, 352, 376syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
378 elfzuzb 11820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
379332, 377, 378