Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. 2
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β π β
β0) |
2 | | simp2 1137 |
. . 3
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β πΎ β (β€β₯βπ)) |
3 | | simp3 1138 |
. . . 4
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β π β (mzPolyβ(1...πΎ))) |
4 | | eqidd 2733 |
. . . 4
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
5 | | fveq1 6890 |
. . . . . . . . 9
β’ (π = π β (πβπ’) = (πβπ’)) |
6 | 5 | eqeq1d 2734 |
. . . . . . . 8
β’ (π = π β ((πβπ’) = 0 β (πβπ’) = 0)) |
7 | 6 | anbi2d 629 |
. . . . . . 7
β’ (π = π β ((π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β (π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0))) |
8 | 7 | rexbidv 3178 |
. . . . . 6
β’ (π = π β (βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0))) |
9 | 8 | abbidv 2801 |
. . . . 5
β’ (π = π β {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
10 | 9 | rspceeqv 3633 |
. . . 4
β’ ((π β (mzPolyβ(1...πΎ)) β§ {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) β βπ β (mzPolyβ(1...πΎ)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
11 | 3, 4, 10 | syl2anc 584 |
. . 3
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β βπ β (mzPolyβ(1...πΎ)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
12 | | oveq2 7419 |
. . . . . 6
β’ (π = πΎ β (1...π) = (1...πΎ)) |
13 | 12 | fveq2d 6895 |
. . . . 5
β’ (π = πΎ β (mzPolyβ(1...π)) = (mzPolyβ(1...πΎ))) |
14 | 12 | oveq2d 7427 |
. . . . . . . 8
β’ (π = πΎ β (β0
βm (1...π))
= (β0 βm (1...πΎ))) |
15 | 14 | rexeqdv 3326 |
. . . . . . 7
β’ (π = πΎ β (βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0) β βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0))) |
16 | 15 | abbidv 2801 |
. . . . . 6
β’ (π = πΎ β {π‘ β£ βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
17 | 16 | eqeq2d 2743 |
. . . . 5
β’ (π = πΎ β ({π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
18 | 13, 17 | rexeqbidv 3343 |
. . . 4
β’ (π = πΎ β (βπ β (mzPolyβ(1...π)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β βπ β (mzPolyβ(1...πΎ)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
19 | 18 | rspcev 3612 |
. . 3
β’ ((πΎ β
(β€β₯βπ) β§ βπ β (mzPolyβ(1...πΎ)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) β βπ β (β€β₯βπ)βπ β (mzPolyβ(1...π)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
20 | 2, 11, 19 | syl2anc 584 |
. 2
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β βπ β (β€β₯βπ)βπ β (mzPolyβ(1...π)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)}) |
21 | | eldiophb 41797 |
. 2
β’ ({π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ) β (π β β0 β§
βπ β
(β€β₯βπ)βπ β (mzPolyβ(1...π)){π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} = {π‘ β£ βπ’ β (β0
βm (1...π))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) |
22 | 1, 20, 21 | sylanbrc 583 |
1
β’ ((π β β0
β§ πΎ β
(β€β₯βπ) β§ π β (mzPolyβ(1...πΎ))) β {π‘ β£ βπ’ β (β0
βm (1...πΎ))(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) |