Step | Hyp | Ref
| Expression |
1 | | simpr 483 |
. . . 4
β’ ((π β§ πΉ = (0gβπ)) β πΉ = (0gβπ)) |
2 | | ply1degltlss.d |
. . . . . . . . . 10
β’ π· = ( deg1
βπ
) |
3 | | ply1degltlss.p |
. . . . . . . . . 10
β’ π = (Poly1βπ
) |
4 | | ply1degltel.1 |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
5 | 2, 3, 4 | deg1xrf 26030 |
. . . . . . . . 9
β’ π·:π΅βΆβ* |
6 | 5 | a1i 11 |
. . . . . . . 8
β’ (π β π·:π΅βΆβ*) |
7 | 6 | ffnd 6718 |
. . . . . . 7
β’ (π β π· Fn π΅) |
8 | | ply1degltlss.2 |
. . . . . . . 8
β’ (π β π
β Ring) |
9 | 3 | ply1ring 22170 |
. . . . . . . 8
β’ (π
β Ring β π β Ring) |
10 | | eqid 2725 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
11 | 4, 10 | ring0cl 20202 |
. . . . . . . 8
β’ (π β Ring β
(0gβπ)
β π΅) |
12 | 8, 9, 11 | 3syl 18 |
. . . . . . 7
β’ (π β (0gβπ) β π΅) |
13 | 2, 3, 10 | deg1z 26036 |
. . . . . . . . 9
β’ (π
β Ring β (π·β(0gβπ)) = -β) |
14 | 8, 13 | syl 17 |
. . . . . . . 8
β’ (π β (π·β(0gβπ)) = -β) |
15 | | mnfxr 11296 |
. . . . . . . . . 10
β’ -β
β β* |
16 | 15 | a1i 11 |
. . . . . . . . 9
β’ (π β -β β
β*) |
17 | | ply1degltlss.3 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
18 | 17 | nn0red 12558 |
. . . . . . . . . 10
β’ (π β π β β) |
19 | 18 | rexrd 11289 |
. . . . . . . . 9
β’ (π β π β
β*) |
20 | 16 | xrleidd 13158 |
. . . . . . . . 9
β’ (π β -β β€
-β) |
21 | 18 | mnfltd 13131 |
. . . . . . . . 9
β’ (π β -β < π) |
22 | 16, 19, 16, 20, 21 | elicod 13401 |
. . . . . . . 8
β’ (π β -β β
(-β[,)π)) |
23 | 14, 22 | eqeltrd 2825 |
. . . . . . 7
β’ (π β (π·β(0gβπ)) β (-β[,)π)) |
24 | 7, 12, 23 | elpreimad 7061 |
. . . . . 6
β’ (π β (0gβπ) β (β‘π· β (-β[,)π))) |
25 | | ply1degltlss.1 |
. . . . . 6
β’ π = (β‘π· β (-β[,)π)) |
26 | 24, 25 | eleqtrrdi 2836 |
. . . . 5
β’ (π β (0gβπ) β π) |
27 | 26 | adantr 479 |
. . . 4
β’ ((π β§ πΉ = (0gβπ)) β (0gβπ) β π) |
28 | 1, 27 | eqeltrd 2825 |
. . 3
β’ ((π β§ πΉ = (0gβπ)) β πΉ β π) |
29 | | cnvimass 6081 |
. . . . . 6
β’ (β‘π· β (-β[,)π)) β dom π· |
30 | 25, 29 | eqsstri 4008 |
. . . . 5
β’ π β dom π· |
31 | 5 | fdmi 6728 |
. . . . 5
β’ dom π· = π΅ |
32 | 30, 31 | sseqtri 4010 |
. . . 4
β’ π β π΅ |
33 | 32, 28 | sselid 3971 |
. . 3
β’ ((π β§ πΉ = (0gβπ)) β πΉ β π΅) |
34 | 1 | fveq2d 6894 |
. . . . 5
β’ ((π β§ πΉ = (0gβπ)) β (π·βπΉ) = (π·β(0gβπ))) |
35 | 14 | adantr 479 |
. . . . 5
β’ ((π β§ πΉ = (0gβπ)) β (π·β(0gβπ)) = -β) |
36 | 34, 35 | eqtrd 2765 |
. . . 4
β’ ((π β§ πΉ = (0gβπ)) β (π·βπΉ) = -β) |
37 | | 1red 11240 |
. . . . . . . 8
β’ (π β 1 β
β) |
38 | 18, 37 | resubcld 11667 |
. . . . . . 7
β’ (π β (π β 1) β β) |
39 | 38 | rexrd 11289 |
. . . . . 6
β’ (π β (π β 1) β
β*) |
40 | 39 | adantr 479 |
. . . . 5
β’ ((π β§ πΉ = (0gβπ)) β (π β 1) β
β*) |
41 | 40 | mnfled 13142 |
. . . 4
β’ ((π β§ πΉ = (0gβπ)) β -β β€ (π β 1)) |
42 | 36, 41 | eqbrtrd 5166 |
. . 3
β’ ((π β§ πΉ = (0gβπ)) β (π·βπΉ) β€ (π β 1)) |
43 | | pm5.1 822 |
. . 3
β’ ((πΉ β π β§ (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1))) β (πΉ β π β (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1)))) |
44 | 28, 33, 42, 43 | syl12anc 835 |
. 2
β’ ((π β§ πΉ = (0gβπ)) β (πΉ β π β (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1)))) |
45 | 25 | eleq2i 2817 |
. . . 4
β’ (πΉ β π β πΉ β (β‘π· β (-β[,)π))) |
46 | 7 | adantr 479 |
. . . . 5
β’ ((π β§ πΉ β (0gβπ)) β π· Fn π΅) |
47 | | elpreima 7060 |
. . . . 5
β’ (π· Fn π΅ β (πΉ β (β‘π· β (-β[,)π)) β (πΉ β π΅ β§ (π·βπΉ) β (-β[,)π)))) |
48 | 46, 47 | syl 17 |
. . . 4
β’ ((π β§ πΉ β (0gβπ)) β (πΉ β (β‘π· β (-β[,)π)) β (πΉ β π΅ β§ (π·βπΉ) β (-β[,)π)))) |
49 | 45, 48 | bitrid 282 |
. . 3
β’ ((π β§ πΉ β (0gβπ)) β (πΉ β π β (πΉ β π΅ β§ (π·βπΉ) β (-β[,)π)))) |
50 | 15 | a1i 11 |
. . . . . . 7
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β -β β
β*) |
51 | 19 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β π β
β*) |
52 | | elico1 13394 |
. . . . . . 7
β’
((-β β β* β§ π β β*) β ((π·βπΉ) β (-β[,)π) β ((π·βπΉ) β β* β§ -β
β€ (π·βπΉ) β§ (π·βπΉ) < π))) |
53 | 50, 51, 52 | syl2anc 582 |
. . . . . 6
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β ((π·βπΉ) β (-β[,)π) β ((π·βπΉ) β β* β§ -β
β€ (π·βπΉ) β§ (π·βπΉ) < π))) |
54 | | df-3an 1086 |
. . . . . 6
β’ (((π·βπΉ) β β* β§ -β
β€ (π·βπΉ) β§ (π·βπΉ) < π) β (((π·βπΉ) β β* β§ -β
β€ (π·βπΉ)) β§ (π·βπΉ) < π)) |
55 | 53, 54 | bitrdi 286 |
. . . . 5
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β ((π·βπΉ) β (-β[,)π) β (((π·βπΉ) β β* β§ -β
β€ (π·βπΉ)) β§ (π·βπΉ) < π))) |
56 | 8 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β π
β Ring) |
57 | | simpr 483 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β πΉ β π΅) |
58 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β πΉ β (0gβπ)) |
59 | 2, 3, 10, 4 | deg1nn0cl 26037 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΉ β π΅ β§ πΉ β (0gβπ)) β (π·βπΉ) β
β0) |
60 | 56, 57, 58, 59 | syl3anc 1368 |
. . . . . . . . 9
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β (π·βπΉ) β
β0) |
61 | 60 | nn0red 12558 |
. . . . . . . 8
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β (π·βπΉ) β β) |
62 | 61 | rexrd 11289 |
. . . . . . 7
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β (π·βπΉ) β
β*) |
63 | 62 | mnfled 13142 |
. . . . . . 7
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β -β β€ (π·βπΉ)) |
64 | 62, 63 | jca 510 |
. . . . . 6
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β ((π·βπΉ) β β* β§ -β
β€ (π·βπΉ))) |
65 | 64 | biantrurd 531 |
. . . . 5
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β ((π·βπΉ) < π β (((π·βπΉ) β β* β§ -β
β€ (π·βπΉ)) β§ (π·βπΉ) < π))) |
66 | 60 | nn0zd 12609 |
. . . . . 6
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β (π·βπΉ) β β€) |
67 | 17 | nn0zd 12609 |
. . . . . . 7
β’ (π β π β β€) |
68 | 67 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β π β β€) |
69 | | zltlem1 12640 |
. . . . . 6
β’ (((π·βπΉ) β β€ β§ π β β€) β ((π·βπΉ) < π β (π·βπΉ) β€ (π β 1))) |
70 | 66, 68, 69 | syl2anc 582 |
. . . . 5
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β ((π·βπΉ) < π β (π·βπΉ) β€ (π β 1))) |
71 | 55, 65, 70 | 3bitr2d 306 |
. . . 4
β’ (((π β§ πΉ β (0gβπ)) β§ πΉ β π΅) β ((π·βπΉ) β (-β[,)π) β (π·βπΉ) β€ (π β 1))) |
72 | 71 | pm5.32da 577 |
. . 3
β’ ((π β§ πΉ β (0gβπ)) β ((πΉ β π΅ β§ (π·βπΉ) β (-β[,)π)) β (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1)))) |
73 | 49, 72 | bitrd 278 |
. 2
β’ ((π β§ πΉ β (0gβπ)) β (πΉ β π β (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1)))) |
74 | 44, 73 | pm2.61dane 3019 |
1
β’ (π β (πΉ β π β (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1)))) |