Step | Hyp | Ref
| Expression |
1 | | hbtlem3.ij |
. 2
β’ (π β πΌ β π½) |
2 | | hbtlem3.j |
. . . . . . 7
β’ (π β π½ β π) |
3 | | eqid 2727 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
4 | | hbtlem.u |
. . . . . . . 8
β’ π = (LIdealβπ) |
5 | 3, 4 | lidlss 21097 |
. . . . . . 7
β’ (π½ β π β π½ β (Baseβπ)) |
6 | 2, 5 | syl 17 |
. . . . . 6
β’ (π β π½ β (Baseβπ)) |
7 | 6 | sselda 3978 |
. . . . 5
β’ ((π β§ π β π½) β π β (Baseβπ)) |
8 | | eqid 2727 |
. . . . . 6
β’ (
deg1 βπ
) =
( deg1 βπ
) |
9 | | hbtlem.p |
. . . . . 6
β’ π = (Poly1βπ
) |
10 | 8, 9, 3 | deg1cl 26006 |
. . . . 5
β’ (π β (Baseβπ) β (( deg1
βπ
)βπ) β (β0
βͺ {-β})) |
11 | 7, 10 | syl 17 |
. . . 4
β’ ((π β§ π β π½) β (( deg1 βπ
)βπ) β (β0 βͺ
{-β})) |
12 | | elun 4144 |
. . . . 5
β’ (((
deg1 βπ
)βπ) β (β0 βͺ
{-β}) β ((( deg1 βπ
)βπ) β β0 β¨ ((
deg1 βπ
)βπ) β {-β})) |
13 | | nnssnn0 12497 |
. . . . . . 7
β’ β
β β0 |
14 | | nn0re 12503 |
. . . . . . . 8
β’ (((
deg1 βπ
)βπ) β β0 β ((
deg1 βπ
)βπ) β β) |
15 | | arch 12491 |
. . . . . . . 8
β’ (((
deg1 βπ
)βπ) β β β βπ β β ((
deg1 βπ
)βπ) < π) |
16 | 14, 15 | syl 17 |
. . . . . . 7
β’ (((
deg1 βπ
)βπ) β β0 β
βπ β β ((
deg1 βπ
)βπ) < π) |
17 | | ssrexv 4047 |
. . . . . . 7
β’ (β
β β0 β (βπ β β (( deg1
βπ
)βπ) < π β βπ β β0 ((
deg1 βπ
)βπ) < π)) |
18 | 13, 16, 17 | mpsyl 68 |
. . . . . 6
β’ (((
deg1 βπ
)βπ) β β0 β
βπ β
β0 (( deg1 βπ
)βπ) < π) |
19 | | elsni 4641 |
. . . . . . 7
β’ (((
deg1 βπ
)βπ) β {-β} β (( deg1
βπ
)βπ) = -β) |
20 | | 0nn0 12509 |
. . . . . . . . 9
β’ 0 β
β0 |
21 | | mnflt0 13129 |
. . . . . . . . 9
β’ -β
< 0 |
22 | | breq2 5146 |
. . . . . . . . . 10
β’ (π = 0 β (-β < π β -β <
0)) |
23 | 22 | rspcev 3607 |
. . . . . . . . 9
β’ ((0
β β0 β§ -β < 0) β βπ β β0
-β < π) |
24 | 20, 21, 23 | mp2an 691 |
. . . . . . . 8
β’
βπ β
β0 -β < π |
25 | | breq1 5145 |
. . . . . . . . 9
β’ (((
deg1 βπ
)βπ) = -β β ((( deg1
βπ
)βπ) < π β -β < π)) |
26 | 25 | rexbidv 3173 |
. . . . . . . 8
β’ (((
deg1 βπ
)βπ) = -β β (βπ β β0 ((
deg1 βπ
)βπ) < π β βπ β β0 -β <
π)) |
27 | 24, 26 | mpbiri 258 |
. . . . . . 7
β’ (((
deg1 βπ
)βπ) = -β β βπ β β0 ((
deg1 βπ
)βπ) < π) |
28 | 19, 27 | syl 17 |
. . . . . 6
β’ (((
deg1 βπ
)βπ) β {-β} β βπ β β0 ((
deg1 βπ
)βπ) < π) |
29 | 18, 28 | jaoi 856 |
. . . . 5
β’ ((((
deg1 βπ
)βπ) β β0 β¨ ((
deg1 βπ
)βπ) β {-β}) β βπ β β0 ((
deg1 βπ
)βπ) < π) |
30 | 12, 29 | sylbi 216 |
. . . 4
β’ (((
deg1 βπ
)βπ) β (β0 βͺ
{-β}) β βπ
β β0 (( deg1 βπ
)βπ) < π) |
31 | 11, 30 | syl 17 |
. . 3
β’ ((π β§ π β π½) β βπ β β0 ((
deg1 βπ
)βπ) < π) |
32 | | breq2 5146 |
. . . . . . . . . . 11
β’ (π = 0 β ((( deg1
βπ
)βπ) < π β (( deg1 βπ
)βπ) < 0)) |
33 | 32 | imbi1d 341 |
. . . . . . . . . 10
β’ (π = 0 β (((( deg1
βπ
)βπ) < π β π β πΌ) β ((( deg1 βπ
)βπ) < 0 β π β πΌ))) |
34 | 33 | ralbidv 3172 |
. . . . . . . . 9
β’ (π = 0 β (βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ) β βπ β π½ ((( deg1 βπ
)βπ) < 0 β π β πΌ))) |
35 | 34 | imbi2d 340 |
. . . . . . . 8
β’ (π = 0 β ((π β βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β (π β βπ β π½ ((( deg1 βπ
)βπ) < 0 β π β πΌ)))) |
36 | | breq2 5146 |
. . . . . . . . . . 11
β’ (π = π β ((( deg1 βπ
)βπ) < π β (( deg1 βπ
)βπ) < π)) |
37 | 36 | imbi1d 341 |
. . . . . . . . . 10
β’ (π = π β (((( deg1 βπ
)βπ) < π β π β πΌ) β ((( deg1 βπ
)βπ) < π β π β πΌ))) |
38 | 37 | ralbidv 3172 |
. . . . . . . . 9
β’ (π = π β (βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ) β βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ))) |
39 | 38 | imbi2d 340 |
. . . . . . . 8
β’ (π = π β ((π β βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β (π β βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)))) |
40 | | breq2 5146 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β ((( deg1 βπ
)βπ) < π β (( deg1 βπ
)βπ) < (π + 1))) |
41 | 40 | imbi1d 341 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (((( deg1
βπ
)βπ) < π β π β πΌ) β ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ))) |
42 | 41 | ralbidv 3172 |
. . . . . . . . . 10
β’ (π = (π + 1) β (βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ) β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ))) |
43 | | fveq2 6891 |
. . . . . . . . . . . . 13
β’ (π = π β (( deg1 βπ
)βπ) = (( deg1 βπ
)βπ)) |
44 | 43 | breq1d 5152 |
. . . . . . . . . . . 12
β’ (π = π β ((( deg1 βπ
)βπ) < (π + 1) β (( deg1 βπ
)βπ) < (π + 1))) |
45 | | eleq1 2816 |
. . . . . . . . . . . 12
β’ (π = π β (π β πΌ β π β πΌ)) |
46 | 44, 45 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π = π β (((( deg1 βπ
)βπ) < (π + 1) β π β πΌ) β ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ))) |
47 | 46 | cbvralvw 3229 |
. . . . . . . . . 10
β’
(βπ β
π½ ((( deg1
βπ
)βπ) < (π + 1) β π β πΌ) β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ)) |
48 | 42, 47 | bitrdi 287 |
. . . . . . . . 9
β’ (π = (π + 1) β (βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ) β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ))) |
49 | 48 | imbi2d 340 |
. . . . . . . 8
β’ (π = (π + 1) β ((π β βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β (π β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ)))) |
50 | | hbtlem3.r |
. . . . . . . . . . . 12
β’ (π β π
β Ring) |
51 | 50 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β§ π β π½) β π
β Ring) |
52 | | eqid 2727 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
53 | 8, 9, 52, 3 | deg1lt0 26014 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ π β (Baseβπ)) β ((( deg1
βπ
)βπ) < 0 β π = (0gβπ))) |
54 | 51, 7, 53 | syl2anc 583 |
. . . . . . . . . 10
β’ ((π β§ π β π½) β ((( deg1 βπ
)βπ) < 0 β π = (0gβπ))) |
55 | 9 | ply1ring 22153 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π β Ring) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β Ring) |
57 | | hbtlem3.i |
. . . . . . . . . . . . 13
β’ (π β πΌ β π) |
58 | 4, 52 | lidl0cl 21105 |
. . . . . . . . . . . . 13
β’ ((π β Ring β§ πΌ β π) β (0gβπ) β πΌ) |
59 | 56, 57, 58 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (π β (0gβπ) β πΌ) |
60 | | eleq1a 2823 |
. . . . . . . . . . . 12
β’
((0gβπ) β πΌ β (π = (0gβπ) β π β πΌ)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π = (0gβπ) β π β πΌ)) |
62 | 61 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β π½) β (π = (0gβπ) β π β πΌ)) |
63 | 54, 62 | sylbid 239 |
. . . . . . . . 9
β’ ((π β§ π β π½) β ((( deg1 βπ
)βπ) < 0 β π β πΌ)) |
64 | 63 | ralrimiva 3141 |
. . . . . . . 8
β’ (π β βπ β π½ ((( deg1 βπ
)βπ) < 0 β π β πΌ)) |
65 | 6 | 3ad2ant2 1132 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β π½ β (Baseβπ)) |
66 | 65 | sselda 3978 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β π β (Baseβπ)) |
67 | 8, 9, 3 | deg1cl 26006 |
. . . . . . . . . . . . . 14
β’ (π β (Baseβπ) β (( deg1
βπ
)βπ) β (β0
βͺ {-β})) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β (( deg1 βπ
)βπ) β (β0 βͺ
{-β})) |
69 | | simpl1 1189 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β π β β0) |
70 | 69 | nn0zd 12606 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β π β β€) |
71 | | degltp1le 25996 |
. . . . . . . . . . . . 13
β’ ((((
deg1 βπ
)βπ) β (β0 βͺ
{-β}) β§ π β
β€) β ((( deg1 βπ
)βπ) < (π + 1) β (( deg1 βπ
)βπ) β€ π)) |
72 | 68, 70, 71 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β ((( deg1 βπ
)βπ) < (π + 1) β (( deg1 βπ
)βπ) β€ π)) |
73 | | hbtlem5.e |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ₯ β β0 ((πβπ½)βπ₯) β ((πβπΌ)βπ₯)) |
74 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β ((πβπ½)βπ₯) = ((πβπ½)βπ)) |
75 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β ((πβπΌ)βπ₯) = ((πβπΌ)βπ)) |
76 | 74, 75 | sseq12d 4011 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β (((πβπ½)βπ₯) β ((πβπΌ)βπ₯) β ((πβπ½)βπ) β ((πβπΌ)βπ))) |
77 | 76 | rspcva 3605 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ βπ₯ β
β0 ((πβπ½)βπ₯) β ((πβπΌ)βπ₯)) β ((πβπ½)βπ) β ((πβπΌ)βπ)) |
78 | 73, 77 | sylan2 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π) β ((πβπ½)βπ) β ((πβπΌ)βπ)) |
79 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ π) β π
β Ring) |
80 | 2 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ π) β π½ β π) |
81 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ π) β π β
β0) |
82 | | hbtlem.s |
. . . . . . . . . . . . . . . . . . . 20
β’ π = (ldgIdlSeqβπ
) |
83 | 9, 4, 82, 8 | hbtlem1 42469 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Ring β§ π½ β π β§ π β β0) β ((πβπ½)βπ) = {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
84 | 79, 80, 81, 83 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π) β ((πβπ½)βπ) = {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
85 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ π) β πΌ β π) |
86 | 9, 4, 82, 8 | hbtlem1 42469 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
87 | 79, 85, 81, 86 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
88 | 78, 84, 87 | 3sstr3d 4024 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π) β {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
89 | 88 | 3adant3 1130 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
91 | | simpl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π½ β§ (( deg1 βπ
)βπ) β€ π) β π β π½) |
92 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π½ β§ (( deg1 βπ
)βπ) β€ π) β (( deg1 βπ
)βπ) β€ π) |
93 | | eqidd 2728 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π½ β§ (( deg1 βπ
)βπ) β€ π) β ((coe1βπ)βπ) = ((coe1βπ)βπ)) |
94 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (( deg1 βπ
)βπ) = (( deg1 βπ
)βπ)) |
95 | 94 | breq1d 5152 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((( deg1 βπ
)βπ) β€ π β (( deg1 βπ
)βπ) β€ π)) |
96 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (coe1βπ) = (coe1βπ)) |
97 | 96 | fveq1d 6893 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((coe1βπ)βπ) = ((coe1βπ)βπ)) |
98 | 97 | eqeq2d 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((coe1βπ)βπ) = ((coe1βπ)βπ) β ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
99 | 95, 98 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) |
100 | 99 | rspcev 3607 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π½ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) β βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
101 | 91, 92, 93, 100 | syl12anc 836 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π½ β§ (( deg1 βπ
)βπ) β€ π) β βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
102 | | fvex 6904 |
. . . . . . . . . . . . . . . . . 18
β’
((coe1βπ)βπ) β V |
103 | | eqeq1 2731 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = ((coe1βπ)βπ) β (π = ((coe1βπ)βπ) β ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
104 | 103 | anbi2d 628 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = ((coe1βπ)βπ) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) |
105 | 104 | rexbidv 3173 |
. . . . . . . . . . . . . . . . . 18
β’ (π = ((coe1βπ)βπ) β (βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) |
106 | 102, 105 | elab 3665 |
. . . . . . . . . . . . . . . . 17
β’
(((coe1βπ)βπ) β {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
107 | 101, 106 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((π β π½ β§ (( deg1 βπ
)βπ) β€ π) β ((coe1βπ)βπ) β {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β ((coe1βπ)βπ) β {π β£ βπ β π½ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
109 | 90, 108 | sseldd 3979 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β ((coe1βπ)βπ) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
110 | 104 | rexbidv 3173 |
. . . . . . . . . . . . . . . 16
β’ (π = ((coe1βπ)βπ) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) |
111 | 102, 110 | elab 3665 |
. . . . . . . . . . . . . . 15
β’
(((coe1βπ)βπ) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ))) |
112 | | simpll2 1211 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π) |
113 | 112, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β Ring) |
114 | | ringgrp 20169 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Ring β π β Grp) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β Grp) |
116 | 112, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π½ β (Baseβπ)) |
117 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β π½) |
118 | 116, 117 | sseldd 3979 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β (Baseβπ)) |
119 | 3, 4 | lidlss 21097 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΌ β π β πΌ β (Baseβπ)) |
120 | 57, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΌ β (Baseβπ)) |
121 | 112, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β πΌ β (Baseβπ)) |
122 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β πΌ) |
123 | 121, 122 | sseldd 3979 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β (Baseβπ)) |
124 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . 19
β’
(+gβπ) = (+gβπ) |
125 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . 19
β’
(-gβπ) = (-gβπ) |
126 | 3, 124, 125 | grpnpcan 18979 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Grp β§ π β (Baseβπ) β§ π β (Baseβπ)) β ((π(-gβπ)π)(+gβπ)π) = π) |
127 | 115, 118,
123, 126 | syl3anc 1369 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β ((π(-gβπ)π)(+gβπ)π) = π) |
128 | 57 | 3ad2ant2 1132 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β πΌ β π) |
129 | 128 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β πΌ β π) |
130 | | simpll1 1210 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β β0) |
131 | 112, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π
β Ring) |
132 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β (( deg1 βπ
)βπ) β€ π) |
133 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β (( deg1 βπ
)βπ) β€ π) |
134 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . . 20
β’
(coe1βπ) = (coe1βπ) |
135 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . . 20
β’
(coe1βπ) = (coe1βπ) |
136 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β ((coe1βπ)βπ) = ((coe1βπ)βπ)) |
137 | 8, 9, 3, 125, 130, 131, 118, 132, 123, 133, 134, 135, 136 | deg1sublt 26033 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β (( deg1 βπ
)β(π(-gβπ)π)) < π) |
138 | 112, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π½ β π) |
139 | 1 | 3ad2ant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β πΌ β π½) |
140 | 139 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β πΌ β π½) |
141 | 140, 122 | sseldd 3979 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β π½) |
142 | 4, 125 | lidlsubcl 21109 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β Ring β§ π½ β π) β§ (π β π½ β§ π β π½)) β (π(-gβπ)π) β π½) |
143 | 113, 138,
117, 141, 142 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β (π(-gβπ)π) β π½) |
144 | | simpll3 1212 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) |
145 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π(-gβπ)π) β (( deg1 βπ
)βπ) = (( deg1 βπ
)β(π(-gβπ)π))) |
146 | 145 | breq1d 5152 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π(-gβπ)π) β ((( deg1 βπ
)βπ) < π β (( deg1 βπ
)β(π(-gβπ)π)) < π)) |
147 | | eleq1 2816 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π(-gβπ)π) β (π β πΌ β (π(-gβπ)π) β πΌ)) |
148 | 146, 147 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π(-gβπ)π) β (((( deg1 βπ
)βπ) < π β π β πΌ) β ((( deg1 βπ
)β(π(-gβπ)π)) < π β (π(-gβπ)π) β πΌ))) |
149 | 148 | rspcva 3605 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π(-gβπ)π) β π½ β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β ((( deg1 βπ
)β(π(-gβπ)π)) < π β (π(-gβπ)π) β πΌ)) |
150 | 143, 144,
149 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β ((( deg1 βπ
)β(π(-gβπ)π)) < π β (π(-gβπ)π) β πΌ)) |
151 | 137, 150 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β (π(-gβπ)π) β πΌ) |
152 | 4, 124 | lidlacl 21106 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Ring β§ πΌ β π) β§ ((π(-gβπ)π) β πΌ β§ π β πΌ)) β ((π(-gβπ)π)(+gβπ)π) β πΌ) |
153 | 113, 129,
151, 122, 152 | syl22anc 838 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β ((π(-gβπ)π)(+gβπ)π) β πΌ) |
154 | 127, 153 | eqeltrrd 2829 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β§ (π β πΌ β§ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)))) β π β πΌ) |
155 | 154 | rexlimdvaa 3151 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((coe1βπ)βπ) = ((coe1βπ)βπ)) β π β πΌ)) |
156 | 111, 155 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β (((coe1βπ)βπ) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β π β πΌ)) |
157 | 109, 156 | mpd 15 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ (π β π½ β§ (( deg1 βπ
)βπ) β€ π)) β π β πΌ) |
158 | 157 | expr 456 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β ((( deg1 βπ
)βπ) β€ π β π β πΌ)) |
159 | 72, 158 | sylbid 239 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β§ π β π½) β ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ)) |
160 | 159 | ralrimiva 3141 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β§ βπ β π½ ((( deg1 βπ
)βπ) < π β π β πΌ)) β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ)) |
161 | 160 | 3exp 1117 |
. . . . . . . . 9
β’ (π β β0
β (π β
(βπ β π½ ((( deg1
βπ
)βπ) < π β π β πΌ) β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ)))) |
162 | 161 | a2d 29 |
. . . . . . . 8
β’ (π β β0
β ((π β
βπ β π½ ((( deg1
βπ
)βπ) < π β π β πΌ)) β (π β βπ β π½ ((( deg1 βπ
)βπ) < (π + 1) β π β πΌ)))) |
163 | 35, 39, 49, 39, 64, 162 | nn0ind 12679 |
. . . . . . 7
β’ (π β β0
β (π β
βπ β π½ ((( deg1
βπ
)βπ) < π β π β πΌ))) |
164 | | rsp 3239 |
. . . . . . 7
β’
(βπ β
π½ ((( deg1
βπ
)βπ) < π β π β πΌ) β (π β π½ β ((( deg1 βπ
)βπ) < π β π β πΌ))) |
165 | 163, 164 | syl6com 37 |
. . . . . 6
β’ (π β (π β β0 β (π β π½ β ((( deg1 βπ
)βπ) < π β π β πΌ)))) |
166 | 165 | com23 86 |
. . . . 5
β’ (π β (π β π½ β (π β β0 β (((
deg1 βπ
)βπ) < π β π β πΌ)))) |
167 | 166 | imp 406 |
. . . 4
β’ ((π β§ π β π½) β (π β β0 β (((
deg1 βπ
)βπ) < π β π β πΌ))) |
168 | 167 | rexlimdv 3148 |
. . 3
β’ ((π β§ π β π½) β (βπ β β0 ((
deg1 βπ
)βπ) < π β π β πΌ)) |
169 | 31, 168 | mpd 15 |
. 2
β’ ((π β§ π β π½) β π β πΌ) |
170 | 1, 169 | eqelssd 3999 |
1
β’ (π β πΌ = π½) |