Step | Hyp | Ref
| Expression |
1 | | plyaddcl 25734 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ βf + πΊ) β
(Polyββ)) |
2 | 1 | 3adant3 1133 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (πΉ βf + πΊ) β
(Polyββ)) |
3 | | dgrcl 25747 |
. . . . 5
β’ ((πΉ βf + πΊ) β (Polyββ)
β (degβ(πΉ
βf + πΊ))
β β0) |
4 | 2, 3 | syl 17 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (degβ(πΉ βf + πΊ)) β
β0) |
5 | 4 | nn0red 12533 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (degβ(πΉ βf + πΊ)) β β) |
6 | | dgradd.2 |
. . . . . . 7
β’ π = (degβπΊ) |
7 | | dgrcl 25747 |
. . . . . . 7
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
8 | 6, 7 | eqeltrid 2838 |
. . . . . 6
β’ (πΊ β (Polyβπ) β π β
β0) |
9 | 8 | 3ad2ant2 1135 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β
β0) |
10 | 9 | nn0red 12533 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β β) |
11 | | dgradd.1 |
. . . . . . 7
β’ π = (degβπΉ) |
12 | | dgrcl 25747 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
13 | 11, 12 | eqeltrid 2838 |
. . . . . 6
β’ (πΉ β (Polyβπ) β π β
β0) |
14 | 13 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β
β0) |
15 | 14 | nn0red 12533 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β β) |
16 | 10, 15 | ifcld 4575 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β if(π β€ π, π, π) β β) |
17 | 11, 6 | dgradd 25781 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβ(πΉ βf + πΊ)) β€ if(π β€ π, π, π)) |
18 | 17 | 3adant3 1133 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (degβ(πΉ βf + πΊ)) β€ if(π β€ π, π, π)) |
19 | 10 | leidd 11780 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β€ π) |
20 | | simp3 1139 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π < π) |
21 | 15, 10, 20 | ltled 11362 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β€ π) |
22 | | breq1 5152 |
. . . . 5
β’ (π = if(π β€ π, π, π) β (π β€ π β if(π β€ π, π, π) β€ π)) |
23 | | breq1 5152 |
. . . . 5
β’ (π = if(π β€ π, π, π) β (π β€ π β if(π β€ π, π, π) β€ π)) |
24 | 22, 23 | ifboth 4568 |
. . . 4
β’ ((π β€ π β§ π β€ π) β if(π β€ π, π, π) β€ π) |
25 | 19, 21, 24 | syl2anc 585 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β if(π β€ π, π, π) β€ π) |
26 | 5, 16, 10, 18, 25 | letrd 11371 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (degβ(πΉ βf + πΊ)) β€ π) |
27 | | eqid 2733 |
. . . . . . . 8
β’
(coeffβπΉ) =
(coeffβπΉ) |
28 | | eqid 2733 |
. . . . . . . 8
β’
(coeffβπΊ) =
(coeffβπΊ) |
29 | 27, 28 | coeadd 25765 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (coeffβ(πΉ βf + πΊ)) = ((coeffβπΉ) βf + (coeffβπΊ))) |
30 | 29 | 3adant3 1133 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (coeffβ(πΉ βf + πΊ)) = ((coeffβπΉ) βf + (coeffβπΊ))) |
31 | 30 | fveq1d 6894 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((coeffβ(πΉ βf + πΊ))βπ) = (((coeffβπΉ) βf + (coeffβπΊ))βπ)) |
32 | 27 | coef3 25746 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β (coeffβπΉ):β0βΆβ) |
33 | 32 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (coeffβπΉ):β0βΆβ) |
34 | 33 | ffnd 6719 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (coeffβπΉ) Fn β0) |
35 | 28 | coef3 25746 |
. . . . . . . . 9
β’ (πΊ β (Polyβπ) β (coeffβπΊ):β0βΆβ) |
36 | 35 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (coeffβπΊ):β0βΆβ) |
37 | 36 | ffnd 6719 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (coeffβπΊ) Fn β0) |
38 | | nn0ex 12478 |
. . . . . . . 8
β’
β0 β V |
39 | 38 | a1i 11 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β β0 β
V) |
40 | | inidm 4219 |
. . . . . . 7
β’
(β0 β© β0) =
β0 |
41 | 15, 10 | ltnled 11361 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (π < π β Β¬ π β€ π)) |
42 | 20, 41 | mpbid 231 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β Β¬ π β€ π) |
43 | | simp1 1137 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β πΉ β (Polyβπ)) |
44 | 27, 11 | dgrub 25748 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyβπ) β§ π β β0 β§
((coeffβπΉ)βπ) β 0) β π β€ π) |
45 | 44 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyβπ) β§ π β β0) β
(((coeffβπΉ)βπ) β 0 β π β€ π)) |
46 | 43, 9, 45 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (((coeffβπΉ)βπ) β 0 β π β€ π)) |
47 | 46 | necon1bd 2959 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (Β¬ π β€ π β ((coeffβπΉ)βπ) = 0)) |
48 | 42, 47 | mpd 15 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((coeffβπΉ)βπ) = 0) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β§ π β β0) β
((coeffβπΉ)βπ) = 0) |
50 | | eqidd 2734 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β§ π β β0) β
((coeffβπΊ)βπ) = ((coeffβπΊ)βπ)) |
51 | 34, 37, 39, 39, 40, 49, 50 | ofval 7681 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β§ π β β0) β
(((coeffβπΉ)
βf + (coeffβπΊ))βπ) = (0 + ((coeffβπΊ)βπ))) |
52 | 9, 51 | mpdan 686 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (((coeffβπΉ) βf + (coeffβπΊ))βπ) = (0 + ((coeffβπΊ)βπ))) |
53 | 36, 9 | ffvelcdmd 7088 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((coeffβπΊ)βπ) β β) |
54 | 53 | addlidd 11415 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (0 + ((coeffβπΊ)βπ)) = ((coeffβπΊ)βπ)) |
55 | 31, 52, 54 | 3eqtrd 2777 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((coeffβ(πΉ βf + πΊ))βπ) = ((coeffβπΊ)βπ)) |
56 | | simp2 1138 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β πΊ β (Polyβπ)) |
57 | | 0red 11217 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β 0 β β) |
58 | 14 | nn0ge0d 12535 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β 0 β€ π) |
59 | 57, 15, 10, 58, 20 | lelttrd 11372 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β 0 < π) |
60 | 59 | gt0ne0d 11778 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β 0) |
61 | 6, 28 | dgreq0 25779 |
. . . . . . 7
β’ (πΊ β (Polyβπ) β (πΊ = 0π β
((coeffβπΊ)βπ) = 0)) |
62 | | fveq2 6892 |
. . . . . . . 8
β’ (πΊ = 0π β
(degβπΊ) =
(degβ0π)) |
63 | | dgr0 25776 |
. . . . . . . . 9
β’
(degβ0π) = 0 |
64 | 63 | eqcomi 2742 |
. . . . . . . 8
β’ 0 =
(degβ0π) |
65 | 62, 6, 64 | 3eqtr4g 2798 |
. . . . . . 7
β’ (πΊ = 0π β
π = 0) |
66 | 61, 65 | syl6bir 254 |
. . . . . 6
β’ (πΊ β (Polyβπ) β (((coeffβπΊ)βπ) = 0 β π = 0)) |
67 | 66 | necon3d 2962 |
. . . . 5
β’ (πΊ β (Polyβπ) β (π β 0 β ((coeffβπΊ)βπ) β 0)) |
68 | 56, 60, 67 | sylc 65 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((coeffβπΊ)βπ) β 0) |
69 | 55, 68 | eqnetrd 3009 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((coeffβ(πΉ βf + πΊ))βπ) β 0) |
70 | | eqid 2733 |
. . . 4
β’
(coeffβ(πΉ
βf + πΊ)) =
(coeffβ(πΉ
βf + πΊ)) |
71 | | eqid 2733 |
. . . 4
β’
(degβ(πΉ
βf + πΊ)) =
(degβ(πΉ
βf + πΊ)) |
72 | 70, 71 | dgrub 25748 |
. . 3
β’ (((πΉ βf + πΊ) β (Polyββ)
β§ π β
β0 β§ ((coeffβ(πΉ βf + πΊ))βπ) β 0) β π β€ (degβ(πΉ βf + πΊ))) |
73 | 2, 9, 69, 72 | syl3anc 1372 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β π β€ (degβ(πΉ βf + πΊ))) |
74 | 5, 10 | letri3d 11356 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β ((degβ(πΉ βf + πΊ)) = π β ((degβ(πΉ βf + πΊ)) β€ π β§ π β€ (degβ(πΉ βf + πΊ))))) |
75 | 26, 73, 74 | mpbir2and 712 |
1
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (degβ(πΉ βf + πΊ)) = π) |