Step | Hyp | Ref
| Expression |
1 | | uneq1 4121 |
. . . . . . . 8
β’ (π‘ = π β (π‘ βͺ π€) = (π βͺ π€)) |
2 | 1 | fveqeq2d 6855 |
. . . . . . 7
β’ (π‘ = π β ((πβ(π‘ βͺ π€)) = 0 β (πβ(π βͺ π€)) = 0)) |
3 | 2 | rexbidv 3176 |
. . . . . 6
β’ (π‘ = π β (βπ€ β (β0
βm π)(πβ(π‘ βͺ π€)) = 0 β βπ€ β (β0
βm π)(πβ(π βͺ π€)) = 0)) |
4 | | uneq2 4122 |
. . . . . . . 8
β’ (π€ = π β (π βͺ π€) = (π βͺ π)) |
5 | 4 | fveqeq2d 6855 |
. . . . . . 7
β’ (π€ = π β ((πβ(π βͺ π€)) = 0 β (πβ(π βͺ π)) = 0)) |
6 | 5 | cbvrexvw 3229 |
. . . . . 6
β’
(βπ€ β
(β0 βm π)(πβ(π βͺ π€)) = 0 β βπ β (β0
βm π)(πβ(π βͺ π)) = 0) |
7 | 3, 6 | bitrdi 287 |
. . . . 5
β’ (π‘ = π β (βπ€ β (β0
βm π)(πβ(π‘ βͺ π€)) = 0 β βπ β (β0
βm π)(πβ(π βͺ π)) = 0)) |
8 | 7 | cbvrabv 3420 |
. . . 4
β’ {π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0} |
9 | | fveq1 6846 |
. . . . . . . 8
β’ (π = π β (πβ(π βͺ π)) = (πβ(π βͺ π))) |
10 | 9 | eqeq1d 2739 |
. . . . . . 7
β’ (π = π β ((πβ(π βͺ π)) = 0 β (πβ(π βͺ π)) = 0)) |
11 | 10 | rexbidv 3176 |
. . . . . 6
β’ (π = π β (βπ β (β0
βm π)(πβ(π βͺ π)) = 0 β βπ β (β0
βm π)(πβ(π βͺ π)) = 0)) |
12 | 11 | rabbidv 3418 |
. . . . 5
β’ (π = π β {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0}) |
13 | 12 | rspceeqv 3600 |
. . . 4
β’ ((π β (mzPolyβ(π βͺ (1...π))) β§ {π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0}) β βπ β (mzPolyβ(π βͺ (1...π))){π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0}) |
14 | 8, 13 | mpan2 690 |
. . 3
β’ (π β (mzPolyβ(π βͺ (1...π))) β βπ β (mzPolyβ(π βͺ (1...π))){π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0}) |
15 | 14 | anim2i 618 |
. 2
β’ ((π β β0
β§ π β
(mzPolyβ(π βͺ
(1...π)))) β (π β β0
β§ βπ β
(mzPolyβ(π βͺ
(1...π))){π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0})) |
16 | | eldioph4b.a |
. . 3
β’ π β V |
17 | | eldioph4b.b |
. . 3
β’ Β¬
π β
Fin |
18 | | eldioph4b.c |
. . 3
β’ (π β© β) =
β
|
19 | 16, 17, 18 | eldioph4b 41163 |
. 2
β’ ({π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} β (Diophβπ) β (π β β0 β§
βπ β
(mzPolyβ(π βͺ
(1...π))){π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} = {π β (β0
βm (1...π))
β£ βπ β
(β0 βm π)(πβ(π βͺ π)) = 0})) |
20 | 15, 19 | sylibr 233 |
1
β’ ((π β β0
β§ π β
(mzPolyβ(π βͺ
(1...π)))) β {π‘ β (β0
βm (1...π))
β£ βπ€ β
(β0 βm π)(πβ(π‘ βͺ π€)) = 0} β (Diophβπ)) |