Step | Hyp | Ref
| Expression |
1 | | dgrub.2 |
. . . . 5
β’ π = (degβπΉ) |
2 | | dgrcl 25746 |
. . . . 5
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
3 | 1, 2 | eqeltrid 2837 |
. . . 4
β’ (πΉ β (Polyβπ) β π β
β0) |
4 | 3 | 3ad2ant1 1133 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π β
β0) |
5 | 4 | nn0red 12532 |
. 2
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π β β) |
6 | | simp2 1137 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π β
β0) |
7 | 6 | nn0red 12532 |
. 2
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π β β) |
8 | | dgrub.1 |
. . . . . . . . . . . . 13
β’ π΄ = (coeffβπΉ) |
9 | 8 | dgrlem 25742 |
. . . . . . . . . . . 12
β’ (πΉ β (Polyβπ) β (π΄:β0βΆ(π βͺ {0}) β§ βπ β β€ βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |
10 | 9 | simpld 495 |
. . . . . . . . . . 11
β’ (πΉ β (Polyβπ) β π΄:β0βΆ(π βͺ {0})) |
11 | 10 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π΄:β0βΆ(π βͺ {0})) |
12 | | ffn 6717 |
. . . . . . . . . 10
β’ (π΄:β0βΆ(π βͺ {0}) β π΄ Fn
β0) |
13 | | elpreima 7059 |
. . . . . . . . . 10
β’ (π΄ Fn β0 β
(π¦ β (β‘π΄ β (β β {0})) β
(π¦ β
β0 β§ (π΄βπ¦) β (β β
{0})))) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β (π¦ β (β‘π΄ β (β β {0})) β
(π¦ β
β0 β§ (π΄βπ¦) β (β β
{0})))) |
15 | 14 | biimpa 477 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
(π¦ β
β0 β§ (π΄βπ¦) β (β β
{0}))) |
16 | 15 | simpld 495 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
π¦ β
β0) |
17 | 16 | nn0red 12532 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
π¦ β
β) |
18 | 7 | adantr 481 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
π β
β) |
19 | | eldifsni 4793 |
. . . . . . . 8
β’ ((π΄βπ¦) β (β β {0}) β (π΄βπ¦) β 0) |
20 | 15, 19 | simpl2im 504 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
(π΄βπ¦) β 0) |
21 | | simp3 1138 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β (π΄ β
(β€β₯β(π + 1))) = {0}) |
22 | 8 | coef3 25745 |
. . . . . . . . . . . 12
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
23 | 22 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π΄:β0βΆβ) |
24 | | plyco0 25705 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) = {0} β βπ¦ β β0
((π΄βπ¦) β 0 β π¦ β€ π))) |
25 | 6, 23, 24 | syl2anc 584 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β ((π΄ β
(β€β₯β(π + 1))) = {0} β βπ¦ β β0
((π΄βπ¦) β 0 β π¦ β€ π))) |
26 | 21, 25 | mpbid 231 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β βπ¦ β β0
((π΄βπ¦) β 0 β π¦ β€ π)) |
27 | 26 | r19.21bi 3248 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β β0) β ((π΄βπ¦) β 0 β π¦ β€ π)) |
28 | 16, 27 | syldan 591 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
((π΄βπ¦) β 0 β π¦ β€ π)) |
29 | 20, 28 | mpd 15 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
π¦ β€ π) |
30 | 17, 18, 29 | lensymd 11364 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β§ π¦ β (β‘π΄ β (β β {0}))) β
Β¬ π < π¦) |
31 | 30 | ralrimiva 3146 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β βπ¦ β (β‘π΄ β (β β {0})) Β¬ π < π¦) |
32 | | nn0ssre 12475 |
. . . . . . 7
β’
β0 β β |
33 | | ltso 11293 |
. . . . . . 7
β’ < Or
β |
34 | | soss 5608 |
. . . . . . 7
β’
(β0 β β β ( < Or β β
< Or β0)) |
35 | 32, 33, 34 | mp2 9 |
. . . . . 6
β’ < Or
β0 |
36 | 35 | a1i 11 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β < Or
β0) |
37 | | 0zd 12569 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β 0 β
β€) |
38 | | cnvimass 6080 |
. . . . . . . 8
β’ (β‘π΄ β (β β {0})) β dom
π΄ |
39 | 38, 10 | fssdm 6737 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β (β‘π΄ β (β β {0})) β
β0) |
40 | 9 | simprd 496 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β βπ β β€ βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π) |
41 | | nn0uz 12863 |
. . . . . . . 8
β’
β0 = (β€β₯β0) |
42 | 41 | uzsupss 12923 |
. . . . . . 7
β’ ((0
β β€ β§ (β‘π΄ β (β β {0}))
β β0 β§ βπ β β€ βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π) β βπ β β0 (βπ₯ β (β‘π΄ β (β β {0})) Β¬ π < π₯ β§ βπ₯ β β0 (π₯ < π β βπ¦ β (β‘π΄ β (β β {0}))π₯ < π¦))) |
43 | 37, 39, 40, 42 | syl3anc 1371 |
. . . . . 6
β’ (πΉ β (Polyβπ) β βπ β β0
(βπ₯ β (β‘π΄ β (β β {0})) Β¬ π < π₯ β§ βπ₯ β β0 (π₯ < π β βπ¦ β (β‘π΄ β (β β {0}))π₯ < π¦))) |
44 | 43 | 3ad2ant1 1133 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β βπ β β0
(βπ₯ β (β‘π΄ β (β β {0})) Β¬ π < π₯ β§ βπ₯ β β0 (π₯ < π β βπ¦ β (β‘π΄ β (β β {0}))π₯ < π¦))) |
45 | 36, 44 | supnub 9456 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β ((π β β0 β§
βπ¦ β (β‘π΄ β (β β {0})) Β¬ π < π¦) β Β¬ π < sup((β‘π΄ β (β β {0})),
β0, < ))) |
46 | 6, 31, 45 | mp2and 697 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β Β¬ π < sup((β‘π΄ β (β β {0})),
β0, < )) |
47 | 8 | dgrval 25741 |
. . . . . 6
β’ (πΉ β (Polyβπ) β (degβπΉ) = sup((β‘π΄ β (β β {0})),
β0, < )) |
48 | 1, 47 | eqtrid 2784 |
. . . . 5
β’ (πΉ β (Polyβπ) β π = sup((β‘π΄ β (β β {0})),
β0, < )) |
49 | 48 | 3ad2ant1 1133 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π = sup((β‘π΄ β (β β {0})),
β0, < )) |
50 | 49 | breq2d 5160 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β (π < π β π < sup((β‘π΄ β (β β {0})),
β0, < ))) |
51 | 46, 50 | mtbird 324 |
. 2
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β Β¬ π < π) |
52 | 5, 7, 51 | nltled 11363 |
1
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄ β
(β€β₯β(π + 1))) = {0}) β π β€ π) |