Step | Hyp | Ref
| Expression |
1 | | sbequ 1761 |
. . . . . . 7
|
2 | 1 | anbi2d 451 |
. . . . . 6
|
3 | | sbequ 1761 |
. . . . . . . . . 10
|
4 | 3 | anbi1d 452 |
. . . . . . . . 9
|
5 | 4 | rexbidv 2369 |
. . . . . . . 8
|
6 | 5 | imbi2d 228 |
. . . . . . 7
|
7 | 6 | ralbidv 2368 |
. . . . . 6
|
8 | 2, 7 | imbi12d 232 |
. . . . 5
|
9 | | sbequ 1761 |
. . . . . . 7
|
10 | 9 | anbi2d 451 |
. . . . . 6
|
11 | | sbequ12r 1695 |
. . . . . . . . . 10
|
12 | 11 | anbi1d 452 |
. . . . . . . . 9
|
13 | 12 | rexbidv 2369 |
. . . . . . . 8
|
14 | 13 | imbi2d 228 |
. . . . . . 7
|
15 | 14 | ralbidv 2368 |
. . . . . 6
|
16 | 10, 15 | imbi12d 232 |
. . . . 5
|
17 | | nfv 1461 |
. . . . . . . . . . 11
|
18 | | nfcv 2219 |
. . . . . . . . . . . 12
|
19 | | nfv 1461 |
. . . . . . . . . . . . 13
|
20 | | nfra1 2397 |
. . . . . . . . . . . . 13
|
21 | 19, 20 | nfim 1504 |
. . . . . . . . . . . 12
|
22 | 18, 21 | nfralxy 2402 |
. . . . . . . . . . 11
|
23 | 17, 22 | nfan 1497 |
. . . . . . . . . 10
|
24 | | nfv 1461 |
. . . . . . . . . 10
|
25 | 23, 24 | nfan 1497 |
. . . . . . . . 9
|
26 | | nfv 1461 |
. . . . . . . . 9
|
27 | 25, 26 | nfan 1497 |
. . . . . . . 8
|
28 | | simplr 496 |
. . . . . . . . . 10
|
29 | | nfv 1461 |
. . . . . . . . . . . . . 14
|
30 | | breq2 3789 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | imbi1d 229 |
. . . . . . . . . . . . . . 15
|
32 | 31 | ralbidv 2368 |
. . . . . . . . . . . . . 14
|
33 | 29, 32 | sbie 1714 |
. . . . . . . . . . . . 13
|
34 | | nn0z 8371 |
. . . . . . . . . . . . . . . 16
|
35 | | dvds0 10210 |
. . . . . . . . . . . . . . . 16
|
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . . . 15
|
37 | 36 | biantrurd 299 |
. . . . . . . . . . . . . 14
|
38 | 37 | biimpd 142 |
. . . . . . . . . . . . 13
|
39 | 33, 38 | mprgbir 2421 |
. . . . . . . . . . . 12
|
40 | | nfv 1461 |
. . . . . . . . . . . . 13
|
41 | | dfsbcq2 2818 |
. . . . . . . . . . . . . 14
|
42 | | bezout.sub-gcd |
. . . . . . . . . . . . . . . 16
|
43 | 42 | sbcbii 2873 |
. . . . . . . . . . . . . . 15
|
44 | | c0ex 7113 |
. . . . . . . . . . . . . . . 16
|
45 | | breq2 3789 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 45 | anbi1d 452 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | imbi2d 228 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | ralbidv 2368 |
. . . . . . . . . . . . . . . 16
|
49 | 44, 48 | sbcie 2848 |
. . . . . . . . . . . . . . 15
|
50 | 43, 49 | bitri 182 |
. . . . . . . . . . . . . 14
|
51 | 41, 50 | syl6bb 194 |
. . . . . . . . . . . . 13
|
52 | 40, 51 | sbbid 1767 |
. . . . . . . . . . . 12
|
53 | 39, 52 | mpbiri 166 |
. . . . . . . . . . 11
|
54 | 53 | ad3antlr 476 |
. . . . . . . . . 10
|
55 | | simpr 108 |
. . . . . . . . . 10
|
56 | | nfs1v 1856 |
. . . . . . . . . . . 12
|
57 | | nfs1v 1856 |
. . . . . . . . . . . 12
|
58 | 56, 57 | nfan 1497 |
. . . . . . . . . . 11
|
59 | | sbequ12 1694 |
. . . . . . . . . . . 12
|
60 | | sbequ12 1694 |
. . . . . . . . . . . 12
|
61 | 59, 60 | anbi12d 456 |
. . . . . . . . . . 11
|
62 | 58, 61 | rspce 2696 |
. . . . . . . . . 10
|
63 | 28, 54, 55, 62 | syl12anc 1167 |
. . . . . . . . 9
|
64 | 63 | exp31 356 |
. . . . . . . 8
|
65 | 27, 64 | ralrimi 2432 |
. . . . . . 7
|
66 | | nfv 1461 |
. . . . . . . . . 10
|
67 | 25, 66 | nfan 1497 |
. . . . . . . . 9
|
68 | | bezout.is-bezout |
. . . . . . . . . . 11
|
69 | | simplrl 501 |
. . . . . . . . . . . . 13
|
70 | | bezout.a |
. . . . . . . . . . . . 13
|
71 | 69, 70 | syl 14 |
. . . . . . . . . . . 12
|
72 | 71 | ad2antrr 471 |
. . . . . . . . . . 11
|
73 | | bezout.b |
. . . . . . . . . . . . 13
|
74 | 69, 73 | syl 14 |
. . . . . . . . . . . 12
|
75 | 74 | ad2antrr 471 |
. . . . . . . . . . 11
|
76 | | simplll 499 |
. . . . . . . . . . . . 13
|
77 | | simpr 108 |
. . . . . . . . . . . . 13
|
78 | | elnnnn0b 8332 |
. . . . . . . . . . . . 13
|
79 | 76, 77, 78 | sylanbrc 408 |
. . . . . . . . . . . 12
|
80 | 79 | ad2antrr 471 |
. . . . . . . . . . 11
|
81 | | simpr 108 |
. . . . . . . . . . 11
|
82 | | simplr 496 |
. . . . . . . . . . 11
|
83 | | simplrr 502 |
. . . . . . . . . . . . 13
|
84 | | sbsbc 2819 |
. . . . . . . . . . . . 13
|
85 | 83, 84 | sylib 120 |
. . . . . . . . . . . 12
|
86 | 85 | ad2antrr 471 |
. . . . . . . . . . 11
|
87 | | breq1 3788 |
. . . . . . . . . . . . . 14
|
88 | | breq1 3788 |
. . . . . . . . . . . . . . 15
|
89 | | breq1 3788 |
. . . . . . . . . . . . . . 15
|
90 | 88, 89 | anbi12d 456 |
. . . . . . . . . . . . . 14
|
91 | 87, 90 | imbi12d 232 |
. . . . . . . . . . . . 13
|
92 | 91 | cbvralv 2577 |
. . . . . . . . . . . 12
|
93 | 42, 92 | bitri 182 |
. . . . . . . . . . 11
|
94 | 69 | ad3antrrr 475 |
. . . . . . . . . . . . 13
|
95 | | simpr 108 |
. . . . . . . . . . . . 13
|
96 | 94, 95 | jca 300 |
. . . . . . . . . . . 12
|
97 | 83 | ad3antrrr 475 |
. . . . . . . . . . . 12
|
98 | | simpllr 500 |
. . . . . . . . . . . . . . 15
|
99 | 98 | nn0zd 8467 |
. . . . . . . . . . . . . 14
|
100 | 79 | ad3antrrr 475 |
. . . . . . . . . . . . . 14
|
101 | | zmodfz 9348 |
. . . . . . . . . . . . . 14
|
102 | 99, 100, 101 | syl2anc 403 |
. . . . . . . . . . . . 13
|
103 | | simpll 495 |
. . . . . . . . . . . . . 14
|
104 | | simpr 108 |
. . . . . . . . . . . . . . . 16
|
105 | 104 | ad3antrrr 475 |
. . . . . . . . . . . . . . 15
|
106 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | | nfcv 2219 |
. . . . . . . . . . . . . . . . . . . . 21
|
108 | | nfs1v 1856 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
109 | 108 | nfsbxy 1859 |
. . . . . . . . . . . . . . . . . . . . . 22
|
110 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . . . 22
|
111 | 109, 110 | nfan 1497 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 107, 111 | nfrexxy 2403 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 106, 112 | nfim 1504 |
. . . . . . . . . . . . . . . . . . 19
|
114 | | sbequ 1761 |
. . . . . . . . . . . . . . . . . . . 20
|
115 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
116 | | sbequ12 1694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
117 | 115, 116 | sbbid 1767 |
. . . . . . . . . . . . . . . . . . . . . 22
|
118 | 117 | anbi1d 452 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 118 | rexbidv 2369 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | 114, 119 | imbi12d 232 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 113, 120 | rspc 2695 |
. . . . . . . . . . . . . . . . . 18
|
122 | 121 | imim2d 53 |
. . . . . . . . . . . . . . . . 17
|
123 | 122 | ralimdv 2430 |
. . . . . . . . . . . . . . . 16
|
124 | 123 | ad4antr 477 |
. . . . . . . . . . . . . . 15
|
125 | 105, 124 | mpd 13 |
. . . . . . . . . . . . . 14
|
126 | 103, 125 | sylan 277 |
. . . . . . . . . . . . 13
|
127 | | dfsbcq2 2818 |
. . . . . . . . . . . . . . . 16
|
128 | 127 | anbi2d 451 |
. . . . . . . . . . . . . . 15
|
129 | | sbsbc 2819 |
. . . . . . . . . . . . . . . . . . . 20
|
130 | | sbsbc 2819 |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | 130 | sbcbii 2873 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | 129, 131 | bitri 182 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 132 | anbi1i 445 |
. . . . . . . . . . . . . . . . . 18
|
134 | | dfsbcq 2817 |
. . . . . . . . . . . . . . . . . . 19
|
135 | 134 | anbi1d 452 |
. . . . . . . . . . . . . . . . . 18
|
136 | 133, 135 | syl5bb 190 |
. . . . . . . . . . . . . . . . 17
|
137 | 136 | rexbidv 2369 |
. . . . . . . . . . . . . . . 16
|
138 | 137 | imbi2d 228 |
. . . . . . . . . . . . . . 15
|
139 | 128, 138 | imbi12d 232 |
. . . . . . . . . . . . . 14
|
140 | 139 | rspcv 2697 |
. . . . . . . . . . . . 13
|
141 | 102, 126,
140 | sylc 61 |
. . . . . . . . . . . 12
|
142 | 96, 97, 141 | mp2d 46 |
. . . . . . . . . . 11
|
143 | | nfv 1461 |
. . . . . . . . . . . . . . . 16
|
144 | | nfcv 2219 |
. . . . . . . . . . . . . . . . 17
|
145 | | nfv 1461 |
. . . . . . . . . . . . . . . . . 18
|
146 | | nfcv 2219 |
. . . . . . . . . . . . . . . . . . 19
|
147 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . . 21
|
148 | 147 | nfsbxy 1859 |
. . . . . . . . . . . . . . . . . . . 20
|
149 | | nfs1v 1856 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | 149, 147 | nfan 1497 |
. . . . . . . . . . . . . . . . . . . . 21
|
151 | 146, 150 | nfrexxy 2403 |
. . . . . . . . . . . . . . . . . . . 20
|
152 | 148, 151 | nfim 1504 |
. . . . . . . . . . . . . . . . . . 19
|
153 | 146, 152 | nfralxy 2402 |
. . . . . . . . . . . . . . . . . 18
|
154 | 145, 153 | nfim 1504 |
. . . . . . . . . . . . . . . . 17
|
155 | 144, 154 | nfralxy 2402 |
. . . . . . . . . . . . . . . 16
|
156 | 143, 155 | nfan 1497 |
. . . . . . . . . . . . . . 15
|
157 | | nfv 1461 |
. . . . . . . . . . . . . . 15
|
158 | 156, 157 | nfan 1497 |
. . . . . . . . . . . . . 14
|
159 | | nfv 1461 |
. . . . . . . . . . . . . 14
|
160 | 158, 159 | nfan 1497 |
. . . . . . . . . . . . 13
|
161 | | nfv 1461 |
. . . . . . . . . . . . 13
|
162 | 160, 161 | nfan 1497 |
. . . . . . . . . . . 12
|
163 | 162, 148 | nfan 1497 |
. . . . . . . . . . 11
|
164 | | nfv 1461 |
. . . . . . . . . . . . . . . 16
|
165 | | nfcv 2219 |
. . . . . . . . . . . . . . . . 17
|
166 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . 19
|
167 | | nfs1v 1856 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 166, 167 | nfan 1497 |
. . . . . . . . . . . . . . . . . 18
|
169 | | nfcv 2219 |
. . . . . . . . . . . . . . . . . . 19
|
170 | | nfre1 2407 |
. . . . . . . . . . . . . . . . . . . 20
|
171 | 57, 170 | nfim 1504 |
. . . . . . . . . . . . . . . . . . 19
|
172 | 169, 171 | nfralxy 2402 |
. . . . . . . . . . . . . . . . . 18
|
173 | 168, 172 | nfim 1504 |
. . . . . . . . . . . . . . . . 17
|
174 | 165, 173 | nfralxy 2402 |
. . . . . . . . . . . . . . . 16
|
175 | 164, 174 | nfan 1497 |
. . . . . . . . . . . . . . 15
|
176 | | nfs1v 1856 |
. . . . . . . . . . . . . . . 16
|
177 | 166, 176 | nfan 1497 |
. . . . . . . . . . . . . . 15
|
178 | 175, 177 | nfan 1497 |
. . . . . . . . . . . . . 14
|
179 | | nfv 1461 |
. . . . . . . . . . . . . 14
|
180 | 178, 179 | nfan 1497 |
. . . . . . . . . . . . 13
|
181 | | nfv 1461 |
. . . . . . . . . . . . 13
|
182 | 180, 181 | nfan 1497 |
. . . . . . . . . . . 12
|
183 | 182, 57 | nfan 1497 |
. . . . . . . . . . 11
|
184 | 68, 72, 75, 80, 81, 82, 86, 93, 142, 163, 183 | bezoutlemstep 10386 |
. . . . . . . . . 10
|
185 | 184 | exp31 356 |
. . . . . . . . 9
|
186 | 67, 185 | ralrimi 2432 |
. . . . . . . 8
|
187 | | sbsbc 2819 |
. . . . . . . . . . . 12
|
188 | 187 | anbi1i 445 |
. . . . . . . . . . 11
|
189 | 188 | rexbii 2373 |
. . . . . . . . . 10
|
190 | 189 | imbi2i 224 |
. . . . . . . . 9
|
191 | 190 | ralbii 2372 |
. . . . . . . 8
|
192 | 186, 191 | sylibr 132 |
. . . . . . 7
|
193 | | nn0nlt0 8314 |
. . . . . . . . 9
|
194 | | nn0z 8371 |
. . . . . . . . . . . 12
|
195 | | ztri3or0 8393 |
. . . . . . . . . . . 12
|
196 | 194, 195 | syl 14 |
. . . . . . . . . . 11
|
197 | | 3orass 922 |
. . . . . . . . . . 11
|
198 | 196, 197 | sylib 120 |
. . . . . . . . . 10
|
199 | 198 | orcomd 680 |
. . . . . . . . 9
|
200 | 193, 199 | ecased 1280 |
. . . . . . . 8
|
201 | 200 | ad2antrr 471 |
. . . . . . 7
|
202 | 65, 192, 201 | mpjaodan 744 |
. . . . . 6
|
203 | 202 | exp31 356 |
. . . . 5
|
204 | 8, 16, 203 | nn0sinds 9430 |
. . . 4
|
205 | 204 | expd 254 |
. . 3
|
206 | 205 | impcom 123 |
. 2
|
207 | 206 | ralrimiva 2434 |
1
|