Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . 6
β’ (π = 0 β (π΄βπ) = (π΄β0)) |
2 | 1 | mpteq2dv 5251 |
. . . . 5
β’ (π = 0 β (π₯ β (β€ βm π) β¦ (π΄βπ)) = (π₯ β (β€ βm π) β¦ (π΄β0))) |
3 | 2 | eleq1d 2819 |
. . . 4
β’ (π = 0 β ((π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄β0)) β (mzPolyβπ))) |
4 | 3 | imbi2d 341 |
. . 3
β’ (π = 0 β (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β ((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄β0)) β (mzPolyβπ)))) |
5 | | oveq2 7417 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
6 | 5 | mpteq2dv 5251 |
. . . . 5
β’ (π = π β (π₯ β (β€ βm π) β¦ (π΄βπ)) = (π₯ β (β€ βm π) β¦ (π΄βπ))) |
7 | 6 | eleq1d 2819 |
. . . 4
β’ (π = π β ((π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ))) |
8 | 7 | imbi2d 341 |
. . 3
β’ (π = π β (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ)) β ((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ)))) |
9 | | oveq2 7417 |
. . . . . 6
β’ (π = (π + 1) β (π΄βπ) = (π΄β(π + 1))) |
10 | 9 | mpteq2dv 5251 |
. . . . 5
β’ (π = (π + 1) β (π₯ β (β€ βm π) β¦ (π΄βπ)) = (π₯ β (β€ βm π) β¦ (π΄β(π + 1)))) |
11 | 10 | eleq1d 2819 |
. . . 4
β’ (π = (π + 1) β ((π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄β(π + 1))) β (mzPolyβπ))) |
12 | 11 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ)) β ((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄β(π + 1))) β (mzPolyβπ)))) |
13 | | oveq2 7417 |
. . . . . 6
β’ (π = π· β (π΄βπ) = (π΄βπ·)) |
14 | 13 | mpteq2dv 5251 |
. . . . 5
β’ (π = π· β (π₯ β (β€ βm π) β¦ (π΄βπ)) = (π₯ β (β€ βm π) β¦ (π΄βπ·))) |
15 | 14 | eleq1d 2819 |
. . . 4
β’ (π = π· β ((π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ·)) β (mzPolyβπ))) |
16 | 15 | imbi2d 341 |
. . 3
β’ (π = π· β (((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ)) β ((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄βπ·)) β (mzPolyβπ)))) |
17 | | mzpf 41474 |
. . . . . . 7
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€) |
18 | | zsscn 12566 |
. . . . . . 7
β’ β€
β β |
19 | | fss 6735 |
. . . . . . 7
β’ (((π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€ β§ β€ β
β) β (π₯ β
(β€ βm π) β¦ π΄):(β€ βm π)βΆβ) |
20 | 17, 18, 19 | sylancl 587 |
. . . . . 6
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ) |
21 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β (β€
βm π)
β¦ π΄) = (π₯ β (β€
βm π)
β¦ π΄) |
22 | 21 | fmpt 7110 |
. . . . . 6
β’
(βπ₯ β
(β€ βm π)π΄ β β β (π₯ β (β€ βm π) β¦ π΄):(β€ βm π)βΆβ) |
23 | 20, 22 | sylibr 233 |
. . . . 5
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
βπ₯ β (β€
βm π)π΄ β
β) |
24 | | nfra1 3282 |
. . . . . 6
β’
β²π₯βπ₯ β (β€ βm π)π΄ β β |
25 | | rspa 3246 |
. . . . . . 7
β’
((βπ₯ β
(β€ βm π)π΄ β β β§ π₯ β (β€ βm π)) β π΄ β β) |
26 | 25 | exp0d 14105 |
. . . . . 6
β’
((βπ₯ β
(β€ βm π)π΄ β β β§ π₯ β (β€ βm π)) β (π΄β0) = 1) |
27 | 24, 26 | mpteq2da 5247 |
. . . . 5
β’
(βπ₯ β
(β€ βm π)π΄ β β β (π₯ β (β€ βm π) β¦ (π΄β0)) = (π₯ β (β€ βm π) β¦ 1)) |
28 | 23, 27 | syl 17 |
. . . 4
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (π΄β0)) =
(π₯ β (β€
βm π)
β¦ 1)) |
29 | | elfvex 6930 |
. . . . 5
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
π β
V) |
30 | | 1z 12592 |
. . . . 5
β’ 1 β
β€ |
31 | | mzpconstmpt 41478 |
. . . . 5
β’ ((π β V β§ 1 β
β€) β (π₯ β
(β€ βm π) β¦ 1) β (mzPolyβπ)) |
32 | 29, 30, 31 | sylancl 587 |
. . . 4
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ 1) β (mzPolyβπ)) |
33 | 28, 32 | eqeltrd 2834 |
. . 3
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (π΄β0)) β
(mzPolyβπ)) |
34 | 23 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β βπ₯ β (β€
βm π)π΄ β
β) |
35 | | simp1 1137 |
. . . . . . 7
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β π β β0) |
36 | | nfv 1918 |
. . . . . . . . 9
β’
β²π₯ π β
β0 |
37 | 24, 36 | nfan 1903 |
. . . . . . . 8
β’
β²π₯(βπ₯ β (β€ βm π)π΄ β β β§ π β β0) |
38 | 25 | adantlr 714 |
. . . . . . . . 9
β’
(((βπ₯ β
(β€ βm π)π΄ β β β§ π β β0) β§ π₯ β (β€
βm π))
β π΄ β
β) |
39 | | simplr 768 |
. . . . . . . . 9
β’
(((βπ₯ β
(β€ βm π)π΄ β β β§ π β β0) β§ π₯ β (β€
βm π))
β π β
β0) |
40 | 38, 39 | expp1d 14112 |
. . . . . . . 8
β’
(((βπ₯ β
(β€ βm π)π΄ β β β§ π β β0) β§ π₯ β (β€
βm π))
β (π΄β(π + 1)) = ((π΄βπ) Β· π΄)) |
41 | 37, 40 | mpteq2da 5247 |
. . . . . . 7
β’
((βπ₯ β
(β€ βm π)π΄ β β β§ π β β0) β (π₯ β (β€
βm π)
β¦ (π΄β(π + 1))) = (π₯ β (β€ βm π) β¦ ((π΄βπ) Β· π΄))) |
42 | 34, 35, 41 | syl2anc 585 |
. . . . . 6
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (π΄β(π + 1))) = (π₯ β (β€ βm π) β¦ ((π΄βπ) Β· π΄))) |
43 | | simp3 1139 |
. . . . . . 7
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (π΄βπ)) β (mzPolyβπ)) |
44 | | simp2 1138 |
. . . . . . 7
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ)) |
45 | | mzpmulmpt 41480 |
. . . . . . 7
β’ (((π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ ((π΄βπ) Β· π΄)) β (mzPolyβπ)) |
46 | 43, 44, 45 | syl2anc 585 |
. . . . . 6
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ ((π΄βπ) Β· π΄)) β (mzPolyβπ)) |
47 | 42, 46 | eqeltrd 2834 |
. . . . 5
β’ ((π β β0
β§ (π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (π΄β(π + 1))) β (mzPolyβπ)) |
48 | 47 | 3exp 1120 |
. . . 4
β’ (π β β0
β ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
((π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄β(π + 1))) β (mzPolyβπ)))) |
49 | 48 | a2d 29 |
. . 3
β’ (π β β0
β (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (π΄βπ)) β (mzPolyβπ)) β ((π₯ β (β€ βm π) β¦ π΄) β (mzPolyβπ) β (π₯ β (β€ βm π) β¦ (π΄β(π + 1))) β (mzPolyβπ)))) |
50 | 4, 8, 12, 16, 33, 49 | nn0ind 12657 |
. 2
β’ (π· β β0
β ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (π΄βπ·)) β (mzPolyβπ))) |
51 | 50 | impcom 409 |
1
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
π· β
β0) β (π₯ β (β€ βm π) β¦ (π΄βπ·)) β (mzPolyβπ)) |