Step | Hyp | Ref
| Expression |
1 | | hbtlem3.ij |
. 2
|
2 | | hbtlem3.j |
. . . . . . . . 9
|
3 | | eqid 2622 |
. . . . . . . . . 10
|
4 | | hbtlem.u |
. . . . . . . . . 10
LIdeal |
5 | 3, 4 | lidlss 19210 |
. . . . . . . . 9
|
6 | 2, 5 | syl 17 |
. . . . . . . 8
|
7 | 6 | sselda 3603 |
. . . . . . 7
|
8 | | eqid 2622 |
. . . . . . . 8
deg1 deg1 |
9 | | hbtlem.p |
. . . . . . . 8
Poly1 |
10 | 8, 9, 3 | deg1cl 23843 |
. . . . . . 7
deg1
|
11 | 7, 10 | syl 17 |
. . . . . 6
deg1 |
12 | | elun 3753 |
. . . . . . 7
deg1 deg1
deg1 |
13 | | nnssnn0 11295 |
. . . . . . . . 9
|
14 | | nn0re 11301 |
. . . . . . . . . 10
deg1
deg1 |
15 | | arch 11289 |
. . . . . . . . . 10
deg1
deg1 |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
deg1
deg1 |
17 | | ssrexv 3667 |
. . . . . . . . 9
deg1
deg1 |
18 | 13, 16, 17 | mpsyl 68 |
. . . . . . . 8
deg1
deg1 |
19 | | elsni 4194 |
. . . . . . . . 9
deg1
deg1 |
20 | | 0nn0 11307 |
. . . . . . . . . . 11
|
21 | | mnflt0 11959 |
. . . . . . . . . . 11
|
22 | | breq2 4657 |
. . . . . . . . . . . 12
|
23 | 22 | rspcev 3309 |
. . . . . . . . . . 11
|
24 | 20, 21, 23 | mp2an 708 |
. . . . . . . . . 10
|
25 | | breq1 4656 |
. . . . . . . . . . 11
deg1 deg1
|
26 | 25 | rexbidv 3052 |
. . . . . . . . . 10
deg1 deg1 |
27 | 24, 26 | mpbiri 248 |
. . . . . . . . 9
deg1
deg1 |
28 | 19, 27 | syl 17 |
. . . . . . . 8
deg1
deg1 |
29 | 18, 28 | jaoi 394 |
. . . . . . 7
deg1
deg1 deg1 |
30 | 12, 29 | sylbi 207 |
. . . . . 6
deg1
deg1 |
31 | 11, 30 | syl 17 |
. . . . 5
deg1 |
32 | | breq2 4657 |
. . . . . . . . . . . . 13
deg1 deg1 |
33 | 32 | imbi1d 331 |
. . . . . . . . . . . 12
deg1
deg1 |
34 | 33 | ralbidv 2986 |
. . . . . . . . . . 11
deg1
deg1 |
35 | 34 | imbi2d 330 |
. . . . . . . . . 10
deg1
deg1 |
36 | | breq2 4657 |
. . . . . . . . . . . . 13
deg1 deg1 |
37 | 36 | imbi1d 331 |
. . . . . . . . . . . 12
deg1
deg1 |
38 | 37 | ralbidv 2986 |
. . . . . . . . . . 11
deg1
deg1 |
39 | 38 | imbi2d 330 |
. . . . . . . . . 10
deg1
deg1 |
40 | | breq2 4657 |
. . . . . . . . . . . . . 14
deg1 deg1 |
41 | 40 | imbi1d 331 |
. . . . . . . . . . . . 13
deg1
deg1 |
42 | 41 | ralbidv 2986 |
. . . . . . . . . . . 12
deg1
deg1 |
43 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
deg1 deg1 |
44 | 43 | breq1d 4663 |
. . . . . . . . . . . . . 14
deg1
deg1 |
45 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
46 | 44, 45 | imbi12d 334 |
. . . . . . . . . . . . 13
deg1
deg1 |
47 | 46 | cbvralv 3171 |
. . . . . . . . . . . 12
deg1 deg1
|
48 | 42, 47 | syl6bb 276 |
. . . . . . . . . . 11
deg1
deg1 |
49 | 48 | imbi2d 330 |
. . . . . . . . . 10
deg1
deg1 |
50 | | hbtlem3.r |
. . . . . . . . . . . . . 14
|
51 | 50 | adantr 481 |
. . . . . . . . . . . . 13
|
52 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
53 | 8, 9, 52, 3 | deg1lt0 23851 |
. . . . . . . . . . . . 13
deg1 |
54 | 51, 7, 53 | syl2anc 693 |
. . . . . . . . . . . 12
deg1 |
55 | 9 | ply1ring 19618 |
. . . . . . . . . . . . . . . 16
|
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . 15
|
57 | | hbtlem3.i |
. . . . . . . . . . . . . . 15
|
58 | 4, 52 | lidl0cl 19212 |
. . . . . . . . . . . . . . 15
|
59 | 56, 57, 58 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
60 | | eleq1a 2696 |
. . . . . . . . . . . . . 14
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
|
62 | 61 | adantr 481 |
. . . . . . . . . . . 12
|
63 | 54, 62 | sylbid 230 |
. . . . . . . . . . 11
deg1 |
64 | 63 | ralrimiva 2966 |
. . . . . . . . . 10
deg1
|
65 | 6 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
deg1
|
66 | 65 | sselda 3603 |
. . . . . . . . . . . . . . . 16
deg1 |
67 | 8, 9, 3 | deg1cl 23843 |
. . . . . . . . . . . . . . . 16
deg1
|
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . 15
deg1 deg1 |
69 | | simpl1 1064 |
. . . . . . . . . . . . . . . 16
deg1 |
70 | 69 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
deg1 |
71 | | degltp1le 23833 |
. . . . . . . . . . . . . . 15
deg1
deg1
deg1 |
72 | 68, 70, 71 | syl2anc 693 |
. . . . . . . . . . . . . 14
deg1
deg1
deg1 |
73 | | hbtlem5.e |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
75 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
76 | 74, 75 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . . . . . 22
|
77 | 76 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 73, 77 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 2 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
81 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | | hbtlem.s |
. . . . . . . . . . . . . . . . . . . . . 22
ldgIdlSeq |
83 | 9, 4, 82, 8 | hbtlem1 37693 |
. . . . . . . . . . . . . . . . . . . . 21
deg1
coe1 |
84 | 79, 80, 81, 83 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
deg1
coe1 |
85 | 57 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | 9, 4, 82, 8 | hbtlem1 37693 |
. . . . . . . . . . . . . . . . . . . . 21
deg1
coe1 |
87 | 79, 85, 81, 86 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
deg1
coe1 |
88 | 78, 84, 87 | 3sstr3d 3647 |
. . . . . . . . . . . . . . . . . . 19
deg1 coe1 deg1 coe1 |
89 | 88 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . 18
deg1
deg1
coe1 deg1 coe1 |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . 17
deg1 deg1 deg1
coe1
deg1
coe1 |
91 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
deg1
|
92 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
deg1
deg1
|
93 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
deg1
coe1 coe1 |
94 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1 deg1 |
95 | 94 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 |
96 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 coe1 |
97 | 96 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1 |
98 | 97 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1
coe1 coe1 |
99 | 95, 98 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 coe1 coe1
deg1 coe1 coe1 |
100 | 99 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . 20
deg1 coe1 coe1
deg1 coe1 coe1 |
101 | 91, 92, 93, 100 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . 19
deg1
deg1 coe1 coe1 |
102 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
coe1 |
103 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1
coe1 coe1 |
104 | 103 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 deg1
coe1
deg1 coe1 coe1 |
105 | 104 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . 20
coe1 deg1
coe1
deg1 coe1 coe1 |
106 | 102, 105 | elab 3350 |
. . . . . . . . . . . . . . . . . . 19
coe1
deg1
coe1
deg1 coe1 coe1 |
107 | 101, 106 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
deg1
coe1 deg1
coe1 |
108 | 107 | adantl 482 |
. . . . . . . . . . . . . . . . 17
deg1 deg1 coe1
deg1
coe1 |
109 | 90, 108 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
deg1 deg1 coe1
deg1
coe1 |
110 | 104 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . 18
coe1 deg1
coe1
deg1 coe1 coe1 |
111 | 102, 110 | elab 3350 |
. . . . . . . . . . . . . . . . 17
coe1
deg1
coe1
deg1 coe1 coe1 |
112 | | simpll2 1101 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 |
113 | 112, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 |
114 | | ringgrp 18552 |
. . . . . . . . . . . . . . . . . . . . 21
|
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
deg1 deg1 deg1 coe1 coe1 |
116 | 112, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 |
117 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 |
118 | 116, 117 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
deg1 deg1 deg1 coe1 coe1 |
119 | 3, 4 | lidlss 19210 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
120 | 57, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
121 | 112, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 |
122 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 |
123 | 121, 122 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
deg1 deg1 deg1 coe1 coe1 |
124 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
125 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
126 | 3, 124, 125 | grpnpcan 17507 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 115, 118,
123, 126 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
deg1 deg1 deg1 coe1 coe1 |
128 | 57 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . 21
deg1
|
129 | 128 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
deg1 deg1 deg1 coe1 coe1 |
130 | | simpll1 1100 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 |
131 | 112, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 |
132 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 deg1 |
133 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 deg1 |
134 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1 |
135 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1 |
136 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 coe1 coe1 |
137 | 8, 9, 3, 125, 130, 131, 118, 132, 123, 133, 134, 135, 136 | deg1sublt 23870 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 deg1 |
138 | 112, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1 deg1 deg1 coe1 coe1 |
139 | 1 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
deg1
|
140 | 139 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1 deg1 deg1 coe1 coe1 |
141 | 140, 122 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1 deg1 deg1 coe1 coe1 |
142 | 4, 125 | lidlsubcl 19216 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
143 | 113, 138,
117, 141, 142 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 |
144 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1 deg1 deg1 coe1 coe1 deg1
|
145 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
deg1 deg1 |
146 | 145 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1 deg1 |
147 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 146, 147 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg1
deg1 |
149 | 148 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . . 22
deg1
deg1 |
150 | 143, 144,
149 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
deg1 deg1 deg1 coe1 coe1 deg1 |
151 | 137, 150 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
deg1 deg1 deg1 coe1 coe1 |
152 | 4, 124 | lidlacl 19213 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | 113, 129,
151, 122, 152 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . 19
deg1 deg1 deg1 coe1 coe1 |
154 | 127, 153 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
deg1 deg1 deg1 coe1 coe1 |
155 | 154 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . . . 17
deg1 deg1
deg1 coe1 coe1 |
156 | 111, 155 | syl5bi 232 |
. . . . . . . . . . . . . . . 16
deg1 deg1 coe1
deg1
coe1 |
157 | 109, 156 | mpd 15 |
. . . . . . . . . . . . . . 15
deg1 deg1 |
158 | 157 | expr 643 |
. . . . . . . . . . . . . 14
deg1
deg1 |
159 | 72, 158 | sylbid 230 |
. . . . . . . . . . . . 13
deg1
deg1 |
160 | 159 | ralrimiva 2966 |
. . . . . . . . . . . 12
deg1
deg1
|
161 | 160 | 3exp 1264 |
. . . . . . . . . . 11
deg1
deg1
|
162 | 161 | a2d 29 |
. . . . . . . . . 10
deg1
deg1 |
163 | 35, 39, 49, 39, 64, 162 | nn0ind 11472 |
. . . . . . . . 9
deg1
|
164 | | rsp 2929 |
. . . . . . . . 9
deg1
deg1 |
165 | 163, 164 | syl6com 37 |
. . . . . . . 8
deg1
|
166 | 165 | com23 86 |
. . . . . . 7
deg1
|
167 | 166 | imp 445 |
. . . . . 6
deg1 |
168 | 167 | rexlimdv 3030 |
. . . . 5
deg1 |
169 | 31, 168 | mpd 15 |
. . . 4
|
170 | 169 | ex 450 |
. . 3
|
171 | 170 | ssrdv 3609 |
. 2
|
172 | 1, 171 | eqssd 3620 |
1
|