author | haftmann |
Mon, 26 Mar 2007 14:53:02 +0200 | |
changeset 22519 | eb70ed79dac7 |
parent 22367 | 6860f09242bf |
child 23244 | 1630951f0512 |
permissions | -rw-r--r-- |
21256 | 1 |
(* Title: HOL/GCD.thy |
2 |
ID: $Id$ |
|
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
*) |
|
6 |
||
7 |
header {* The Greatest Common Divisor *} |
|
8 |
||
9 |
theory GCD |
|
10 |
imports Main |
|
11 |
begin |
|
12 |
||
13 |
text {* |
|
14 |
See \cite{davenport92}. |
|
15 |
\bigskip |
|
16 |
*} |
|
17 |
||
18 |
consts |
|
19 |
gcd :: "nat \<times> nat => nat" -- {* Euclid's algorithm *} |
|
20 |
||
21 |
recdef gcd "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)" |
|
22 |
"gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" |
|
23 |
||
21263 | 24 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21263
diff
changeset
|
25 |
is_gcd :: "nat => nat => nat => bool" where -- {* @{term gcd} as a relation *} |
21263 | 26 |
"is_gcd p m n = (p dvd m \<and> p dvd n \<and> |
27 |
(\<forall>d. d dvd m \<and> d dvd n --> d dvd p))" |
|
21256 | 28 |
|
29 |
||
30 |
lemma gcd_induct: |
|
31 |
"(!!m. P m 0) ==> |
|
32 |
(!!m n. 0 < n ==> P n (m mod n) ==> P m n) |
|
33 |
==> P (m::nat) (n::nat)" |
|
34 |
apply (induct m n rule: gcd.induct) |
|
35 |
apply (case_tac "n = 0") |
|
36 |
apply simp_all |
|
37 |
done |
|
38 |
||
39 |
||
40 |
lemma gcd_0 [simp]: "gcd (m, 0) = m" |
|
21263 | 41 |
by simp |
21256 | 42 |
|
43 |
lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" |
|
21263 | 44 |
by simp |
21256 | 45 |
|
46 |
declare gcd.simps [simp del] |
|
47 |
||
48 |
lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" |
|
21263 | 49 |
by (simp add: gcd_non_0) |
21256 | 50 |
|
51 |
text {* |
|
52 |
\medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The |
|
53 |
conjunctions don't seem provable separately. |
|
54 |
*} |
|
55 |
||
56 |
lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" |
|
57 |
and gcd_dvd2 [iff]: "gcd (m, n) dvd n" |
|
58 |
apply (induct m n rule: gcd_induct) |
|
21263 | 59 |
apply (simp_all add: gcd_non_0) |
21256 | 60 |
apply (blast dest: dvd_mod_imp_dvd) |
61 |
done |
|
62 |
||
63 |
text {* |
|
64 |
\medskip Maximality: for all @{term m}, @{term n}, @{term k} |
|
65 |
naturals, if @{term k} divides @{term m} and @{term k} divides |
|
66 |
@{term n} then @{term k} divides @{term "gcd (m, n)"}. |
|
67 |
*} |
|
68 |
||
69 |
lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" |
|
21263 | 70 |
by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod) |
21256 | 71 |
|
72 |
lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)" |
|
21263 | 73 |
by (blast intro!: gcd_greatest intro: dvd_trans) |
21256 | 74 |
|
75 |
lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)" |
|
21263 | 76 |
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff) |
21256 | 77 |
|
78 |
||
79 |
text {* |
|
80 |
\medskip Function gcd yields the Greatest Common Divisor. |
|
81 |
*} |
|
82 |
||
83 |
lemma is_gcd: "is_gcd (gcd (m, n)) m n" |
|
84 |
apply (simp add: is_gcd_def gcd_greatest) |
|
85 |
done |
|
86 |
||
87 |
text {* |
|
88 |
\medskip Uniqueness of GCDs. |
|
89 |
*} |
|
90 |
||
91 |
lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" |
|
92 |
apply (simp add: is_gcd_def) |
|
93 |
apply (blast intro: dvd_anti_sym) |
|
94 |
done |
|
95 |
||
96 |
lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" |
|
97 |
apply (auto simp add: is_gcd_def) |
|
98 |
done |
|
99 |
||
100 |
||
101 |
text {* |
|
102 |
\medskip Commutativity |
|
103 |
*} |
|
104 |
||
105 |
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" |
|
106 |
apply (auto simp add: is_gcd_def) |
|
107 |
done |
|
108 |
||
109 |
lemma gcd_commute: "gcd (m, n) = gcd (n, m)" |
|
110 |
apply (rule is_gcd_unique) |
|
111 |
apply (rule is_gcd) |
|
112 |
apply (subst is_gcd_commute) |
|
113 |
apply (simp add: is_gcd) |
|
114 |
done |
|
115 |
||
116 |
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" |
|
117 |
apply (rule is_gcd_unique) |
|
118 |
apply (rule is_gcd) |
|
119 |
apply (simp add: is_gcd_def) |
|
120 |
apply (blast intro: dvd_trans) |
|
121 |
done |
|
122 |
||
123 |
lemma gcd_0_left [simp]: "gcd (0, m) = m" |
|
124 |
apply (simp add: gcd_commute [of 0]) |
|
125 |
done |
|
126 |
||
127 |
lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1" |
|
128 |
apply (simp add: gcd_commute [of "Suc 0"]) |
|
129 |
done |
|
130 |
||
131 |
||
132 |
text {* |
|
133 |
\medskip Multiplication laws |
|
134 |
*} |
|
135 |
||
136 |
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" |
|
137 |
-- {* \cite[page 27]{davenport92} *} |
|
138 |
apply (induct m n rule: gcd_induct) |
|
139 |
apply simp |
|
140 |
apply (case_tac "k = 0") |
|
141 |
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
|
142 |
done |
|
143 |
||
144 |
lemma gcd_mult [simp]: "gcd (k, k * n) = k" |
|
145 |
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) |
|
146 |
done |
|
147 |
||
148 |
lemma gcd_self [simp]: "gcd (k, k) = k" |
|
149 |
apply (rule gcd_mult [of k 1, simplified]) |
|
150 |
done |
|
151 |
||
152 |
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" |
|
153 |
apply (insert gcd_mult_distrib2 [of m k n]) |
|
154 |
apply simp |
|
155 |
apply (erule_tac t = m in ssubst) |
|
156 |
apply simp |
|
157 |
done |
|
158 |
||
159 |
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" |
|
160 |
apply (blast intro: relprime_dvd_mult dvd_trans) |
|
161 |
done |
|
162 |
||
163 |
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" |
|
164 |
apply (rule dvd_anti_sym) |
|
165 |
apply (rule gcd_greatest) |
|
166 |
apply (rule_tac n = k in relprime_dvd_mult) |
|
167 |
apply (simp add: gcd_assoc) |
|
168 |
apply (simp add: gcd_commute) |
|
169 |
apply (simp_all add: mult_commute) |
|
170 |
apply (blast intro: dvd_trans) |
|
171 |
done |
|
172 |
||
173 |
||
174 |
text {* \medskip Addition laws *} |
|
175 |
||
176 |
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" |
|
177 |
apply (case_tac "n = 0") |
|
178 |
apply (simp_all add: gcd_non_0) |
|
179 |
done |
|
180 |
||
181 |
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" |
|
182 |
proof - |
|
22367 | 183 |
have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) |
21256 | 184 |
also have "... = gcd (n + m, m)" by (simp add: add_commute) |
185 |
also have "... = gcd (n, m)" by simp |
|
22367 | 186 |
also have "... = gcd (m, n)" by (rule gcd_commute) |
21256 | 187 |
finally show ?thesis . |
188 |
qed |
|
189 |
||
190 |
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" |
|
191 |
apply (subst add_commute) |
|
192 |
apply (rule gcd_add2) |
|
193 |
done |
|
194 |
||
195 |
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" |
|
21263 | 196 |
by (induct k) (simp_all add: add_assoc) |
21256 | 197 |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
198 |
|
22367 | 199 |
text {* |
200 |
\medskip Division by gcd yields rrelatively primes. |
|
201 |
*} |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
202 |
|
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
203 |
lemma div_gcd_relprime: |
22367 | 204 |
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
205 |
shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1" |
22367 | 206 |
proof - |
207 |
let ?g = "gcd (a, b)" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
208 |
let ?a' = "a div ?g" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
209 |
let ?b' = "b div ?g" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
210 |
let ?g' = "gcd (?a', ?b')" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
211 |
have dvdg: "?g dvd a" "?g dvd b" by simp_all |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
212 |
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all |
22367 | 213 |
from dvdg dvdg' obtain ka kb ka' kb' where |
214 |
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
215 |
unfolding dvd_def by blast |
22367 | 216 |
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all |
217 |
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" |
|
218 |
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] |
|
219 |
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
220 |
have "?g \<noteq> 0" using nz by (simp add: gcd_zero) |
22367 | 221 |
then have gp: "?g > 0" by simp |
222 |
from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . |
|
223 |
with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
224 |
qed |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
225 |
|
22367 | 226 |
|
227 |
text {* |
|
228 |
\medskip Gcd on integers. |
|
229 |
*} |
|
230 |
||
231 |
definition |
|
232 |
igcd :: "int \<Rightarrow> int \<Rightarrow> int" where |
|
233 |
"igcd i j = int (gcd (nat (abs i), nat (abs j)))" |
|
234 |
||
235 |
lemma igcd_dvd1 [simp]: "igcd i j dvd i" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
236 |
by (simp add: igcd_def int_dvd_iff) |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
237 |
|
22367 | 238 |
lemma igcd_dvd2 [simp]: "igcd i j dvd j" |
239 |
by (simp add: igcd_def int_dvd_iff) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
240 |
|
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
241 |
lemma igcd_pos: "igcd i j \<ge> 0" |
22367 | 242 |
by (simp add: igcd_def) |
243 |
||
244 |
lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)" |
|
245 |
by (simp add: igcd_def gcd_zero) arith |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
246 |
|
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
247 |
lemma igcd_commute: "igcd i j = igcd j i" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
248 |
unfolding igcd_def by (simp add: gcd_commute) |
22367 | 249 |
|
250 |
lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
251 |
unfolding igcd_def by simp |
22367 | 252 |
|
253 |
lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
254 |
unfolding igcd_def by simp |
22367 | 255 |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
256 |
lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
257 |
unfolding igcd_def |
22367 | 258 |
proof - |
259 |
assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j" |
|
260 |
then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp |
|
261 |
from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
262 |
have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>" |
22367 | 263 |
unfolding dvd_def |
264 |
by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric]) |
|
265 |
from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
266 |
unfolding dvd_def by blast |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
267 |
from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp |
22367 | 268 |
then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
269 |
then show ?thesis |
22367 | 270 |
apply (subst zdvd_abs1 [symmetric]) |
271 |
apply (subst zdvd_abs2 [symmetric]) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
272 |
apply (unfold dvd_def) |
22367 | 273 |
apply (rule_tac x = "int h'" in exI, simp) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
274 |
done |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
275 |
qed |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
276 |
|
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
277 |
lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith |
22367 | 278 |
|
279 |
lemma igcd_greatest: |
|
280 |
assumes "k dvd m" and "k dvd n" |
|
281 |
shows "k dvd igcd m n" |
|
282 |
proof - |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
283 |
let ?k' = "nat \<bar>k\<bar>" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
284 |
let ?m' = "nat \<bar>m\<bar>" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
285 |
let ?n' = "nat \<bar>n\<bar>" |
22367 | 286 |
from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
287 |
unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2) |
22367 | 288 |
from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
289 |
unfolding igcd_def by (simp only: zdvd_int) |
22367 | 290 |
then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs) |
291 |
then show "k dvd igcd m n" by (simp add: zdvd_abs1) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
292 |
qed |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
293 |
|
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
294 |
lemma div_igcd_relprime: |
22367 | 295 |
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
296 |
shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1" |
22367 | 297 |
proof - |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
298 |
from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by simp |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
299 |
let ?g = "igcd a b" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
300 |
let ?a' = "a div ?g" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
301 |
let ?b' = "b div ?g" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
302 |
let ?g' = "igcd ?a' ?b'" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
303 |
have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2) |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
304 |
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2) |
22367 | 305 |
from dvdg dvdg' obtain ka kb ka' kb' where |
306 |
kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
307 |
unfolding dvd_def by blast |
22367 | 308 |
then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all |
309 |
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" |
|
310 |
by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)] |
|
311 |
zdvd_mult_div_cancel [OF dvdg(2)] dvd_def) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
312 |
have "?g \<noteq> 0" using nz by simp |
22367 | 313 |
then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith |
314 |
from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . |
|
315 |
with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
316 |
with igcd_pos show "?g' = 1" by simp |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
317 |
qed |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
318 |
|
21256 | 319 |
end |