Euler totient function is multiplicative!

diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma
index 5ebc08b6ce646d3e2b108cceab97967b4cad2c33..60bdbadc4c228ebc5019eea85d783fd70e00757d 100644 (file)
--- a/helm/matita/library/nat/count.ma
+++ b/helm/matita/library/nat/count.ma
@@ -123,7 +123,8 @@ theorem count_times:\forall n,m:nat.
 (count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
 intros.unfold count.
 rewrite < eq_map_iter_i_sigma.
-rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? (\lambda i.g (div i (S n)) (mod i (S n)))).
+rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? 
+           (\lambda i.g (div i (S n)) (mod i (S n)))).
 rewrite > eq_map_iter_i_sigma.
 rewrite > eq_sigma_sigma1.
 apply (trans_eq ? ?
@@ -131,8 +132,10 @@ apply (trans_eq ? ?
   sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O)).
 apply eq_sigma.intros.
 apply eq_sigma.intros.
-rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
-rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
+rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) 
+                                        ((i1*(S n) + i) \mod (S n)) i1 i).
+rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) 
+                                        ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.
 simplify.apply le_S_S.assumption.

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 792629aaa04c224689edcf2a152a3c2925aa547f..d42a57e8e8db6c1661d480d829bcf1d6289c96de 100644 (file)
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -390,6 +390,16 @@ rewrite < H.
 apply divides_gcd_nm.
 qed.
 
+theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
+intros.
+apply (nat_case1 (gcd m n)).
+intros.
+generalize in match (gcd_O_to_eq_O m n H1).
+intros.elim H2.
+rewrite < H4 in \vdash (? ? %).assumption.
+intros.simplify.apply le_S_S.apply le_O_n.
+qed.
+
 theorem symmetric_gcd: symmetric nat gcd.
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
@@ -418,6 +428,33 @@ qed.
 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 symmetric_gcd.
 
+theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
+intros.
+apply (nat_case n).reflexivity.
+intro.
+apply divides_to_le.
+apply lt_O_gcd.
+rewrite > (times_n_O O).
+apply lt_times.simplify.apply le_S_S.apply le_O_n.assumption.
+apply divides_d_gcd.
+apply (transitive_divides ? (S m1)).
+apply divides_gcd_m.
+apply (witness ? ? p).reflexivity.
+apply divides_gcd_n.
+qed.
+
+theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to 
+gcd m (n*p) = (S O) \to gcd m n = (S O).
+intros.
+apply antisymmetric_le.
+rewrite < H2.
+apply le_gcd_times.assumption.
+change with (O < gcd m n). 
+apply lt_O_gcd.assumption.
+qed.
+
+(* for the "converse" of the previous result see the end  of this development *)
+
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
 apply antisym_le.apply divides_to_le.simplify.apply le_n.
@@ -432,7 +469,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
-theorem divides_gcd_mod: \forall m,n:nat. O < n \to O < m \to
+theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 divides (gcd m n) (gcd n (m \mod n)).
 intros.
 apply divides_d_gcd.
@@ -442,7 +479,7 @@ apply divides_gcd_m.
 apply divides_gcd_m.
 qed.
 
-theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to
+theorem divides_mod_gcd: \forall m,n:nat. O < n \to
 divides (gcd n (m \mod n)) (gcd m n) .
 intros.
 apply divides_d_gcd.
@@ -453,6 +490,14 @@ apply divides_gcd_m.
 apply divides_gcd_n.
 qed.
 
+theorem gcd_mod: \forall m,n:nat. O < n \to
+(gcd n (m \mod n)) = (gcd m n) .
+intros.
+apply antisymmetric_divides.
+apply divides_mod_gcd.assumption.
+apply divides_gcd_mod.assumption.
+qed.
+
 (* gcd and primes *)
 
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
@@ -515,3 +560,49 @@ apply (decidable_divides n p).
 apply (trans_lt ? (S O)).simplify.apply le_n.
 simplify in H.elim H. assumption.
 qed.
+
+theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
+gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
+intros.
+apply antisymmetric_le.
+apply not_lt_to_le.
+unfold Not.intro.
+cut (divides (smallest_factor (gcd m (n*p))) n \lor 
+     divides (smallest_factor (gcd m (n*p))) p).
+elim Hcut.
+apply (not_le_Sn_n (S O)).
+change with ((S O) < (S O)).
+rewrite < H2 in \vdash (? ? %).
+apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
+apply lt_SO_smallest_factor.assumption.
+apply divides_to_le.
+rewrite > H2.simplify.apply le_n.
+apply divides_d_gcd.assumption.
+apply (transitive_divides ? (gcd m (n*p))).
+apply divides_smallest_factor_n.
+apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply divides_gcd_n.
+apply (not_le_Sn_n (S O)).
+change with ((S O) < (S O)).
+rewrite < H3 in \vdash (? ? %).
+apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
+apply lt_SO_smallest_factor.assumption.
+apply divides_to_le.
+rewrite > H3.simplify.apply le_n.
+apply divides_d_gcd.assumption.
+apply (transitive_divides ? (gcd m (n*p))).
+apply divides_smallest_factor_n.
+apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply divides_gcd_n.
+apply divides_times_to_divides.
+apply prime_smallest_factor_n.
+assumption.
+apply (transitive_divides ? (gcd m (n*p))).
+apply divides_smallest_factor_n.
+apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply divides_gcd_m.
+change with (O < gcd m (n*p)).
+apply lt_O_gcd.
+rewrite > (times_n_O O).
+apply lt_times.assumption.assumption.
+qed.

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 74fd74e7455de4b999461b2944efcd952fe96ad1..452adc89c9788ac726cdd661ffb83294865353bd 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -150,6 +150,23 @@ assumption.
 apply (decidable_le n m).
 qed.
 
+theorem antisymmetric_divides: antisymmetric nat divides.
+simplify.intros.elim H. elim H1.
+apply (nat_case1 n2).intro.
+rewrite > H3.rewrite > H2.rewrite > H4.
+rewrite < times_n_O.reflexivity.
+intros.
+apply (nat_case1 n).intro.
+rewrite > H2.rewrite > H3.rewrite > H5.
+rewrite < times_n_O.reflexivity.
+intros.
+apply antisymmetric_le.
+rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
+rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
+qed.
+
 (* divides le *)
 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
 intros. elim H1.rewrite > H2.cut (O < n2).

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index 6715fe854993ebce6ca7b668606ed9ab64c97f42..ff425772cd276d31b239c15bb35d5f5e6345ef50 100644 (file)
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -28,7 +28,6 @@ theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
 reflexivity.
 qed.
 
-(*
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intro.
@@ -66,4 +65,38 @@ rewrite > eq_to_eqb_true.
 rewrite > eq_to_eqb_true.
 reflexivity.
 rewrite < H4.
-*)
+rewrite > sym_gcd.
+rewrite > gcd_mod.
+apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
+simplify.apply le_S_S.apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
+assumption.
+simplify.apply le_S_S.apply le_O_n.
+rewrite < H5.
+rewrite > sym_gcd.
+rewrite > gcd_mod.
+apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
+simplify.apply le_S_S.apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
+rewrite > sym_times.
+assumption.
+simplify.apply le_S_S.apply le_O_n.
+intro.
+apply eqb_elim.
+intro.apply eqb_elim.
+intro.apply False_ind.
+apply H6.
+apply eq_gcd_times_SO.
+simplify.apply le_S_S.apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
+rewrite < gcd_mod.
+rewrite > H4.
+rewrite > sym_gcd.assumption.
+simplify.apply le_S_S.apply le_O_n.
+rewrite < gcd_mod.
+rewrite > H5.
+rewrite > sym_gcd.assumption.
+simplify.apply le_S_S.apply le_O_n.
+intro.reflexivity.
+intro.reflexivity.
+qed.
\ No newline at end of file