Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
πΉ =
0π) |
2 | 1 | fveq2d 6896 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
(degβπΉ) =
(degβ0π)) |
3 | | dgreq0.1 |
. . . . . 6
β’ π = (degβπΉ) |
4 | | dgr0 25776 |
. . . . . . 7
β’
(degβ0π) = 0 |
5 | 4 | eqcomi 2742 |
. . . . . 6
β’ 0 =
(degβ0π) |
6 | 2, 3, 5 | 3eqtr4g 2798 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
π = 0) |
7 | | nn0ge0 12497 |
. . . . . 6
β’ (π β β0
β 0 β€ π) |
8 | 7 | ad2antlr 726 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
0 β€ π) |
9 | 6, 8 | eqbrtrd 5171 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
π β€ π) |
10 | 1 | fveq2d 6896 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
(coeffβπΉ) =
(coeffβ0π)) |
11 | | dgreq0.2 |
. . . . . . 7
β’ π΄ = (coeffβπΉ) |
12 | | coe0 25770 |
. . . . . . . 8
β’
(coeffβ0π) = (β0 Γ
{0}) |
13 | 12 | eqcomi 2742 |
. . . . . . 7
β’
(β0 Γ {0}) =
(coeffβ0π) |
14 | 10, 11, 13 | 3eqtr4g 2798 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
π΄ = (β0
Γ {0})) |
15 | 14 | fveq1d 6894 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
(π΄βπ) = ((β0 Γ
{0})βπ)) |
16 | | c0ex 11208 |
. . . . . . 7
β’ 0 β
V |
17 | 16 | fvconst2 7205 |
. . . . . 6
β’ (π β β0
β ((β0 Γ {0})βπ) = 0) |
18 | 17 | ad2antlr 726 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
((β0 Γ {0})βπ) = 0) |
19 | 15, 18 | eqtrd 2773 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
(π΄βπ) = 0) |
20 | 9, 19 | jca 513 |
. . 3
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ πΉ = 0π) β
(π β€ π β§ (π΄βπ) = 0)) |
21 | | dgrcl 25747 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
22 | 3, 21 | eqeltrid 2838 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β π β
β0) |
23 | 22 | nn0red 12533 |
. . . . . 6
β’ (πΉ β (Polyβπ) β π β β) |
24 | | nn0re 12481 |
. . . . . 6
β’ (π β β0
β π β
β) |
25 | | ltle 11302 |
. . . . . 6
β’ ((π β β β§ π β β) β (π < π β π β€ π)) |
26 | 23, 24, 25 | syl2an 597 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π β β0) β (π < π β π β€ π)) |
27 | 26 | imp 408 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ π < π) β π β€ π) |
28 | 11, 3 | dgrub 25748 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄βπ) β 0) β π β€ π) |
29 | 28 | 3expia 1122 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
30 | | lenlt 11292 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π β€ π β Β¬ π < π)) |
31 | 24, 23, 30 | syl2anr 598 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ π β β0) β (π β€ π β Β¬ π < π)) |
32 | 29, 31 | sylibd 238 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((π΄βπ) β 0 β Β¬ π < π)) |
33 | 32 | necon4ad 2960 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π β β0) β (π < π β (π΄βπ) = 0)) |
34 | 33 | imp 408 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ π < π) β (π΄βπ) = 0) |
35 | 27, 34 | jca 513 |
. . 3
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ π < π) β (π β€ π β§ (π΄βπ) = 0)) |
36 | 20, 35 | jaodan 957 |
. 2
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (πΉ = 0π β¨
π < π)) β (π β€ π β§ (π΄βπ) = 0)) |
37 | | leloe 11300 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π β€ π β (π < π β¨ π = π))) |
38 | 23, 24, 37 | syl2an 597 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π β β0) β (π β€ π β (π < π β¨ π = π))) |
39 | 38 | biimpa 478 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ π β€ π) β (π < π β¨ π = π)) |
40 | 39 | adantrr 716 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (π < π β¨ π = π)) |
41 | | fveq2 6892 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
42 | 3, 11 | dgreq0 25779 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β (πΉ = 0π β (π΄βπ) = 0)) |
43 | 42 | ad2antrr 725 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (πΉ = 0π β (π΄βπ) = 0)) |
44 | | simprr 772 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (π΄βπ) = 0) |
45 | 44 | eqeq2d 2744 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β ((π΄βπ) = (π΄βπ) β (π΄βπ) = 0)) |
46 | 43, 45 | bitr4d 282 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (πΉ = 0π β (π΄βπ) = (π΄βπ))) |
47 | 41, 46 | imbitrrid 245 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (π = π β πΉ = 0π)) |
48 | 47 | orim2d 966 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β ((π < π β¨ π = π) β (π < π β¨ πΉ = 0π))) |
49 | 40, 48 | mpd 15 |
. . 3
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (π < π β¨ πΉ = 0π)) |
50 | 49 | orcomd 870 |
. 2
β’ (((πΉ β (Polyβπ) β§ π β β0) β§ (π β€ π β§ (π΄βπ) = 0)) β (πΉ = 0π β¨ π < π)) |
51 | 36, 50 | impbida 800 |
1
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((πΉ = 0π β¨
π < π) β (π β€ π β§ (π΄βπ) = 0))) |