Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . 5
β’ (π β πΉ β (Polyβπ)) |
2 | | plydiv.g |
. . . . 5
β’ (π β πΊ β (Polyβπ)) |
3 | | plydiv.z |
. . . . 5
β’ (π β πΊ β
0π) |
4 | | eqid 2732 |
. . . . . 6
β’ (πΉ βf β
(πΊ βf
Β· π)) = (πΉ βf β
(πΊ βf
Β· π)) |
5 | 4 | quotval 25804 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) = (β©π β (Polyββ)((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)))) |
6 | 1, 2, 3, 5 | syl3anc 1371 |
. . . 4
β’ (π β (πΉ quot πΊ) = (β©π β (Polyββ)((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)))) |
7 | | plydiv.pl |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) |
8 | | plydiv.tm |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) |
9 | | plydiv.rc |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) |
10 | | plydiv.m1 |
. . . . . . 7
β’ (π β -1 β π) |
11 | 7, 8, 9, 10, 1, 2,
3, 4 | plydivalg 25811 |
. . . . . 6
β’ (π β β!π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) |
12 | | reurex 3380 |
. . . . . 6
β’
(β!π β
(Polyβπ)((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)) β βπ β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (π β βπ β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) |
14 | | addcl 11191 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
15 | 14 | adantl 482 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
16 | | mulcl 11193 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
17 | 16 | adantl 482 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
18 | | reccl 11878 |
. . . . . . 7
β’ ((π₯ β β β§ π₯ β 0) β (1 / π₯) β
β) |
19 | 18 | adantl 482 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ π₯ β 0)) β (1 / π₯) β β) |
20 | | neg1cn 12325 |
. . . . . . 7
β’ -1 β
β |
21 | 20 | a1i 11 |
. . . . . 6
β’ (π β -1 β
β) |
22 | | plyssc 25713 |
. . . . . . 7
β’
(Polyβπ)
β (Polyββ) |
23 | 22, 1 | sselid 3980 |
. . . . . 6
β’ (π β πΉ β
(Polyββ)) |
24 | 22, 2 | sselid 3980 |
. . . . . 6
β’ (π β πΊ β
(Polyββ)) |
25 | 15, 17, 19, 21, 23, 24, 3, 4 | plydivalg 25811 |
. . . . 5
β’ (π β β!π β (Polyββ)((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ))) |
26 | | id 22 |
. . . . . . 7
β’ (((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)) β ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) |
27 | 26 | rgenw 3065 |
. . . . . 6
β’
βπ β
(Polyβπ)(((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)) β ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) |
28 | | riotass2 7395 |
. . . . . 6
β’
((((Polyβπ)
β (Polyββ) β§ βπ β (Polyβπ)(((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)) β ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)))) β§ (βπ β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)) β§ β!π β
(Polyββ)((πΉ
βf β (πΊ βf Β· π)) = 0π β¨
(degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)))) β (β©π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) = (β©π β
(Polyββ)((πΉ
βf β (πΊ βf Β· π)) = 0π β¨
(degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)))) |
29 | 22, 27, 28 | mpanl12 700 |
. . . . 5
β’
((βπ β
(Polyβπ)((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)) β§ β!π β
(Polyββ)((πΉ
βf β (πΊ βf Β· π)) = 0π β¨
(degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) β (β©π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) = (β©π β
(Polyββ)((πΉ
βf β (πΊ βf Β· π)) = 0π β¨
(degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)))) |
30 | 13, 25, 29 | syl2anc 584 |
. . . 4
β’ (π β (β©π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) = (β©π β
(Polyββ)((πΉ
βf β (πΊ βf Β· π)) = 0π β¨
(degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)))) |
31 | 6, 30 | eqtr4d 2775 |
. . 3
β’ (π β (πΉ quot πΊ) = (β©π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)))) |
32 | | riotacl2 7381 |
. . . 4
β’
(β!π β
(Polyβπ)((πΉ βf β
(πΊ βf
Β· π)) =
0π β¨ (degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ)) β (β©π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) β {π β (Polyβπ) β£ ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))}) |
33 | 11, 32 | syl 17 |
. . 3
β’ (π β (β©π β (Polyβπ)((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))) β {π β (Polyβπ) β£ ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))}) |
34 | 31, 33 | eqeltrd 2833 |
. 2
β’ (π β (πΉ quot πΊ) β {π β (Polyβπ) β£ ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))}) |
35 | | oveq2 7416 |
. . . . . . 7
β’ (π = (πΉ quot πΊ) β (πΊ βf Β· π) = (πΊ βf Β· (πΉ quot πΊ))) |
36 | 35 | oveq2d 7424 |
. . . . . 6
β’ (π = (πΉ quot πΊ) β (πΉ βf β (πΊ βf Β·
π)) = (πΉ βf β (πΊ βf Β·
(πΉ quot πΊ)))) |
37 | | quotlem.8 |
. . . . . 6
β’ π
= (πΉ βf β (πΊ βf Β·
(πΉ quot πΊ))) |
38 | 36, 37 | eqtr4di 2790 |
. . . . 5
β’ (π = (πΉ quot πΊ) β (πΉ βf β (πΊ βf Β·
π)) = π
) |
39 | 38 | eqeq1d 2734 |
. . . 4
β’ (π = (πΉ quot πΊ) β ((πΉ βf β (πΊ βf Β·
π)) = 0π
β π
=
0π)) |
40 | 38 | fveq2d 6895 |
. . . . 5
β’ (π = (πΉ quot πΊ) β (degβ(πΉ βf β (πΊ βf Β·
π))) = (degβπ
)) |
41 | 40 | breq1d 5158 |
. . . 4
β’ (π = (πΉ quot πΊ) β ((degβ(πΉ βf β (πΊ βf Β·
π))) < (degβπΊ) β (degβπ
) < (degβπΊ))) |
42 | 39, 41 | orbi12d 917 |
. . 3
β’ (π = (πΉ quot πΊ) β (((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ)) β (π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |
43 | 42 | elrab 3683 |
. 2
β’ ((πΉ quot πΊ) β {π β (Polyβπ) β£ ((πΉ βf β (πΊ βf Β·
π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β· π))) < (degβπΊ))} β ((πΉ quot πΊ) β (Polyβπ) β§ (π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |
44 | 34, 43 | sylib 217 |
1
β’ (π β ((πΉ quot πΊ) β (Polyβπ) β§ (π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |