Step | Hyp | Ref
| Expression |
1 | | gcdcl 11865 |
. . . . . 6
|
2 | 1 | nn0ge0d 9151 |
. . . . 5
|
3 | | gcddvds 11862 |
. . . . 5
|
4 | | 3anass 967 |
. . . . . . . 8
|
5 | | ancom 264 |
. . . . . . . 8
|
6 | 4, 5 | bitri 183 |
. . . . . . 7
|
7 | | dvdsgcd 11911 |
. . . . . . 7
|
8 | 6, 7 | sylbir 134 |
. . . . . 6
|
9 | 8 | ralrimiva 2530 |
. . . . 5
|
10 | 2, 3, 9 | 3jca 1162 |
. . . 4
|
11 | 10 | adantr 274 |
. . 3
|
12 | | breq2 3971 |
. . . . 5
|
13 | | breq1 3970 |
. . . . . 6
|
14 | | breq1 3970 |
. . . . . 6
|
15 | 13, 14 | anbi12d 465 |
. . . . 5
|
16 | | breq2 3971 |
. . . . . . 7
|
17 | 16 | imbi2d 229 |
. . . . . 6
|
18 | 17 | ralbidv 2457 |
. . . . 5
|
19 | 12, 15, 18 | 3anbi123d 1294 |
. . . 4
|
20 | 19 | adantl 275 |
. . 3
|
21 | 11, 20 | mpbird 166 |
. 2
|
22 | | gcdval 11858 |
. . . 4
|
23 | 22 | adantr 274 |
. . 3
|
24 | | iftrue 3511 |
. . . . . . 7
|
25 | 24 | adantr 274 |
. . . . . 6
|
26 | | breq2 3971 |
. . . . . . . . . . 11
|
27 | | breq2 3971 |
. . . . . . . . . . 11
|
28 | 26, 27 | bi2anan9 596 |
. . . . . . . . . 10
|
29 | | breq2 3971 |
. . . . . . . . . . . . 13
|
30 | | breq2 3971 |
. . . . . . . . . . . . 13
|
31 | 29, 30 | bi2anan9 596 |
. . . . . . . . . . . 12
|
32 | 31 | imbi1d 230 |
. . . . . . . . . . 11
|
33 | 32 | ralbidv 2457 |
. . . . . . . . . 10
|
34 | 28, 33 | 3anbi23d 1297 |
. . . . . . . . 9
|
35 | | dvdszrcl 11699 |
. . . . . . . . . . . . 13
|
36 | | dvds0 11713 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36, 36 | jca 304 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 37 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
|
39 | | pm5.5 241 |
. . . . . . . . . . . . . . . . . 18
|
40 | 38, 39 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | ralbidva 2453 |
. . . . . . . . . . . . . . . 16
|
42 | | 0z 9183 |
. . . . . . . . . . . . . . . . . . 19
|
43 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | 43 | rspcv 2812 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 42, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
46 | | 0dvds 11718 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 46 | biimpd 143 |
. . . . . . . . . . . . . . . . . . 19
|
48 | | eqcom 2159 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 47, 48 | syl6ibr 161 |
. . . . . . . . . . . . . . . . . 18
|
50 | 45, 49 | syl5 32 |
. . . . . . . . . . . . . . . . 17
|
51 | 50 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
52 | 41, 51 | sylbid 149 |
. . . . . . . . . . . . . . 15
|
53 | 52 | ex 114 |
. . . . . . . . . . . . . 14
|
54 | 53 | adantr 274 |
. . . . . . . . . . . . 13
|
55 | 35, 54 | syl 14 |
. . . . . . . . . . . 12
|
56 | 55 | adantr 274 |
. . . . . . . . . . 11
|
57 | 56 | com12 30 |
. . . . . . . . . 10
|
58 | 57 | 3imp 1176 |
. . . . . . . . 9
|
59 | 34, 58 | syl6bi 162 |
. . . . . . . 8
|
60 | 59 | adantld 276 |
. . . . . . 7
|
61 | 60 | imp 123 |
. . . . . 6
|
62 | 25, 61 | eqtrd 2190 |
. . . . 5
|
63 | 62 | ancoms 266 |
. . . 4
|
64 | | iffalse 3514 |
. . . . . . 7
|
65 | 64 | adantr 274 |
. . . . . 6
|
66 | | lttri3 7959 |
. . . . . . . 8
|
67 | 66 | adantl 275 |
. . . . . . 7
|
68 | | dvdszrcl 11699 |
. . . . . . . . . . . 12
|
69 | 68 | simpld 111 |
. . . . . . . . . . 11
|
70 | 69 | zred 9291 |
. . . . . . . . . 10
|
71 | 70 | adantr 274 |
. . . . . . . . 9
|
72 | 71 | 3ad2ant2 1004 |
. . . . . . . 8
|
73 | 72 | ad2antll 483 |
. . . . . . 7
|
74 | | breq1 3970 |
. . . . . . . . . . 11
|
75 | | breq1 3970 |
. . . . . . . . . . 11
|
76 | 74, 75 | anbi12d 465 |
. . . . . . . . . 10
|
77 | 76 | elrab 2868 |
. . . . . . . . 9
|
78 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 78, 79 | anbi12d 465 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 80, 81 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 82 | rspcv 2812 |
. . . . . . . . . . . . . . . . . 18
|
84 | 83 | com23 78 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | imp 123 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
|
87 | | elnn0z 9185 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | simplbi2 383 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 88 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 68, 89 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 90 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
|
92 | 91 | impcom 124 |
. . . . . . . . . . . . . . . . 17
|
93 | | zre 9176 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | 93 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 94 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 71 | ad3antlr 485 |
. . . . . . . . . . . . . . . . . . 19
|
97 | | simp-5l 533 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
98 | | elnn0 9097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
99 | | 2a1 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
100 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
101 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
102 | 100, 101 | anbi12d 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
103 | 102 | anbi2d 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
104 | 103 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
105 | | simplr 520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
106 | | zdceq 9244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
DECID |
107 | 42, 106 | mpan2 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
DECID
|
108 | | ianordc 885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
DECID
|
109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
110 | 109 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
111 | 105, 110 | mpbid 146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
112 | | dvdszrcl 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
113 | | 0dvds 11718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
114 | | pm2.24 611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
115 | 113, 114 | syl6bi 162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
116 | 115 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
117 | 112, 116 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
118 | 117 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
119 | 118 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
120 | | dvdszrcl 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
121 | | 0dvds 11718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
122 | | pm2.24 611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
123 | 121, 122 | syl6bi 162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
124 | 123 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
125 | 120, 124 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
126 | 125 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
127 | 126 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
128 | 119, 127 | jaoi 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
129 | 111, 128 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
130 | 129 | adantld 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
131 | 130 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
132 | 104, 131 | sylbid 149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
133 | 132 | ex 114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
134 | 99, 133 | jaoi 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
135 | 98, 134 | sylbi 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
136 | 135 | impcom 124 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
137 | 136 | imp 123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
138 | | dvdsle 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
139 | 97, 137, 138 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
140 | 139 | exp31 362 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
141 | 140 | com14 88 |
. . . . . . . . . . . . . . . . . . . . . 22
|
142 | 141 | imp 123 |
. . . . . . . . . . . . . . . . . . . . 21
|
143 | 142 | impcom 124 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | 143 | imp 123 |
. . . . . . . . . . . . . . . . . . 19
|
145 | 95, 96, 144 | lensymd 8001 |
. . . . . . . . . . . . . . . . . 18
|
146 | 145 | exp31 362 |
. . . . . . . . . . . . . . . . 17
|
147 | 92, 146 | mpan2d 425 |
. . . . . . . . . . . . . . . 16
|
148 | 147 | com13 80 |
. . . . . . . . . . . . . . 15
|
149 | 86, 148 | syld 45 |
. . . . . . . . . . . . . 14
|
150 | 149 | com13 80 |
. . . . . . . . . . . . 13
|
151 | 150 | 3impia 1182 |
. . . . . . . . . . . 12
|
152 | 151 | com12 30 |
. . . . . . . . . . 11
|
153 | 152 | expimpd 361 |
. . . . . . . . . 10
|
154 | 153 | expimpd 361 |
. . . . . . . . 9
|
155 | 77, 154 | sylbi 120 |
. . . . . . . 8
|
156 | 155 | impcom 124 |
. . . . . . 7
|
157 | 69 | adantr 274 |
. . . . . . . . . . . . 13
|
158 | 157 | ancri 322 |
. . . . . . . . . . . 12
|
159 | 158 | 3ad2ant2 1004 |
. . . . . . . . . . 11
|
160 | 159 | ad2antll 483 |
. . . . . . . . . 10
|
161 | 160 | adantr 274 |
. . . . . . . . 9
|
162 | | breq1 3970 |
. . . . . . . . . . 11
|
163 | | breq1 3970 |
. . . . . . . . . . 11
|
164 | 162, 163 | anbi12d 465 |
. . . . . . . . . 10
|
165 | 164 | elrab 2868 |
. . . . . . . . 9
|
166 | 161, 165 | sylibr 133 |
. . . . . . . 8
|
167 | | breq2 3971 |
. . . . . . . . 9
|
168 | 167 | adantl 275 |
. . . . . . . 8
|
169 | | simprr 522 |
. . . . . . . 8
|
170 | 166, 168,
169 | rspcedvd 2822 |
. . . . . . 7
|
171 | 67, 73, 156, 170 | eqsuptid 6943 |
. . . . . 6
|
172 | 65, 171 | eqtrd 2190 |
. . . . 5
|
173 | 172 | ancoms 266 |
. . . 4
|
174 | | gcdmndc 11843 |
. . . . . 6
DECID |
175 | 174 | adantr 274 |
. . . . 5
DECID |
176 | | exmiddc 822 |
. . . . 5
DECID
|
177 | 175, 176 | syl 14 |
. . . 4
|
178 | 63, 173, 177 | mpjaodan 788 |
. . 3
|
179 | 23, 178 | eqtr2d 2191 |
. 2
|
180 | 21, 179 | impbida 586 |
1
|