Step | Hyp | Ref
| Expression |
1 | | risset 3231 |
. . . . 5
β’ (π΄ β β0
β βπ β
β0 π =
π΄) |
2 | 1 | rabbii 3439 |
. . . 4
β’ {π‘ β (β0
βm (1...π))
β£ π΄ β
β0} = {π‘
β (β0 βm (1...π)) β£ βπ β β0 π = π΄} |
3 | 2 | a1i 11 |
. . 3
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ β β0} = {π‘ β (β0
βm (1...π))
β£ βπ β
β0 π =
π΄}) |
4 | | nfcv 2904 |
. . . 4
β’
β²π‘(β0 βm
(1...π)) |
5 | | nfcv 2904 |
. . . 4
β’
β²π(β0 βm
(1...π)) |
6 | | nfv 1918 |
. . . 4
β’
β²πβπ β β0
π = π΄ |
7 | | nfcv 2904 |
. . . . 5
β’
β²π‘β0 |
8 | | nfcsb1v 3919 |
. . . . . 6
β’
β²π‘β¦π / π‘β¦π΄ |
9 | 8 | nfeq2 2921 |
. . . . 5
β’
β²π‘ π = β¦π / π‘β¦π΄ |
10 | 7, 9 | nfrexw 3311 |
. . . 4
β’
β²π‘βπ β β0
π = β¦π / π‘β¦π΄ |
11 | | csbeq1a 3908 |
. . . . . 6
β’ (π‘ = π β π΄ = β¦π / π‘β¦π΄) |
12 | 11 | eqeq2d 2744 |
. . . . 5
β’ (π‘ = π β (π = π΄ β π = β¦π / π‘β¦π΄)) |
13 | 12 | rexbidv 3179 |
. . . 4
β’ (π‘ = π β (βπ β β0 π = π΄ β βπ β β0 π = β¦π / π‘β¦π΄)) |
14 | 4, 5, 6, 10, 13 | cbvrabw 3468 |
. . 3
β’ {π‘ β (β0
βm (1...π))
β£ βπ β
β0 π =
π΄} = {π β (β0
βm (1...π))
β£ βπ β
β0 π =
β¦π / π‘β¦π΄} |
15 | 3, 14 | eqtrdi 2789 |
. 2
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ β β0} = {π β (β0
βm (1...π))
β£ βπ β
β0 π =
β¦π / π‘β¦π΄}) |
16 | | peano2nn0 12512 |
. . . . 5
β’ (π β β0
β (π + 1) β
β0) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π + 1) β
β0) |
18 | | ovex 7442 |
. . . . 5
β’
(1...(π + 1)) β
V |
19 | | nn0p1nn 12511 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β) |
20 | | elfz1end 13531 |
. . . . . . 7
β’ ((π + 1) β β β
(π + 1) β (1...(π + 1))) |
21 | 19, 20 | sylib 217 |
. . . . . 6
β’ (π β β0
β (π + 1) β
(1...(π +
1))) |
22 | 21 | adantr 482 |
. . . . 5
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π + 1) β
(1...(π +
1))) |
23 | | mzpproj 41475 |
. . . . 5
β’
(((1...(π + 1))
β V β§ (π + 1)
β (1...(π + 1)))
β (π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
24 | 18, 22, 23 | sylancr 588 |
. . . 4
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
25 | | eqid 2733 |
. . . . 5
β’ (π + 1) = (π + 1) |
26 | 25 | rabdiophlem2 41540 |
. . . 4
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΄) β (mzPolyβ(1...(π + 1)))) |
27 | | eqrabdioph 41515 |
. . . 4
β’ (((π + 1) β β0
β§ (π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1))) β§ (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΄) β (mzPolyβ(1...(π + 1)))) β {π β (β0
βm (1...(π
+ 1))) β£ (πβ(π + 1)) = β¦(π βΎ (1...π)) / π‘β¦π΄} β (Diophβ(π + 1))) |
28 | 17, 24, 26, 27 | syl3anc 1372 |
. . 3
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β {π β
(β0 βm (1...(π + 1))) β£ (πβ(π + 1)) = β¦(π βΎ (1...π)) / π‘β¦π΄} β (Diophβ(π + 1))) |
29 | | eqeq1 2737 |
. . . 4
β’ (π = (πβ(π + 1)) β (π = β¦π / π‘β¦π΄ β (πβ(π + 1)) = β¦π / π‘β¦π΄)) |
30 | | csbeq1 3897 |
. . . . 5
β’ (π = (π βΎ (1...π)) β β¦π / π‘β¦π΄ = β¦(π βΎ (1...π)) / π‘β¦π΄) |
31 | 30 | eqeq2d 2744 |
. . . 4
β’ (π = (π βΎ (1...π)) β ((πβ(π + 1)) = β¦π / π‘β¦π΄ β (πβ(π + 1)) = β¦(π βΎ (1...π)) / π‘β¦π΄)) |
32 | 25, 29, 31 | rexrabdioph 41532 |
. . 3
β’ ((π β β0
β§ {π β
(β0 βm (1...(π + 1))) β£ (πβ(π + 1)) = β¦(π βΎ (1...π)) / π‘β¦π΄} β (Diophβ(π + 1))) β {π β (β0
βm (1...π))
β£ βπ β
β0 π =
β¦π / π‘β¦π΄} β (Diophβπ)) |
33 | 28, 32 | syldan 592 |
. 2
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β {π β
(β0 βm (1...π)) β£ βπ β β0 π = β¦π / π‘β¦π΄} β (Diophβπ)) |
34 | 15, 33 | eqeltrd 2834 |
1
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ β β0} β
(Diophβπ)) |