Step | Hyp | Ref
| Expression |
1 | | dgrco.4 |
. . . . . . . . . . 11
β’ (π β πΊ β (Polyβπ)) |
2 | | plyf 25711 |
. . . . . . . . . . 11
β’ (πΊ β (Polyβπ) β πΊ:ββΆβ) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
β’ (π β πΊ:ββΆβ) |
4 | 3 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (πΊβπ₯) β β) |
5 | | dgrco.3 |
. . . . . . . . . . 11
β’ (π β πΉ β (Polyβπ)) |
6 | | plyf 25711 |
. . . . . . . . . . 11
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
8 | 7 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ ((π β§ (πΊβπ₯) β β) β (πΉβ(πΊβπ₯)) β β) |
9 | 4, 8 | syldan 591 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (πΉβ(πΊβπ₯)) β β) |
10 | | dgrco.5 |
. . . . . . . . . . . . 13
β’ π΄ = (coeffβπΉ) |
11 | 10 | coef3 25745 |
. . . . . . . . . . . 12
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
12 | 5, 11 | syl 17 |
. . . . . . . . . . 11
β’ (π β π΄:β0βΆβ) |
13 | | dgrco.1 |
. . . . . . . . . . . 12
β’ π = (degβπΉ) |
14 | | dgrcl 25746 |
. . . . . . . . . . . . 13
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
15 | 5, 14 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (degβπΉ) β
β0) |
16 | 13, 15 | eqeltrid 2837 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
17 | 12, 16 | ffvelcdmd 7087 |
. . . . . . . . . 10
β’ (π β (π΄βπ) β β) |
18 | 17 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π΄βπ) β β) |
19 | 16 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β π β
β0) |
20 | 4, 19 | expcld 14110 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((πΊβπ₯)βπ) β β) |
21 | 18, 20 | mulcld 11233 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((π΄βπ) Β· ((πΊβπ₯)βπ)) β β) |
22 | 9, 21 | npcand 11574 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))) + ((π΄βπ) Β· ((πΊβπ₯)βπ))) = (πΉβ(πΊβπ₯))) |
23 | 22 | mpteq2dva 5248 |
. . . . . 6
β’ (π β (π₯ β β β¦ (((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))) + ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (π₯ β β β¦ (πΉβ(πΊβπ₯)))) |
24 | | cnex 11190 |
. . . . . . . 8
β’ β
β V |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
26 | 9, 21 | subcld 11570 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))) β β) |
27 | | eqidd 2733 |
. . . . . . 7
β’ (π β (π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
28 | | eqidd 2733 |
. . . . . . 7
β’ (π β (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))) = (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) |
29 | 25, 26, 21, 27, 28 | offval2 7689 |
. . . . . 6
β’ (π β ((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) βf + (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (π₯ β β β¦ (((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))) + ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
30 | 3 | feqmptd 6960 |
. . . . . . 7
β’ (π β πΊ = (π₯ β β β¦ (πΊβπ₯))) |
31 | 7 | feqmptd 6960 |
. . . . . . 7
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
32 | | fveq2 6891 |
. . . . . . 7
β’ (π¦ = (πΊβπ₯) β (πΉβπ¦) = (πΉβ(πΊβπ₯))) |
33 | 4, 30, 31, 32 | fmptco 7126 |
. . . . . 6
β’ (π β (πΉ β πΊ) = (π₯ β β β¦ (πΉβ(πΊβπ₯)))) |
34 | 23, 29, 33 | 3eqtr4rd 2783 |
. . . . 5
β’ (π β (πΉ β πΊ) = ((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) βf + (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
35 | 34 | fveq2d 6895 |
. . . 4
β’ (π β (degβ(πΉ β πΊ)) = (degβ((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) βf + (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))))) |
36 | 35 | adantr 481 |
. . 3
β’ ((π β§ π β β) β (degβ(πΉ β πΊ)) = (degβ((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) βf + (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))))) |
37 | 25, 9, 21, 33, 28 | offval2 7689 |
. . . . . 6
β’ (π β ((πΉ β πΊ) βf β (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
38 | | plyssc 25713 |
. . . . . . . . 9
β’
(Polyβπ)
β (Polyββ) |
39 | 38, 5 | sselid 3980 |
. . . . . . . 8
β’ (π β πΉ β
(Polyββ)) |
40 | 38, 1 | sselid 3980 |
. . . . . . . 8
β’ (π β πΊ β
(Polyββ)) |
41 | | addcl 11191 |
. . . . . . . . 9
β’ ((π§ β β β§ π€ β β) β (π§ + π€) β β) |
42 | 41 | adantl 482 |
. . . . . . . 8
β’ ((π β§ (π§ β β β§ π€ β β)) β (π§ + π€) β β) |
43 | | mulcl 11193 |
. . . . . . . . 9
β’ ((π§ β β β§ π€ β β) β (π§ Β· π€) β β) |
44 | 43 | adantl 482 |
. . . . . . . 8
β’ ((π β§ (π§ β β β§ π€ β β)) β (π§ Β· π€) β β) |
45 | 39, 40, 42, 44 | plyco 25754 |
. . . . . . 7
β’ (π β (πΉ β πΊ) β
(Polyββ)) |
46 | | eqidd 2733 |
. . . . . . . . 9
β’ (π β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) = (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) |
47 | | oveq1 7415 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ₯) β (π¦βπ) = ((πΊβπ₯)βπ)) |
48 | 47 | oveq2d 7424 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ₯) β ((π΄βπ) Β· (π¦βπ)) = ((π΄βπ) Β· ((πΊβπ₯)βπ))) |
49 | 4, 30, 46, 48 | fmptco 7126 |
. . . . . . . 8
β’ (π β ((π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) β πΊ) = (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) |
50 | | ssidd 4005 |
. . . . . . . . . 10
β’ (π β β β
β) |
51 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) = (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) |
52 | 51 | ply1term 25717 |
. . . . . . . . . 10
β’ ((β
β β β§ (π΄βπ) β β β§ π β β0) β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) β
(Polyββ)) |
53 | 50, 17, 16, 52 | syl3anc 1371 |
. . . . . . . . 9
β’ (π β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) β
(Polyββ)) |
54 | 53, 40, 42, 44 | plyco 25754 |
. . . . . . . 8
β’ (π β ((π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) β πΊ) β
(Polyββ)) |
55 | 49, 54 | eqeltrrd 2834 |
. . . . . . 7
β’ (π β (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))) β
(Polyββ)) |
56 | | plysubcl 25735 |
. . . . . . 7
β’ (((πΉ β πΊ) β (Polyββ) β§ (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))) β (Polyββ)) β
((πΉ β πΊ) βf β
(π₯ β β β¦
((π΄βπ) Β· ((πΊβπ₯)βπ)))) β
(Polyββ)) |
57 | 45, 55, 56 | syl2anc 584 |
. . . . . 6
β’ (π β ((πΉ β πΊ) βf β (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) β
(Polyββ)) |
58 | 37, 57 | eqeltrrd 2834 |
. . . . 5
β’ (π β (π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) β
(Polyββ)) |
59 | 58 | adantr 481 |
. . . 4
β’ ((π β§ π β β) β (π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) β
(Polyββ)) |
60 | 55 | adantr 481 |
. . . 4
β’ ((π β§ π β β) β (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))) β
(Polyββ)) |
61 | | dgrco.7 |
. . . . . . . . . . 11
β’ (π β π = (π· + 1)) |
62 | | dgrco.6 |
. . . . . . . . . . . 12
β’ (π β π· β
β0) |
63 | | nn0p1nn 12510 |
. . . . . . . . . . . 12
β’ (π· β β0
β (π· + 1) β
β) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π· + 1) β β) |
65 | 61, 64 | eqeltrd 2833 |
. . . . . . . . . 10
β’ (π β π β β) |
66 | 65 | nngt0d 12260 |
. . . . . . . . 9
β’ (π β 0 < π) |
67 | | fveq2 6891 |
. . . . . . . . . . 11
β’ ((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) = 0π β
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) =
(degβ0π)) |
68 | | dgr0 25775 |
. . . . . . . . . . 11
β’
(degβ0π) = 0 |
69 | 67, 68 | eqtrdi 2788 |
. . . . . . . . . 10
β’ ((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) = 0π β
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) = 0) |
70 | 69 | breq1d 5158 |
. . . . . . . . 9
β’ ((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) = 0π β
((degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < π β 0 < π)) |
71 | 66, 70 | syl5ibrcom 246 |
. . . . . . . 8
β’ (π β ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) = 0π β
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < π)) |
72 | | idd 24 |
. . . . . . . 8
β’ (π β ((degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) < π β (degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < π)) |
73 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(degβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))) = (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) |
74 | 13, 73 | dgrsub 25785 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ)
β§ (π¦ β β
β¦ ((π΄βπ) Β· (π¦βπ))) β (Polyββ)) β
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β€ if(π β€ (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), π)) |
75 | 39, 53, 74 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β€ if(π β€ (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), π)) |
76 | 65 | nnne0d 12261 |
. . . . . . . . . . . . . 14
β’ (π β π β 0) |
77 | 13, 10 | dgreq0 25778 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β (Polyβπ) β (πΉ = 0π β (π΄βπ) = 0)) |
78 | 5, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ = 0π β (π΄βπ) = 0)) |
79 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ = 0π β
(degβπΉ) =
(degβ0π)) |
80 | 79, 68 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ = 0π β
(degβπΉ) =
0) |
81 | 13, 80 | eqtrid 2784 |
. . . . . . . . . . . . . . . 16
β’ (πΉ = 0π β
π = 0) |
82 | 78, 81 | syl6bir 253 |
. . . . . . . . . . . . . . 15
β’ (π β ((π΄βπ) = 0 β π = 0)) |
83 | 82 | necon3d 2961 |
. . . . . . . . . . . . . 14
β’ (π β (π β 0 β (π΄βπ) β 0)) |
84 | 76, 83 | mpd 15 |
. . . . . . . . . . . . 13
β’ (π β (π΄βπ) β 0) |
85 | 51 | dgr1term 25773 |
. . . . . . . . . . . . 13
β’ (((π΄βπ) β β β§ (π΄βπ) β 0 β§ π β β0) β
(degβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))) = π) |
86 | 17, 84, 16, 85 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ (π β (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) = π) |
87 | 86 | ifeq1d 4547 |
. . . . . . . . . . 11
β’ (π β if(π β€ (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), π) = if(π β€ (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), π, π)) |
88 | | ifid 4568 |
. . . . . . . . . . 11
β’ if(π β€ (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), π, π) = π |
89 | 87, 88 | eqtrdi 2788 |
. . . . . . . . . 10
β’ (π β if(π β€ (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), (degβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))), π) = π) |
90 | 75, 89 | breqtrd 5174 |
. . . . . . . . 9
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β€ π) |
91 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(coeffβ(π¦
β β β¦ ((π΄βπ) Β· (π¦βπ)))) = (coeffβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) |
92 | 10, 91 | coesub 25770 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyββ)
β§ (π¦ β β
β¦ ((π΄βπ) Β· (π¦βπ))) β (Polyββ)) β
(coeffβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) = (π΄ βf β
(coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))))) |
93 | 39, 53, 92 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (coeffβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) = (π΄ βf β
(coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))))) |
94 | 93 | fveq1d 6893 |
. . . . . . . . . 10
β’ (π β ((coeffβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))))βπ) = ((π΄ βf β
(coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))))βπ)) |
95 | 12 | ffnd 6718 |
. . . . . . . . . . . 12
β’ (π β π΄ Fn β0) |
96 | 91 | coef3 25745 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))) β (Polyββ) β
(coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))):β0βΆβ) |
97 | 53, 96 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (coeffβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))):β0βΆβ) |
98 | 97 | ffnd 6718 |
. . . . . . . . . . . 12
β’ (π β (coeffβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) Fn
β0) |
99 | | nn0ex 12477 |
. . . . . . . . . . . . 13
β’
β0 β V |
100 | 99 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β0 β
V) |
101 | | inidm 4218 |
. . . . . . . . . . . 12
β’
(β0 β© β0) =
β0 |
102 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (π΄βπ) = (π΄βπ)) |
103 | 51 | coe1term 25772 |
. . . . . . . . . . . . . . 15
β’ (((π΄βπ) β β β§ π β β0 β§ π β β0)
β ((coeffβ(π¦
β β β¦ ((π΄βπ) Β· (π¦βπ))))βπ) = if(π = π, (π΄βπ), 0)) |
104 | 17, 16, 16, 103 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ (π β ((coeffβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))βπ) = if(π = π, (π΄βπ), 0)) |
105 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ π = π |
106 | 105 | iftruei 4535 |
. . . . . . . . . . . . . 14
β’ if(π = π, (π΄βπ), 0) = (π΄βπ) |
107 | 104, 106 | eqtrdi 2788 |
. . . . . . . . . . . . 13
β’ (π β ((coeffβ(π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))βπ) = (π΄βπ)) |
108 | 107 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β
((coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ))))βπ) = (π΄βπ)) |
109 | 95, 98, 100, 100, 101, 102, 108 | ofval 7680 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((π΄ βf β
(coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))))βπ) = ((π΄βπ) β (π΄βπ))) |
110 | 16, 109 | mpdan 685 |
. . . . . . . . . 10
β’ (π β ((π΄ βf β
(coeffβ(π¦ β
β β¦ ((π΄βπ) Β· (π¦βπ)))))βπ) = ((π΄βπ) β (π΄βπ))) |
111 | 17 | subidd 11558 |
. . . . . . . . . 10
β’ (π β ((π΄βπ) β (π΄βπ)) = 0) |
112 | 94, 110, 111 | 3eqtrd 2776 |
. . . . . . . . 9
β’ (π β ((coeffβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))))βπ) = 0) |
113 | | plysubcl 25735 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ)
β§ (π¦ β β
β¦ ((π΄βπ) Β· (π¦βπ))) β (Polyββ)) β
(πΉ βf
β (π¦ β β
β¦ ((π΄βπ) Β· (π¦βπ)))) β
(Polyββ)) |
114 | 39, 53, 113 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β
(Polyββ)) |
115 | | eqid 2732 |
. . . . . . . . . . 11
β’
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) = (degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) |
116 | | eqid 2732 |
. . . . . . . . . . 11
β’
(coeffβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) = (coeffβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) |
117 | 115, 116 | dgrlt 25779 |
. . . . . . . . . 10
β’ (((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) β (Polyββ) β§ π β β0)
β (((πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) = 0π β¨
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < π) β ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β€ π β§ ((coeffβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))))βπ) = 0))) |
118 | 114, 16, 117 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) = 0π β¨
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < π) β ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β€ π β§ ((coeffβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))))βπ) = 0))) |
119 | 90, 112, 118 | mpbir2and 711 |
. . . . . . . 8
β’ (π β ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) = 0π β¨
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < π)) |
120 | 71, 72, 119 | mpjaod 858 |
. . . . . . 7
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) < π) |
121 | 120 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β) β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) < π) |
122 | | dgrcl 25746 |
. . . . . . . . . 10
β’ ((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) β (Polyββ) β
(degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β
β0) |
123 | 114, 122 | syl 17 |
. . . . . . . . 9
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β
β0) |
124 | 123 | nn0red 12532 |
. . . . . . . 8
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β β) |
125 | 124 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β β) |
126 | 16 | nn0red 12532 |
. . . . . . . 8
β’ (π β π β β) |
127 | 126 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
128 | | nnre 12218 |
. . . . . . . 8
β’ (π β β β π β
β) |
129 | 128 | adantl 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
130 | | nngt0 12242 |
. . . . . . . 8
β’ (π β β β 0 <
π) |
131 | 130 | adantl 482 |
. . . . . . 7
β’ ((π β§ π β β) β 0 < π) |
132 | | ltmul1 12063 |
. . . . . . 7
β’
(((degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β β β§ π β β β§ (π β β β§ 0 < π)) β ((degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) < π β ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π) < (π Β· π))) |
133 | 125, 127,
129, 131, 132 | syl112anc 1374 |
. . . . . 6
β’ ((π β§ π β β) β ((degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) < π β ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π) < (π Β· π))) |
134 | 121, 133 | mpbid 231 |
. . . . 5
β’ ((π β§ π β β) β ((degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) Β· π) < (π Β· π)) |
135 | 7 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (πΉβπ¦) β β) |
136 | 17 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (π΄βπ) β β) |
137 | | id 22 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ β
β) |
138 | | expcl 14044 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π β β0)
β (π¦βπ) β
β) |
139 | 137, 16, 138 | syl2anr 597 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (π¦βπ) β β) |
140 | 136, 139 | mulcld 11233 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β ((π΄βπ) Β· (π¦βπ)) β β) |
141 | 25, 135, 140, 31, 46 | offval2 7689 |
. . . . . . . . 9
β’ (π β (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) = (π¦ β β β¦ ((πΉβπ¦) β ((π΄βπ) Β· (π¦βπ))))) |
142 | 32, 48 | oveq12d 7426 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ₯) β ((πΉβπ¦) β ((π΄βπ) Β· (π¦βπ))) = ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) |
143 | 4, 30, 141, 142 | fmptco 7126 |
. . . . . . . 8
β’ (π β ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β πΊ) = (π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
144 | 143 | fveq2d 6895 |
. . . . . . 7
β’ (π β (degβ((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) β πΊ)) = (degβ(π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))))) |
145 | 120, 61 | breqtrd 5174 |
. . . . . . . . 9
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) < (π· + 1)) |
146 | | nn0leltp1 12620 |
. . . . . . . . . 10
β’
(((degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β β0 β§ π· β β0)
β ((degβ(πΉ
βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β€ π· β (degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < (π· + 1))) |
147 | 123, 62, 146 | syl2anc 584 |
. . . . . . . . 9
β’ (π β ((degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β€ π· β (degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) < (π· + 1))) |
148 | 145, 147 | mpbird 256 |
. . . . . . . 8
β’ (π β (degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β€ π·) |
149 | | fveq2 6891 |
. . . . . . . . . . 11
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β (degβπ) = (degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))))) |
150 | 149 | breq1d 5158 |
. . . . . . . . . 10
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β ((degβπ) β€ π· β (degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β€ π·)) |
151 | | coeq1 5857 |
. . . . . . . . . . . 12
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β (π β πΊ) = ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β πΊ)) |
152 | 151 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β (degβ(π β πΊ)) = (degβ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β πΊ))) |
153 | 149 | oveq1d 7423 |
. . . . . . . . . . 11
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β ((degβπ) Β· π) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π)) |
154 | 152, 153 | eqeq12d 2748 |
. . . . . . . . . 10
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β ((degβ(π β πΊ)) = ((degβπ) Β· π) β (degβ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β πΊ)) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π))) |
155 | 150, 154 | imbi12d 344 |
. . . . . . . . 9
β’ (π = (πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β (((degβπ) β€ π· β (degβ(π β πΊ)) = ((degβπ) Β· π)) β ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) β€ π· β (degβ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β πΊ)) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π)))) |
156 | | dgrco.8 |
. . . . . . . . 9
β’ (π β βπ β (Polyββ)((degβπ) β€ π· β (degβ(π β πΊ)) = ((degβπ) Β· π))) |
157 | 155, 156,
114 | rspcdva 3613 |
. . . . . . . 8
β’ (π β ((degβ(πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ))))) β€ π· β (degβ((πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ)))) β πΊ)) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π))) |
158 | 148, 157 | mpd 15 |
. . . . . . 7
β’ (π β (degβ((πΉ βf β
(π¦ β β β¦
((π΄βπ) Β· (π¦βπ)))) β πΊ)) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π)) |
159 | 144, 158 | eqtr3d 2774 |
. . . . . 6
β’ (π β (degβ(π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π)) |
160 | 159 | adantr 481 |
. . . . 5
β’ ((π β§ π β β) β (degβ(π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) = ((degβ(πΉ βf β (π¦ β β β¦ ((π΄βπ) Β· (π¦βπ))))) Β· π)) |
161 | | fconstmpt 5738 |
. . . . . . . . . . 11
β’ (β
Γ {(π΄βπ)}) = (π₯ β β β¦ (π΄βπ)) |
162 | 161 | a1i 11 |
. . . . . . . . . 10
β’ (π β (β Γ {(π΄βπ)}) = (π₯ β β β¦ (π΄βπ))) |
163 | | eqidd 2733 |
. . . . . . . . . 10
β’ (π β (π₯ β β β¦ ((πΊβπ₯)βπ)) = (π₯ β β β¦ ((πΊβπ₯)βπ))) |
164 | 25, 18, 20, 162, 163 | offval2 7689 |
. . . . . . . . 9
β’ (π β ((β Γ {(π΄βπ)}) βf Β· (π₯ β β β¦ ((πΊβπ₯)βπ))) = (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) |
165 | 164 | fveq2d 6895 |
. . . . . . . 8
β’ (π β (degβ((β
Γ {(π΄βπ)}) βf Β·
(π₯ β β β¦
((πΊβπ₯)βπ)))) = (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
166 | | eqidd 2733 |
. . . . . . . . . . 11
β’ (π β (π¦ β β β¦ (π¦βπ)) = (π¦ β β β¦ (π¦βπ))) |
167 | 4, 30, 166, 47 | fmptco 7126 |
. . . . . . . . . 10
β’ (π β ((π¦ β β β¦ (π¦βπ)) β πΊ) = (π₯ β β β¦ ((πΊβπ₯)βπ))) |
168 | | 1cnd 11208 |
. . . . . . . . . . . 12
β’ (π β 1 β
β) |
169 | | plypow 25718 |
. . . . . . . . . . . 12
β’ ((β
β β β§ 1 β β β§ π β β0) β (π¦ β β β¦ (π¦βπ)) β
(Polyββ)) |
170 | 50, 168, 16, 169 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (π β (π¦ β β β¦ (π¦βπ)) β
(Polyββ)) |
171 | 170, 40, 42, 44 | plyco 25754 |
. . . . . . . . . 10
β’ (π β ((π¦ β β β¦ (π¦βπ)) β πΊ) β
(Polyββ)) |
172 | 167, 171 | eqeltrrd 2834 |
. . . . . . . . 9
β’ (π β (π₯ β β β¦ ((πΊβπ₯)βπ)) β
(Polyββ)) |
173 | | dgrmulc 25784 |
. . . . . . . . 9
β’ (((π΄βπ) β β β§ (π΄βπ) β 0 β§ (π₯ β β β¦ ((πΊβπ₯)βπ)) β (Polyββ)) β
(degβ((β Γ {(π΄βπ)}) βf Β· (π₯ β β β¦ ((πΊβπ₯)βπ)))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ)))) |
174 | 17, 84, 172, 173 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (degβ((β
Γ {(π΄βπ)}) βf Β·
(π₯ β β β¦
((πΊβπ₯)βπ)))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ)))) |
175 | 165, 174 | eqtr3d 2774 |
. . . . . . 7
β’ (π β (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ)))) |
176 | 175 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β) β (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (degβ(π₯ β β β¦ ((πΊβπ₯)βπ)))) |
177 | | dgrco.2 |
. . . . . . 7
β’ π = (degβπΊ) |
178 | 65 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
179 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
180 | 1 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β πΊ β (Polyβπ)) |
181 | 177, 178,
179, 180 | dgrcolem1 25786 |
. . . . . 6
β’ ((π β§ π β β) β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) |
182 | 176, 181 | eqtrd 2772 |
. . . . 5
β’ ((π β§ π β β) β (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (π Β· π)) |
183 | 134, 160,
182 | 3brtr4d 5180 |
. . . 4
β’ ((π β§ π β β) β (degβ(π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) < (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
184 | | eqid 2732 |
. . . . 5
β’
(degβ(π₯ β
β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) = (degβ(π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
185 | | eqid 2732 |
. . . . 5
β’
(degβ(π₯ β
β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) = (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ)))) |
186 | 184, 185 | dgradd2 25781 |
. . . 4
β’ (((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) β (Polyββ) β§
(π₯ β β β¦
((π΄βπ) Β· ((πΊβπ₯)βπ))) β (Polyββ) β§
(degβ(π₯ β
β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ))))) < (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) β (degβ((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) βf + (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) = (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
187 | 59, 60, 183, 186 | syl3anc 1371 |
. . 3
β’ ((π β§ π β β) β (degβ((π₯ β β β¦ ((πΉβ(πΊβπ₯)) β ((π΄βπ) Β· ((πΊβπ₯)βπ)))) βf + (π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) = (degβ(π₯ β β β¦ ((π΄βπ) Β· ((πΊβπ₯)βπ))))) |
188 | 36, 187, 182 | 3eqtrd 2776 |
. 2
β’ ((π β§ π β β) β (degβ(πΉ β πΊ)) = (π Β· π)) |
189 | | 0cn 11205 |
. . . . . . . 8
β’ 0 β
β |
190 | | ffvelcdm 7083 |
. . . . . . . 8
β’ ((πΊ:ββΆβ β§ 0
β β) β (πΊβ0) β β) |
191 | 3, 189, 190 | sylancl 586 |
. . . . . . 7
β’ (π β (πΊβ0) β β) |
192 | 7, 191 | ffvelcdmd 7087 |
. . . . . 6
β’ (π β (πΉβ(πΊβ0)) β β) |
193 | | 0dgr 25758 |
. . . . . 6
β’ ((πΉβ(πΊβ0)) β β β
(degβ(β Γ {(πΉβ(πΊβ0))})) = 0) |
194 | 192, 193 | syl 17 |
. . . . 5
β’ (π β (degβ(β
Γ {(πΉβ(πΊβ0))})) =
0) |
195 | 16 | nn0cnd 12533 |
. . . . . 6
β’ (π β π β β) |
196 | 195 | mul01d 11412 |
. . . . 5
β’ (π β (π Β· 0) = 0) |
197 | 194, 196 | eqtr4d 2775 |
. . . 4
β’ (π β (degβ(β
Γ {(πΉβ(πΊβ0))})) = (π Β· 0)) |
198 | 197 | adantr 481 |
. . 3
β’ ((π β§ π = 0) β (degβ(β Γ
{(πΉβ(πΊβ0))})) = (π Β· 0)) |
199 | 191 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π = 0) β§ π₯ β β) β (πΊβ0) β β) |
200 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π = 0) β π = 0) |
201 | 177, 200 | eqtr3id 2786 |
. . . . . . . 8
β’ ((π β§ π = 0) β (degβπΊ) = 0) |
202 | | 0dgrb 25759 |
. . . . . . . . . 10
β’ (πΊ β (Polyβπ) β ((degβπΊ) = 0 β πΊ = (β Γ {(πΊβ0)}))) |
203 | 1, 202 | syl 17 |
. . . . . . . . 9
β’ (π β ((degβπΊ) = 0 β πΊ = (β Γ {(πΊβ0)}))) |
204 | 203 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π = 0) β ((degβπΊ) = 0 β πΊ = (β Γ {(πΊβ0)}))) |
205 | 201, 204 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π = 0) β πΊ = (β Γ {(πΊβ0)})) |
206 | | fconstmpt 5738 |
. . . . . . 7
β’ (β
Γ {(πΊβ0)}) =
(π₯ β β β¦
(πΊβ0)) |
207 | 205, 206 | eqtrdi 2788 |
. . . . . 6
β’ ((π β§ π = 0) β πΊ = (π₯ β β β¦ (πΊβ0))) |
208 | 31 | adantr 481 |
. . . . . 6
β’ ((π β§ π = 0) β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
209 | | fveq2 6891 |
. . . . . 6
β’ (π¦ = (πΊβ0) β (πΉβπ¦) = (πΉβ(πΊβ0))) |
210 | 199, 207,
208, 209 | fmptco 7126 |
. . . . 5
β’ ((π β§ π = 0) β (πΉ β πΊ) = (π₯ β β β¦ (πΉβ(πΊβ0)))) |
211 | | fconstmpt 5738 |
. . . . 5
β’ (β
Γ {(πΉβ(πΊβ0))}) = (π₯ β β β¦ (πΉβ(πΊβ0))) |
212 | 210, 211 | eqtr4di 2790 |
. . . 4
β’ ((π β§ π = 0) β (πΉ β πΊ) = (β Γ {(πΉβ(πΊβ0))})) |
213 | 212 | fveq2d 6895 |
. . 3
β’ ((π β§ π = 0) β (degβ(πΉ β πΊ)) = (degβ(β Γ {(πΉβ(πΊβ0))}))) |
214 | 200 | oveq2d 7424 |
. . 3
β’ ((π β§ π = 0) β (π Β· π) = (π Β· 0)) |
215 | 198, 213,
214 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π = 0) β (degβ(πΉ β πΊ)) = (π Β· π)) |
216 | | dgrcl 25746 |
. . . . 5
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
217 | 1, 216 | syl 17 |
. . . 4
β’ (π β (degβπΊ) β
β0) |
218 | 177, 217 | eqeltrid 2837 |
. . 3
β’ (π β π β
β0) |
219 | | elnn0 12473 |
. . 3
β’ (π β β0
β (π β β
β¨ π =
0)) |
220 | 218, 219 | sylib 217 |
. 2
β’ (π β (π β β β¨ π = 0)) |
221 | 188, 215,
220 | mpjaodan 957 |
1
β’ (π β (degβ(πΉ β πΊ)) = (π Β· π)) |