Step | Hyp | Ref
| Expression |
1 | | dgradd.1 |
. . . 4
β’ π = (degβπΉ) |
2 | | dgradd.2 |
. . . 4
β’ π = (degβπΊ) |
3 | 1, 2 | dgrmul2 25783 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβ(πΉ βf Β· πΊ)) β€ (π + π)) |
4 | 3 | ad2ant2r 746 |
. 2
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(degβ(πΉ
βf Β· πΊ)) β€ (π + π)) |
5 | | plymulcl 25735 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ βf Β· πΊ) β
(Polyββ)) |
6 | 5 | ad2ant2r 746 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β (πΉ βf Β·
πΊ) β
(Polyββ)) |
7 | | dgrcl 25747 |
. . . . . 6
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
8 | 1, 7 | eqeltrid 2838 |
. . . . 5
β’ (πΉ β (Polyβπ) β π β
β0) |
9 | 8 | ad2antrr 725 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β π β
β0) |
10 | | dgrcl 25747 |
. . . . . 6
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
11 | 2, 10 | eqeltrid 2838 |
. . . . 5
β’ (πΊ β (Polyβπ) β π β
β0) |
12 | 11 | ad2antrl 727 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β π β
β0) |
13 | 9, 12 | nn0addcld 12536 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β (π + π) β
β0) |
14 | | eqid 2733 |
. . . . . 6
β’
(coeffβπΉ) =
(coeffβπΉ) |
15 | | eqid 2733 |
. . . . . 6
β’
(coeffβπΊ) =
(coeffβπΊ) |
16 | 14, 15, 1, 2 | coemulhi 25768 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβ(πΉ βf Β· πΊ))β(π + π)) = (((coeffβπΉ)βπ) Β· ((coeffβπΊ)βπ))) |
17 | 16 | ad2ant2r 746 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((coeffβ(πΉ
βf Β· πΊ))β(π + π)) = (((coeffβπΉ)βπ) Β· ((coeffβπΊ)βπ))) |
18 | 14 | coef3 25746 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β (coeffβπΉ):β0βΆβ) |
19 | 18 | ad2antrr 725 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(coeffβπΉ):β0βΆβ) |
20 | 19, 9 | ffvelcdmd 7088 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((coeffβπΉ)βπ) β β) |
21 | 15 | coef3 25746 |
. . . . . . 7
β’ (πΊ β (Polyβπ) β (coeffβπΊ):β0βΆβ) |
22 | 21 | ad2antrl 727 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(coeffβπΊ):β0βΆβ) |
23 | 22, 12 | ffvelcdmd 7088 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((coeffβπΊ)βπ) β β) |
24 | 1, 14 | dgreq0 25779 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β (πΉ = 0π β
((coeffβπΉ)βπ) = 0)) |
25 | 24 | necon3bid 2986 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β (πΉ β 0π β
((coeffβπΉ)βπ) β 0)) |
26 | 25 | biimpa 478 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΉ β 0π) β
((coeffβπΉ)βπ) β 0) |
27 | 26 | adantr 482 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((coeffβπΉ)βπ) β 0) |
28 | 2, 15 | dgreq0 25779 |
. . . . . . . 8
β’ (πΊ β (Polyβπ) β (πΊ = 0π β
((coeffβπΊ)βπ) = 0)) |
29 | 28 | necon3bid 2986 |
. . . . . . 7
β’ (πΊ β (Polyβπ) β (πΊ β 0π β
((coeffβπΊ)βπ) β 0)) |
30 | 29 | biimpa 478 |
. . . . . 6
β’ ((πΊ β (Polyβπ) β§ πΊ β 0π) β
((coeffβπΊ)βπ) β 0) |
31 | 30 | adantl 483 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((coeffβπΊ)βπ) β 0) |
32 | 20, 23, 27, 31 | mulne0d 11866 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(((coeffβπΉ)βπ) Β· ((coeffβπΊ)βπ)) β 0) |
33 | 17, 32 | eqnetrd 3009 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((coeffβ(πΉ
βf Β· πΊ))β(π + π)) β 0) |
34 | | eqid 2733 |
. . . 4
β’
(coeffβ(πΉ
βf Β· πΊ)) = (coeffβ(πΉ βf Β· πΊ)) |
35 | | eqid 2733 |
. . . 4
β’
(degβ(πΉ
βf Β· πΊ)) = (degβ(πΉ βf Β· πΊ)) |
36 | 34, 35 | dgrub 25748 |
. . 3
β’ (((πΉ βf Β·
πΊ) β
(Polyββ) β§ (π + π) β β0 β§
((coeffβ(πΉ
βf Β· πΊ))β(π + π)) β 0) β (π + π) β€ (degβ(πΉ βf Β· πΊ))) |
37 | 6, 13, 33, 36 | syl3anc 1372 |
. 2
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β (π + π) β€ (degβ(πΉ βf Β· πΊ))) |
38 | | dgrcl 25747 |
. . . . 5
β’ ((πΉ βf Β·
πΊ) β
(Polyββ) β (degβ(πΉ βf Β· πΊ)) β
β0) |
39 | 6, 38 | syl 17 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(degβ(πΉ
βf Β· πΊ)) β
β0) |
40 | 39 | nn0red 12533 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(degβ(πΉ
βf Β· πΊ)) β β) |
41 | 13 | nn0red 12533 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β (π + π) β β) |
42 | 40, 41 | letri3d 11356 |
. 2
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
((degβ(πΉ
βf Β· πΊ)) = (π + π) β ((degβ(πΉ βf Β· πΊ)) β€ (π + π) β§ (π + π) β€ (degβ(πΉ βf Β· πΊ))))) |
43 | 4, 37, 42 | mpbir2and 712 |
1
β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β
(degβ(πΉ
βf Β· πΊ)) = (π + π)) |