Step | Hyp | Ref
| Expression |
1 | | dgreq0.2 |
. . . . . 6
β’ π΄ = (coeffβπΉ) |
2 | | fveq2 6847 |
. . . . . 6
β’ (πΉ = 0π β
(coeffβπΉ) =
(coeffβ0π)) |
3 | 1, 2 | eqtrid 2789 |
. . . . 5
β’ (πΉ = 0π β
π΄ =
(coeffβ0π)) |
4 | | coe0 25633 |
. . . . 5
β’
(coeffβ0π) = (β0 Γ
{0}) |
5 | 3, 4 | eqtrdi 2793 |
. . . 4
β’ (πΉ = 0π β
π΄ = (β0
Γ {0})) |
6 | | dgreq0.1 |
. . . . . 6
β’ π = (degβπΉ) |
7 | | fveq2 6847 |
. . . . . 6
β’ (πΉ = 0π β
(degβπΉ) =
(degβ0π)) |
8 | 6, 7 | eqtrid 2789 |
. . . . 5
β’ (πΉ = 0π β
π =
(degβ0π)) |
9 | | dgr0 25639 |
. . . . 5
β’
(degβ0π) = 0 |
10 | 8, 9 | eqtrdi 2793 |
. . . 4
β’ (πΉ = 0π β
π = 0) |
11 | 5, 10 | fveq12d 6854 |
. . 3
β’ (πΉ = 0π β
(π΄βπ) = ((β0 Γ
{0})β0)) |
12 | | 0nn0 12435 |
. . . 4
β’ 0 β
β0 |
13 | | fvconst2g 7156 |
. . . 4
β’ ((0
β β0 β§ 0 β β0) β
((β0 Γ {0})β0) = 0) |
14 | 12, 12, 13 | mp2an 691 |
. . 3
β’
((β0 Γ {0})β0) = 0 |
15 | 11, 14 | eqtrdi 2793 |
. 2
β’ (πΉ = 0π β
(π΄βπ) = 0) |
16 | 1 | coefv0 25625 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β (πΉβ0) = (π΄β0)) |
17 | 16 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (πΉβ0) = (π΄β0)) |
18 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β π β β) |
19 | 18 | nnred 12175 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β π β β) |
20 | 19 | ltm1d 12094 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β (π β 1) < π) |
21 | | nnre 12167 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
22 | 21 | adantl 483 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β π β β) |
23 | | peano2rem 11475 |
. . . . . . . . . . . 12
β’ (π β β β (π β 1) β
β) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β (π β 1) β β) |
25 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β πΉ β (Polyβπ)) |
26 | | nnm1nn0 12461 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
27 | 26 | adantl 483 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β (π β 1) β
β0) |
28 | 1, 6 | dgrub 25611 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄βπ) β 0) β π β€ π) |
29 | 28 | 3expia 1122 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
30 | 29 | ad2ant2rl 748 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β ((π΄βπ) β 0 β π β€ π)) |
31 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β (π΄βπ) = 0) |
32 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π΄βπ) = 0 β (π΄βπ) = 0)) |
33 | 31, 32 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β (π = π β (π΄βπ) = 0)) |
34 | 33 | necon3d 2965 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β ((π΄βπ) β 0 β π β π)) |
35 | 30, 34 | jcad 514 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β ((π΄βπ) β 0 β (π β€ π β§ π β π))) |
36 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β) |
37 | 36 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β π β
β) |
38 | 21 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β π β
β) |
39 | 37, 38 | ltlend 11307 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β (π < π β (π β€ π β§ π β π))) |
40 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β€) |
41 | 40 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β π β
β€) |
42 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β€) |
43 | 42 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β π β
β€) |
44 | | zltlem1 12563 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β€) β (π < π β π β€ (π β 1))) |
45 | 41, 43, 44 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β (π < π β π β€ (π β 1))) |
46 | 39, 45 | bitr3d 281 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β ((π β€ π β§ π β π) β π β€ (π β 1))) |
47 | 35, 46 | sylibd 238 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ (π β β β§ π β β0)) β ((π΄βπ) β 0 β π β€ (π β 1))) |
48 | 47 | expr 458 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β (π β β0 β ((π΄βπ) β 0 β π β€ (π β 1)))) |
49 | 48 | ralrimiv 3143 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β βπ β β0
((π΄βπ) β 0 β π β€ (π β 1))) |
50 | 1 | coef3 25609 |
. . . . . . . . . . . . . . 15
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β π΄:β0βΆβ) |
52 | | plyco0 25569 |
. . . . . . . . . . . . . 14
β’ (((π β 1) β
β0 β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β((π β 1) + 1))) = {0} β
βπ β
β0 ((π΄βπ) β 0 β π β€ (π β 1)))) |
53 | 27, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β ((π΄ β
(β€β₯β((π β 1) + 1))) = {0} β
βπ β
β0 ((π΄βπ) β 0 β π β€ (π β 1)))) |
54 | 49, 53 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β (π΄ β
(β€β₯β((π β 1) + 1))) = {0}) |
55 | 1, 6 | dgrlb 25613 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyβπ) β§ (π β 1) β β0 β§
(π΄ β
(β€β₯β((π β 1) + 1))) = {0}) β π β€ (π β 1)) |
56 | 25, 27, 54, 55 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β π β€ (π β 1)) |
57 | 22, 24, 56 | lensymd 11313 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β§ π β β) β Β¬ (π β 1) < π) |
58 | 20, 57 | pm2.65da 816 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β Β¬ π β β) |
59 | | dgrcl 25610 |
. . . . . . . . . . . . 13
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
60 | 6, 59 | eqeltrid 2842 |
. . . . . . . . . . . 12
β’ (πΉ β (Polyβπ) β π β
β0) |
61 | 60 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β π β
β0) |
62 | | elnn0 12422 |
. . . . . . . . . . 11
β’ (π β β0
β (π β β
β¨ π =
0)) |
63 | 61, 62 | sylib 217 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (π β β β¨ π = 0)) |
64 | 63 | ord 863 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (Β¬ π β β β π = 0)) |
65 | 58, 64 | mpd 15 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β π = 0) |
66 | 65 | fveq2d 6851 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (π΄βπ) = (π΄β0)) |
67 | | simpr 486 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (π΄βπ) = 0) |
68 | 17, 66, 67 | 3eqtr2d 2783 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (πΉβ0) = 0) |
69 | 68 | sneqd 4603 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β {(πΉβ0)} = {0}) |
70 | 69 | xpeq2d 5668 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (β Γ {(πΉβ0)}) = (β Γ
{0})) |
71 | 6, 65 | eqtr3id 2791 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β (degβπΉ) = 0) |
72 | | 0dgrb 25623 |
. . . . . 6
β’ (πΉ β (Polyβπ) β ((degβπΉ) = 0 β πΉ = (β Γ {(πΉβ0)}))) |
73 | 72 | adantr 482 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β ((degβπΉ) = 0 β πΉ = (β Γ {(πΉβ0)}))) |
74 | 71, 73 | mpbid 231 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β πΉ = (β Γ {(πΉβ0)})) |
75 | | df-0p 25050 |
. . . . 5
β’
0π = (β Γ {0}) |
76 | 75 | a1i 11 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β 0π =
(β Γ {0})) |
77 | 70, 74, 76 | 3eqtr4d 2787 |
. . 3
β’ ((πΉ β (Polyβπ) β§ (π΄βπ) = 0) β πΉ = 0π) |
78 | 77 | ex 414 |
. 2
β’ (πΉ β (Polyβπ) β ((π΄βπ) = 0 β πΉ = 0π)) |
79 | 15, 78 | impbid2 225 |
1
β’ (πΉ β (Polyβπ) β (πΉ = 0π β (π΄βπ) = 0)) |