Step | Hyp | Ref
| Expression |
1 | | nnmulcl 8060 |
. . . . 5
|
2 | 1 | nnred 8052 |
. . . 4
|
3 | | nnz 8370 |
. . . . . . 7
|
4 | 3 | adantr 270 |
. . . . . 6
|
5 | 4 | zred 8469 |
. . . . 5
|
6 | | nnz 8370 |
. . . . . . 7
|
7 | 6 | adantl 271 |
. . . . . 6
|
8 | 7 | zred 8469 |
. . . . 5
|
9 | | 0red 7120 |
. . . . . . 7
|
10 | | nnre 8046 |
. . . . . . 7
|
11 | | nngt0 8064 |
. . . . . . 7
|
12 | 9, 10, 11 | ltled 7228 |
. . . . . 6
|
13 | 12 | adantr 270 |
. . . . 5
|
14 | | 0red 7120 |
. . . . . . 7
|
15 | | nnre 8046 |
. . . . . . 7
|
16 | | nngt0 8064 |
. . . . . . 7
|
17 | 14, 15, 16 | ltled 7228 |
. . . . . 6
|
18 | 17 | adantl 271 |
. . . . 5
|
19 | 5, 8, 13, 18 | mulge0d 7721 |
. . . 4
|
20 | 2, 19 | absidd 10053 |
. . 3
|
21 | 3, 6 | anim12i 331 |
. . . . . 6
|
22 | | nnne0 8067 |
. . . . . . . . 9
|
23 | 22 | neneqd 2266 |
. . . . . . . 8
|
24 | | nnne0 8067 |
. . . . . . . . 9
|
25 | 24 | neneqd 2266 |
. . . . . . . 8
|
26 | 23, 25 | anim12i 331 |
. . . . . . 7
|
27 | | ioran 701 |
. . . . . . 7
|
28 | 26, 27 | sylibr 132 |
. . . . . 6
|
29 | | lcmn0val 10448 |
. . . . . 6
lcm inf
|
30 | 21, 28, 29 | syl2anc 403 |
. . . . 5
lcm inf
|
31 | | lttri3 7191 |
. . . . . . 7
|
32 | 31 | adantl 271 |
. . . . . 6
|
33 | | gcddvds 10355 |
. . . . . . . . . . 11
|
34 | 33 | simpld 110 |
. . . . . . . . . 10
|
35 | | gcdcl 10358 |
. . . . . . . . . . . 12
|
36 | 35 | nn0zd 8467 |
. . . . . . . . . . 11
|
37 | | dvdsmultr1 10233 |
. . . . . . . . . . . 12
|
38 | 37 | 3expb 1139 |
. . . . . . . . . . 11
|
39 | 36, 38 | mpancom 413 |
. . . . . . . . . 10
|
40 | 34, 39 | mpd 13 |
. . . . . . . . 9
|
41 | 21, 40 | syl 14 |
. . . . . . . 8
|
42 | | gcdnncl 10359 |
. . . . . . . . 9
|
43 | | nndivdvds 10201 |
. . . . . . . . 9
|
44 | 1, 42, 43 | syl2anc 403 |
. . . . . . . 8
|
45 | 41, 44 | mpbid 145 |
. . . . . . 7
|
46 | 45 | nnred 8052 |
. . . . . 6
|
47 | 33 | simprd 112 |
. . . . . . . . . . . 12
|
48 | 21, 47 | syl 14 |
. . . . . . . . . . 11
|
49 | 21, 36 | syl 14 |
. . . . . . . . . . . 12
|
50 | 42 | nnne0d 8083 |
. . . . . . . . . . . 12
|
51 | | dvdsval2 10198 |
. . . . . . . . . . . 12
|
52 | 49, 50, 7, 51 | syl3anc 1169 |
. . . . . . . . . . 11
|
53 | 48, 52 | mpbid 145 |
. . . . . . . . . 10
|
54 | | dvdsmul1 10217 |
. . . . . . . . . 10
|
55 | 4, 53, 54 | syl2anc 403 |
. . . . . . . . 9
|
56 | | nncn 8047 |
. . . . . . . . . . 11
|
57 | 56 | adantr 270 |
. . . . . . . . . 10
|
58 | | nncn 8047 |
. . . . . . . . . . 11
|
59 | 58 | adantl 271 |
. . . . . . . . . 10
|
60 | 42 | nncnd 8053 |
. . . . . . . . . 10
|
61 | 42 | nnap0d 8084 |
. . . . . . . . . 10
# |
62 | 57, 59, 60, 61 | divassapd 7912 |
. . . . . . . . 9
|
63 | 55, 62 | breqtrrd 3811 |
. . . . . . . 8
|
64 | 21, 34 | syl 14 |
. . . . . . . . . . 11
|
65 | | dvdsval2 10198 |
. . . . . . . . . . . 12
|
66 | 49, 50, 4, 65 | syl3anc 1169 |
. . . . . . . . . . 11
|
67 | 64, 66 | mpbid 145 |
. . . . . . . . . 10
|
68 | | dvdsmul1 10217 |
. . . . . . . . . 10
|
69 | 7, 67, 68 | syl2anc 403 |
. . . . . . . . 9
|
70 | 57, 59 | mulcomd 7140 |
. . . . . . . . . . 11
|
71 | 70 | oveq1d 5547 |
. . . . . . . . . 10
|
72 | 59, 57, 60, 61 | divassapd 7912 |
. . . . . . . . . 10
|
73 | 71, 72 | eqtrd 2113 |
. . . . . . . . 9
|
74 | 69, 73 | breqtrrd 3811 |
. . . . . . . 8
|
75 | 63, 74 | jca 300 |
. . . . . . 7
|
76 | | breq2 3789 |
. . . . . . . . 9
|
77 | | breq2 3789 |
. . . . . . . . 9
|
78 | 76, 77 | anbi12d 456 |
. . . . . . . 8
|
79 | 78 | elrab 2749 |
. . . . . . 7
|
80 | 45, 75, 79 | sylanbrc 408 |
. . . . . 6
|
81 | 46 | adantr 270 |
. . . . . . 7
|
82 | | elrabi 2746 |
. . . . . . . . 9
|
83 | 82 | nnred 8052 |
. . . . . . . 8
|
84 | 83 | adantl 271 |
. . . . . . 7
|
85 | | breq2 3789 |
. . . . . . . . . 10
|
86 | | breq2 3789 |
. . . . . . . . . 10
|
87 | 85, 86 | anbi12d 456 |
. . . . . . . . 9
|
88 | 87 | elrab 2749 |
. . . . . . . 8
|
89 | | bezout 10400 |
. . . . . . . . . . . . 13
|
90 | 21, 89 | syl 14 |
. . . . . . . . . . . 12
|
91 | 90 | adantr 270 |
. . . . . . . . . . 11
|
92 | | nncn 8047 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
93 | 92 | ad2antlr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
94 | 1 | nncnd 8053 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
95 | 94 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
96 | 60 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
97 | 57 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
98 | 58 | ad3antlr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | | simplll 499 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
100 | 99 | nnap0d 8084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
# |
101 | | simpllr 500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
102 | 101 | nnap0d 8084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
# |
103 | 97, 98, 100, 102 | mulap0d 7748 |
. . . . . . . . . . . . . . . . . . . . . . 23
# |
104 | 61 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
# |
105 | 93, 95, 96, 103, 104 | divdivap2d 7909 |
. . . . . . . . . . . . . . . . . . . . . 22
|
106 | 105 | adantr 270 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | | oveq2 5540 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
108 | 107 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . . . . 22
|
109 | | zcn 8356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
110 | 109 | ad2antrl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
111 | 97, 110 | mulcld 7139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
112 | | zcn 8356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
113 | 112 | ad2antll 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
114 | 98, 113 | mulcld 7139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
115 | 93, 111, 114 | adddid 7143 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
116 | 115 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
117 | 93, 111 | mulcld 7139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
118 | 93, 114 | mulcld 7139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
119 | 117, 118,
95, 103 | divdirapd 7915 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
120 | 116, 119 | eqtrd 2113 |
. . . . . . . . . . . . . . . . . . . . . 22
|
121 | 108, 120 | sylan9eqr 2135 |
. . . . . . . . . . . . . . . . . . . . 21
|
122 | 93, 97, 110 | mul12d 7260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
123 | 122 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
124 | 93, 110 | mulcld 7139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
125 | 124, 98, 97, 102, 100 | divcanap5d 7903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
126 | 123, 125 | eqtrd 2113 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
127 | 93, 98, 113 | mul12d 7260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
128 | 127 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
129 | 70 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
130 | 129 | oveq2d 5548 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
131 | 93, 113 | mulcld 7139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
132 | 131, 97, 98, 100, 102 | divcanap5d 7903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
133 | 128, 130,
132 | 3eqtrd 2117 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
134 | 126, 133 | oveq12d 5550 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 134 | adantr 270 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 106, 121,
135 | 3eqtrd 2117 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | 136 | ex 113 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 137 | adantlrr 466 |
. . . . . . . . . . . . . . . . . 18
|
139 | 138 | imp 122 |
. . . . . . . . . . . . . . . . 17
|
140 | 6 | ad3antlr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
141 | | nnz 8370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
142 | 141 | ad2antlr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
143 | | simprl 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
144 | | dvdsmultr1 10233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
145 | 140, 142,
143, 144 | syl3anc 1169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
146 | 24 | ad3antlr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
147 | 142, 143 | zmulcld 8475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
148 | | dvdsval2 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
149 | 140, 146,
147, 148 | syl3anc 1169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
150 | 145, 149 | sylibd 147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
151 | 150 | adantld 272 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
152 | 151 | 3impia 1135 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
153 | 3 | ad3antrrr 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
154 | | simprr 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
155 | | dvdsmultr1 10233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
156 | 153, 142,
154, 155 | syl3anc 1169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
157 | 22 | ad3antrrr 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
158 | 142, 154 | zmulcld 8475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
159 | | dvdsval2 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
160 | 153, 157,
158, 159 | syl3anc 1169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
161 | 156, 160 | sylibd 147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
162 | 161 | adantrd 273 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
163 | 162 | 3impia 1135 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
164 | 152, 163 | zaddcld 8473 |
. . . . . . . . . . . . . . . . . . . . . 22
|
165 | 164 | 3expia 1140 |
. . . . . . . . . . . . . . . . . . . . 21
|
166 | 165 | an32s 532 |
. . . . . . . . . . . . . . . . . . . 20
|
167 | 166 | impr 371 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 167 | an32s 532 |
. . . . . . . . . . . . . . . . . 18
|
169 | 168 | adantr 270 |
. . . . . . . . . . . . . . . . 17
|
170 | 139, 169 | eqeltrd 2155 |
. . . . . . . . . . . . . . . 16
|
171 | 45 | nnzd 8468 |
. . . . . . . . . . . . . . . . . . 19
|
172 | 171 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . 18
|
173 | 45 | nnne0d 8083 |
. . . . . . . . . . . . . . . . . . 19
|
174 | 173 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . 18
|
175 | 142 | adantlrr 466 |
. . . . . . . . . . . . . . . . . 18
|
176 | | dvdsval2 10198 |
. . . . . . . . . . . . . . . . . 18
|
177 | 172, 174,
175, 176 | syl3anc 1169 |
. . . . . . . . . . . . . . . . 17
|
178 | 177 | adantr 270 |
. . . . . . . . . . . . . . . 16
|
179 | 170, 178 | mpbird 165 |
. . . . . . . . . . . . . . 15
|
180 | 179 | ex 113 |
. . . . . . . . . . . . . 14
|
181 | 180 | anassrs 392 |
. . . . . . . . . . . . 13
|
182 | 181 | reximdva 2463 |
. . . . . . . . . . . 12
|
183 | 182 | reximdva 2463 |
. . . . . . . . . . 11
|
184 | 91, 183 | mpd 13 |
. . . . . . . . . 10
|
185 | | 1z 8377 |
. . . . . . . . . . . 12
|
186 | | elex2 2615 |
. . . . . . . . . . . 12
|
187 | | r19.9rmv 3333 |
. . . . . . . . . . . 12
|
188 | 185, 186,
187 | mp2b 8 |
. . . . . . . . . . 11
|
189 | | r19.9rmv 3333 |
. . . . . . . . . . . 12
|
190 | 185, 186,
189 | mp2b 8 |
. . . . . . . . . . 11
|
191 | 188, 190 | bitri 182 |
. . . . . . . . . 10
|
192 | 184, 191 | sylibr 132 |
. . . . . . . . 9
|
193 | 171 | adantr 270 |
. . . . . . . . . 10
|
194 | | simprl 497 |
. . . . . . . . . 10
|
195 | | dvdsle 10244 |
. . . . . . . . . 10
|
196 | 193, 194,
195 | syl2anc 403 |
. . . . . . . . 9
|
197 | 192, 196 | mpd 13 |
. . . . . . . 8
|
198 | 88, 197 | sylan2b 281 |
. . . . . . 7
|
199 | 81, 84, 198 | lensymd 7231 |
. . . . . 6
|
200 | 32, 46, 80, 199 | infminti 6440 |
. . . . 5
inf
|
201 | 30, 200 | eqtr2d 2114 |
. . . 4
lcm |
202 | 201, 45 | eqeltrrd 2156 |
. . . . . 6
lcm |
203 | 202 | nncnd 8053 |
. . . . 5
lcm |
204 | 94, 203, 60, 61 | divmulap3d 7911 |
. . . 4
lcm
lcm |
205 | 201, 204 | mpbid 145 |
. . 3
lcm |
206 | 20, 205 | eqtr2d 2114 |
. 2
lcm
|
207 | | simprl 497 |
. . . 4
|
208 | | eleq1 2141 |
. . . . . . . 8
|
209 | | breq2 3789 |
. . . . . . . . 9
|
210 | | breq2 3789 |
. . . . . . . . 9
|
211 | 209, 210 | anbi12d 456 |
. . . . . . . 8
|
212 | 208, 211 | anbi12d 456 |
. . . . . . 7
|
213 | 212 | anbi2d 451 |
. . . . . 6
|
214 | | breq2 3789 |
. . . . . 6
lcm
lcm |
215 | 213, 214 | imbi12d 232 |
. . . . 5
lcm
lcm
|
216 | 201 | breq1d 3795 |
. . . . . . 7
lcm |
217 | 216 | adantr 270 |
. . . . . 6
lcm |
218 | 192, 217 | mpbid 145 |
. . . . 5
lcm
|
219 | 215, 218 | vtoclg 2658 |
. . . 4
lcm
|
220 | 207, 219 | mpcom 36 |
. . 3
lcm
|
221 | 220 | ex 113 |
. 2
lcm |
222 | 206, 221 | jca 300 |
1
lcm
lcm |