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/propr_div_mod_lt_le_totient1_aux/".
17 include "nat/iteration2.ma".
19 (*this part of the library contains some properties useful to prove
20 the main theorem in totient1.ma, and some new properties about gcd
21 (see gcd_properties1.ma).
22 These theorems are saved separately from the other part of the library
23 in order to avoid to create circular dependences in it.
26 (* some basic properties of and - or*)
27 theorem andb_sym: \forall A,B:bool.
28 (A \land B) = (B \land A).
36 theorem andb_assoc: \forall A,B,C:bool.
37 (A \land (B \land C)) = ((A \land B) \land C).
46 theorem orb_sym: \forall A,B:bool.
47 (A \lor B) = (B \lor A).
55 theorem andb_t_t_t: \forall A,B,C:bool.
56 A = true \to B = true \to C = true \to (A \land (B \land C)) = true.
64 (*properties about relational operators*)
66 theorem Sa_le_b_to_O_lt_b: \forall a,b:nat.
67 (S a) \le b \to O \lt b.
73 theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
74 (S O) \lt n \to O \lt (pred n).
79 | rewrite < (pred_Sn n1).
80 apply (lt_to_le_to_lt O (S (S O)) n1)
89 theorem NdivM_times_M_to_N: \forall n,m:nat.
90 O \lt m \to m \divides n \to (n / m) * m = n.
99 apply divides_to_mod_O;
105 theorem lt_to_divides_to_div_le: \forall a,c:nat.
106 O \lt c \to c \divides a \to a/c \le a.
108 apply (le_times_to_le c (a/c) a)
110 | rewrite > (sym_times c (a/c)).
111 rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?)
112 [ rewrite < (sym_times a c).
113 apply (O_lt_const_to_le_times_const).
122 theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
123 O \lt b \to (b*c) \le a \to c \le (a /b).
125 rewrite > (div_mod a b) in H1
126 [ apply (le_times_to_le b ? ?)
128 | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
130 [ rewrite < (sym_times c b).
131 rewrite < (sym_times (a/b) b).
134 [ change in Hcut1 with ((S (a/b)) \le c).
135 cut( b*(S (a/b)) \le b*c)
136 [ rewrite > (sym_times b (S (a/b))) in Hcut2.
138 cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
139 [ cut (b \le (a \mod b))
141 apply (lt_to_not_le (a \mod b) b)
142 [ apply (lt_mod_m_m).
146 | apply (le_plus_to_le ((a/b)*b)).
150 | apply (trans_le ? (b*c) ?);
153 | apply (le_times_r b ? ?).
156 | apply (lt_times_n_to_lt b (a/b) c)
162 | apply (leb_elim (c*b) ((a/b)*b))
168 apply cic:/matita/nat/orders/not_le_to_lt.con.
177 theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
179 O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
184 rewrite > (sym_times a n2).
185 rewrite > (div_times_ltO n2 a);
187 | apply (divides_to_lt_O n2 b)
189 | apply (witness n2 b a).
196 (* some properties of div operator between natural numbers *)
198 theorem separazioneFattoriSuDivisione: \forall a,b,c:nat.
199 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
203 rewrite > (sym_times c n2).
205 [ rewrite > (div_times_ltO n2 c)
206 [ rewrite < assoc_times.
207 rewrite > (div_times_ltO (a *n2) c)
213 | apply (divides_to_lt_O c b);
219 theorem div_times_to_eqSO: \forall a,d:nat.
220 O \lt d \to a*d = d \to a = (S O).
222 rewrite > (plus_n_O d) in H1:(? ? ? %).
224 [ rewrite > sym_times in Hcut.
225 rewrite > times_n_SO in Hcut:(? ? (? ? %) ?).
226 rewrite < distr_times_minus in Hcut.
227 cut ((a - (S O)) = O)
228 [ apply (minus_to_plus a (S O) O)
229 [ apply (nat_case1 a)
233 rewrite < (plus_n_O d) in H1.
236 change in H with ((S O) \le O).
237 apply (not_le_Sn_O O H)
244 | apply (lt_times_eq_O d (a - (S O)));
247 | apply (plus_to_minus ).
252 theorem div_mod_minus:
253 \forall a,b:nat. O \lt b \to
254 (a /b)*b = a - (a \mod b).
257 apply (inj_plus_r (a \mod b)).
258 rewrite > (sym_plus (a \mod b) ?).
259 rewrite < (plus_minus_m_m a (a \mod b))
260 [ rewrite > sym_plus.
263 | rewrite > (div_mod a b) in \vdash (? ? %)
264 [ rewrite > plus_n_O in \vdash (? % ?).
266 apply cic:/matita/nat/le_arith/le_plus_n.con
272 theorem sum_div_eq_div: \forall a,b,c:nat.
273 O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
277 rewrite > (sym_times c n2).
278 rewrite > (div_plus_times c n2 b)
279 [ rewrite > (div_times_ltO n2 c)
288 (* A corollary to the division theorem (between natural numbers).
290 * Forall a,b,c: Nat, b > O,
291 * a/b = c iff (b*c <= a && a < b*(c+1)
293 * two parts of the theorem are proved separately
294 * - (=>) th_div_interi_2
295 * - (<=) th_div_interi_1
298 theorem th_div_interi_2: \forall a,b,c:nat.
299 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
304 rewrite > div_mod_minus
305 [ apply (le_minus_m a (a \mod b))
308 | rewrite < (times_n_Sm b c).
311 rewrite > div_mod_minus
312 [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b))
313 [ rewrite < (sym_plus a b).
314 rewrite > (eq_minus_plus_plus_minus a b (a \mod b))
315 [ rewrite > (plus_n_O a) in \vdash (? % ?).
316 apply (le_to_lt_to_plus_lt)
318 | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con.
319 apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con.
326 | rewrite > (div_mod a b) in \vdash (? ? %)
327 [ rewrite > plus_n_O in \vdash (? % ?).
329 apply cic:/matita/nat/le_arith/le_plus_n.con
338 theorem th_div_interi_1: \forall a,c,b:nat.
339 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
341 apply (le_to_le_to_eq)
342 [ cut (a/b \le c \lor c \lt a/b)
345 | change in H3 with ((S c) \le (a/b)).
346 cut (b*(S c) \le (b*(a/b)))
347 [ rewrite > (sym_times b (S c)) in Hcut1.
348 cut (a \lt (b * (a/b)))
349 [ rewrite > (div_mod a b) in Hcut2:(? % ?)
350 [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %).
351 cut ((a \mod b) \lt O)
353 apply (lt_to_not_le (a \mod b) O)
357 | apply (lt_plus_to_lt_r ((a/b)*b)).
358 rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)).
363 | apply (lt_to_le_to_lt ? (b*(S c)) ?)
365 | rewrite > (sym_times b (S c)).
373 | apply (leb_elim (a/b) c)
379 apply cic:/matita/nat/orders/not_le_to_lt.con.
383 | apply (bTIMESc_le_a_to_c_le_aDIVb);
388 theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
389 O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
392 cut (b*d \le a \land a \lt b*(S d))
394 apply th_div_interi_1
395 [ rewrite > (S_pred b)
396 [ rewrite > (S_pred c)
397 [ apply (lt_O_times_S_S)
402 | rewrite > assoc_times.
403 rewrite > (sym_times c d).
404 rewrite < assoc_times.
405 rewrite > (sym_times (b*d) c).
406 rewrite > (sym_times a c).
407 apply (le_times_r c (b*d) a).
409 | rewrite > (sym_times a c).
410 rewrite > (assoc_times ).
411 rewrite > (sym_times c (S d)).
412 rewrite < (assoc_times).
413 rewrite > (sym_times (b*(S d)) c).
414 apply (lt_times_r1 c a (b*(S d)));
417 | apply (th_div_interi_2)
425 theorem times_numerator_denominator: \forall a,b,c:nat.
426 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
428 apply (times_numerator_denominator_aux a b c (a/b))
435 theorem times_mod: \forall a,b,c:nat.
436 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
438 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
439 [ apply div_mod_spec_intro
440 [ apply (lt_mod_m_m (a*c) (b*c)).
442 [ rewrite > (S_pred c)
443 [ apply lt_O_times_S_S
448 | rewrite > (times_numerator_denominator a b c)
449 [ apply (div_mod (a*c) (b*c)).
451 [ rewrite > (S_pred c)
452 [ apply (lt_O_times_S_S)
462 [ rewrite > (sym_times b c).
463 apply (lt_times_r1 c)
465 | apply (lt_mod_m_m).
468 | rewrite < (assoc_times (a/b) b c).
469 rewrite > (sym_times a c).
470 rewrite > (sym_times ((a/b)*b) c).
471 rewrite < (distr_times_plus c ? ?).