1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/gcd_properties1".
17 include "nat/propr_div_mod_lt_le_totient1_aux.ma".
19 (* this file contains some important properites of gcd in N *)
21 (*it's a generalization of the existing theorem divides_gcd_aux (in which
22 c = 1), proved in file gcd.ma
24 theorem divides_times_gcd_aux: \forall p,m,n,d,c.
25 O \lt c \to O < n \to n \le m \to n \le p \to
26 d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
35 cut (n1 \divides m \lor n1 \ndivides m)
37 [ rewrite > divides_to_divides_b_true
43 | rewrite > not_divides_to_divides_b_false
47 | cut (O \lt m \mod n1 \lor O = m \mod n1)
50 | absurd (n1 \divides m)
51 [ apply mod_O_to_divides
59 | apply le_to_or_lt_eq.
67 [ change with (m \mod n1 < n1).
74 [ rewrite < (sym_times c m).
75 rewrite < (sym_times c n1).
77 [ rewrite > (S_pred c)
78 [ rewrite > (S_pred n1)
79 [ apply (lt_O_times_S_S)
95 | apply (decidable_divides n1 m).
101 (*it's a generalization of the existing theorem divides_gcd_d (in which
102 c = 1), proved in file gcd.ma
104 theorem divides_d_times_gcd: \forall m,n,d,c.
105 O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
113 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
117 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
119 [ apply (nat_case1 n)
124 change with (d \divides c*gcd_aux (S m1) m (S m1)).
125 apply divides_times_gcd_aux
131 | apply (le_n (S m1))
137 | apply (nat_case1 m)
142 change with (d \divides c * gcd_aux (S m1) n (S m1)).
143 apply divides_times_gcd_aux
145 change with (O \lt c).
151 | apply (le_n (S m1)).
160 (* a basic property of divides predicate *)
162 theorem O_div_c_to_c_eq_O: \forall c:nat.
163 O \divides c \to c = O.
165 apply antisymmetric_divides
171 (* an alternative characterization for gcd *)
172 theorem gcd1: \forall a,b,c:nat.
173 c \divides a \to c \divides b \to
174 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
176 elim (H2 ((gcd a b)))
177 [ apply (antisymmetric_divides (gcd a b) c)
178 [ apply (witness (gcd a b) c n2).
180 | apply divides_d_gcd;
183 | apply divides_gcd_n
190 theorem eq_gcd_times_times_eqv_times_gcd: \forall a,b,c:nat.
191 (gcd (c*a) (c*b)) = c*(gcd a b).
200 [ apply divides_times
202 | apply divides_gcd_n.
204 | apply divides_times
210 apply (divides_d_times_gcd)
220 theorem associative_nat_gcd: associative nat gcd.
221 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
224 [ apply divides_d_gcd
225 [ apply (trans_divides ? (gcd b c) ?)
226 [ apply divides_gcd_m
227 | apply divides_gcd_n
229 | apply divides_gcd_n
231 | apply (trans_divides ? (gcd b c) ?)
232 [ apply divides_gcd_m
233 | apply divides_gcd_m
236 cut (d \divides a \land d \divides b)
238 cut (d \divides (gcd b c))
239 [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
240 | apply (divides_d_gcd c b d H1 H3)
243 [ apply (trans_divides d (gcd a b) a H).
245 | apply (trans_divides d (gcd a b) b H).
252 theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat.
253 a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
259 cut (d = O) (*this is an impossible case*)
263 | rewrite > H2 in H1.
270 [ rewrite > (S_pred d Hcut).
275 apply (divides_n_n O)
276 | apply (lt_times_eq_O b c)
279 | apply (O_div_c_to_c_eq_O (b*c) H)
291 cut (d \divides a \land d \divides b)
295 rewrite < (NdivM_times_M_to_N a d) in H3
296 [ rewrite < (NdivM_times_M_to_N b d) in H3
297 [ cut (b/d*c = a/d*n2)
298 [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
299 [ apply (O_lt_times_to_O_lt (a/d) d).
300 rewrite > (NdivM_times_M_to_N a d);
302 | apply (inj_times_r1 d ? ?)
304 | rewrite < (eq_gcd_times_times_eqv_times_gcd (a/d) (b/d) d).
305 rewrite < (times_n_SO d).
306 rewrite < (sym_times (a/d) d).
307 rewrite < (sym_times (b/d) d).
308 rewrite > (NdivM_times_M_to_N a d)
309 [ rewrite > (NdivM_times_M_to_N b d);
315 | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
317 | apply (inj_times_r1 d ? ?)
319 | rewrite > sym_times.
320 rewrite > (sym_times d ((a/d) * n2)).
321 rewrite > assoc_times.
322 rewrite > (assoc_times (a/d) n2 d).
323 rewrite > (sym_times c d).
324 rewrite > (sym_times n2 d).
325 rewrite < assoc_times.
326 rewrite < (assoc_times (a/d) d n2).
346 [ apply divides_gcd_n
347 | apply divides_gcd_m
353 theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat.
354 (gcd (a+m*b) b) = d \to (gcd a b) = d.
357 [ rewrite > (minus_plus_m_m a (m*b)).
361 | rewrite > (times_n_SO d).
362 rewrite > (sym_times d ?).
377 | rewrite > (times_n_SO d1).
378 rewrite > (sym_times d1 ?).
388 theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat.
389 (gcd (a+m*b) b) = (gcd a b).
392 apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m).
396 theorem gcd_div_div_eq_div_gcd: \forall a,b,m:nat.
397 O \lt m \to m \divides a \to m \divides b \to
398 (gcd (a/m) (b/m)) = (gcd a b) / m.
400 apply (inj_times_r1 m H).
401 rewrite > (sym_times m ((gcd a b)/m)).
402 rewrite > (NdivM_times_M_to_N (gcd a b) m)
403 [ rewrite < eq_gcd_times_times_eqv_times_gcd.
404 rewrite > (sym_times m (a/m)).
405 rewrite > (sym_times m (b/m)).
406 rewrite > (NdivM_times_M_to_N a m H H1).
407 rewrite > (NdivM_times_M_to_N b m H H2).
410 | apply divides_d_gcd;
416 theorem gcdSO_divides_divides_times_divides: \forall c,e,f:nat.
417 (gcd e f) = (S O) \to e \divides c \to f \divides c \to
425 apply (divides_n_n O).
430 [ apply (le_to_not_lt O O)
434 | apply (divides_to_lt_O O c)
446 rewrite > (sym_times e f).
447 apply (divides_times)
448 [ apply (divides_n_n)
449 | rewrite > H5 in H1.
450 apply (gcd_SO_to_divides_times_to_divides f e n)
461 (* the following theorem shows that gcd is a multiplicative function in
462 the following sense: if a1 and a2 are relatively prime, then
463 gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
465 theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat.
466 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
469 [ apply divides_times;
471 | apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c))
479 apply (divides_d_gcd b a d Hcut1 Hcut)
480 | apply (trans_divides d (gcd b c) b)
482 | apply (divides_gcd_n)
485 | apply (trans_divides d (gcd a c) a)
487 | apply (divides_gcd_n)
491 | apply (divides_gcd_m)
492 | apply (divides_gcd_m)
495 rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)).
496 rewrite > (sym_times (gcd a c) b).
497 rewrite > (sym_times (gcd a c) c).
498 rewrite < (eq_gcd_times_times_eqv_times_gcd a c b).
499 rewrite < (eq_gcd_times_times_eqv_times_gcd a c c).
500 apply (divides_d_gcd)
501 [ apply (divides_d_gcd)
502 [ rewrite > (times_n_SO d).
503 apply (divides_times)
507 | rewrite > (times_n_SO d).
508 apply (divides_times)
513 | apply (divides_d_gcd)
514 [ rewrite > (times_n_SO d).
515 rewrite > (sym_times d (S O)).
516 apply (divides_times)
517 [ apply (divides_SO_n)
520 | rewrite < (sym_times a b).
528 theorem gcd_eq_gcd_minus: \forall a,b:nat.
529 a \lt b \to (gcd a b) = (gcd (b - a) b).
533 [ apply (divides_minus (gcd a b) b a)
534 [ apply divides_gcd_m
535 | apply divides_gcd_n
537 | apply divides_gcd_m
542 [ cut (b - (d*n2) = a)
543 [ rewrite > H4 in Hcut1.
544 rewrite < (distr_times_minus d n n2) in Hcut1.
547 | apply (witness d a (n - n2)).
551 | apply (plus_to_minus ? ? ? Hcut)
553 | rewrite > sym_plus.
554 apply (minus_to_plus)