set "baseuri" "cic:/matita/nat/gcd_properties1".
-include "nat/propr_div_mod_lt_le_totient1_aux.ma".
+include "nat/gcd.ma".
(* this file contains some important properites of gcd in N *)
]
qed.
-theorem divides_times_to_gcd_to_divides_div: \forall a,b,c,d:nat.
-a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
+
+theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
+O \lt m \to m \divides a \to m \divides b \to
+(gcd (a/m) (b/m)) = (gcd a b) / m.
+intros.
+apply (inj_times_r1 m H).
+rewrite > (sym_times m ((gcd a b)/m)).
+rewrite > (divides_to_times_div (gcd a b) m)
+[ rewrite < eq_gcd_times_times_times_gcd.
+ rewrite > (sym_times m (a/m)).
+ rewrite > (sym_times m (b/m)).
+ rewrite > (divides_to_times_div a m H H1).
+ rewrite > (divides_to_times_div b m H H2).
+ reflexivity
+| assumption
+| apply divides_d_gcd;
+ assumption
+]
+qed.
+
+
+
+theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat.
+a \divides (b*c) \to (a/(gcd a b)) \divides c.
intros.
apply (nat_case1 a)
[ intros.
apply (nat_case1 b)
- [ intros.
- cut (d = O) (*this is an impossible case*)
+ [ (*It's an impossible situation*)
+ intros.
+ simplify.
+ apply divides_SO_n
+ | intros.
+ cut (c = O)
[ rewrite > Hcut.
- simplify.
- apply divides_SO_n
- | rewrite > H2 in H1.
- rewrite > H3 in H1.
- apply sym_eq.
- assumption
- ]
- | intros.
- cut (O \lt d)
- [ rewrite > (S_pred d Hcut).
- simplify.
- rewrite > H2 in H.
- cut (c = O)
- [ rewrite > Hcut1.
- apply (divides_n_n O)
- | apply (lt_times_eq_O b c)
- [ rewrite > H3.
- apply lt_O_S
- | apply antisymmetric_divides
- [ apply divides_n_O
- | assumption
- ]
+ apply (divides_n_n O)
+ | apply (lt_times_eq_O b c)
+ [ rewrite > H2.
+ apply lt_O_S
+ | apply antisymmetric_divides
+ [ apply divides_n_O
+ | rewrite < H1.
+ assumption
]
]
- | rewrite < H1.
- apply lt_O_gcd.
- rewrite > H3.
- apply lt_O_S
]
]
| intros.
- rewrite < H2.
+ rewrite < H1.
elim H.
- cut (d \divides a \land d \divides b)
- [ cut (O \lt a)
- [ cut (O \lt d)
- [ elim Hcut.
- rewrite < (NdivM_times_M_to_N a d) in H3
- [ rewrite < (NdivM_times_M_to_N b d) in H3
- [ cut (b/d*c = a/d*n2)
- [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
- [ apply (O_lt_times_to_O_lt (a/d) d).
- rewrite > (NdivM_times_M_to_N a d);
- assumption
- | apply (inj_times_r1 d ? ?)
- [ assumption
- | rewrite < (eq_gcd_times_times_times_gcd (a/d) (b/d) d).
- rewrite < (times_n_SO d).
- rewrite < (sym_times (a/d) d).
- rewrite < (sym_times (b/d) d).
- rewrite > (NdivM_times_M_to_N a d)
- [ rewrite > (NdivM_times_M_to_N b d);
- assumption
- | assumption
- | assumption
- ]
- ]
- | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
- ]
- | apply (inj_times_r1 d ? ?)
- [ assumption
- | rewrite > sym_times.
- rewrite > (sym_times d ((a/d) * n2)).
- rewrite > assoc_times.
- rewrite > (assoc_times (a/d) n2 d).
- rewrite > (sym_times c d).
- rewrite > (sym_times n2 d).
- rewrite < assoc_times.
- rewrite < (assoc_times (a/d) d n2).
- assumption
- ]
- ]
- | assumption
+ cut (O \lt a)
+ [ cut (O \lt (gcd a b))
+ [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
+ [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
+ rewrite > (divides_to_times_div a (gcd a b))
+ [ assumption
+ | assumption
+ | apply divides_gcd_n
+ ]
+ | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
+ [ apply eq_gcd_div_div_div_gcd
+ [ assumption
+ | apply divides_gcd_n
+ | apply divides_gcd_m
+ ]
+ | assumption
+ ]
+ | apply (witness ? ? n2).
+ apply (inj_times_r1 (gcd a b) Hcut1).
+ rewrite < assoc_times.
+ rewrite < sym_times in \vdash (? ? (? % ?) ?).
+ rewrite > (divides_to_times_div b (gcd a b))
+ [ rewrite < assoc_times in \vdash (? ? ? %).
+ rewrite < sym_times in \vdash (? ? ? (? % ?)).
+ rewrite > (divides_to_times_div a (gcd a b))
+ [ assumption
| assumption
+ | apply divides_gcd_n
]
| assumption
- | assumption
+ | apply divides_gcd_m
]
- | rewrite < H1.
- rewrite > sym_gcd.
- apply lt_O_gcd.
- assumption
]
- | rewrite > H2.
- apply lt_O_S
- ]
- | rewrite < H1.
- split
- [ apply divides_gcd_n
- | apply divides_gcd_m
+ | rewrite > sym_gcd.
+ apply lt_O_gcd.
+ assumption
]
- ]
+ | rewrite > H1.
+ apply lt_O_S
+ ]
]
qed.
qed.
-theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
-O \lt m \to m \divides a \to m \divides b \to
-(gcd (a/m) (b/m)) = (gcd a b) / m.
-intros.
-apply (inj_times_r1 m H).
-rewrite > (sym_times m ((gcd a b)/m)).
-rewrite > (NdivM_times_M_to_N (gcd a b) m)
-[ rewrite < eq_gcd_times_times_times_gcd.
- rewrite > (sym_times m (a/m)).
- rewrite > (sym_times m (b/m)).
- rewrite > (NdivM_times_M_to_N a m H H1).
- rewrite > (NdivM_times_M_to_N b m H H2).
- reflexivity
-| assumption
-| apply divides_d_gcd;
- assumption
-]
-qed.
-
theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat.
(gcd e f) = (S O) \to e \divides c \to f \divides c \to
(e*f) \divides c.
intros.
-apply (nat_case1 e)
-[ intros.
- apply (nat_case1 c)
- [ intros.
- simplify.
- apply (divides_n_n O).
- | intros.
- rewrite > H3 in H1.
- apply False_ind.
- cut (O \lt O)
- [ apply (le_to_not_lt O O)
- [ apply (le_n O)
- | assumption
- ]
- | apply (divides_to_lt_O O c)
- [ rewrite > H4.
- apply lt_O_S
- | assumption
- ]
- ]
- ]
-| intros.
- rewrite < H3.
+apply (nat_case1 c); intros
+[ apply divides_n_O
+| rewrite < H3.
elim H1.
elim H2.
rewrite > H5.
[ apply (divides_n_n)
| rewrite > H5 in H1.
apply (gcd_SO_to_divides_times_to_divides f e n)
- [ rewrite > H3.
- apply (lt_O_S m)
+ [ rewrite < H5 in H1.
+ rewrite > H3 in H1.
+ apply (divides_to_lt_O e (S m))
+ [ apply lt_O_S
+ | assumption
+ ]
| assumption
| assumption
]
]
]
qed.
-
-
(* the following theorem shows that gcd is a multiplicative function in
the following sense: if a1 and a2 are relatively prime, then
gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/".
-
-include "nat/iteration2.ma".
-
-(*this part of the library contains some properties useful to prove
- the main theorem in totient1.ma, and some new properties about gcd
- (see gcd_properties1.ma).
- These theorems are saved separately from the other part of the library
- in order to avoid to create circular dependences in it.
- *)
-
-(* some basic properties of and - or*)
-(*theorem andb_sym: \forall A,B:bool.
-(A \land B) = (B \land A).
-intros.
-elim A;
- elim B;
- simplify;
- reflexivity.
-qed.
-
-theorem andb_assoc: \forall A,B,C:bool.
-(A \land (B \land C)) = ((A \land B) \land C).
-intros.
-elim A;
- elim B;
- elim C;
- simplify;
- reflexivity.
-qed.
-
-theorem orb_sym: \forall A,B:bool.
-(A \lor B) = (B \lor A).
-intros.
-elim A;
- elim B;
- simplify;
- reflexivity.
-qed.
-
-theorem andb_t_t_t: \forall A,B,C:bool.
-A = true \to B = true \to C = true \to (A \land (B \land C)) = true.
-intros.
-rewrite > H.
-rewrite > H1.
-rewrite > H2.
-reflexivity.
-qed.
-*)
-(*properties about relational operators*)
-
-theorem Sa_le_b_to_O_lt_b: \forall a,b:nat.
-(S a) \le b \to O \lt b.
-intros.
-elim H;
- apply lt_O_S.
-qed.
-
-
-theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
-(S O) \lt n \to O \lt (pred n).
-intros.
-apply (Sa_le_b_to_O_lt_b (pred (S O)) (pred n) ?).
- apply (lt_pred (S O) n ? ?);
- [ apply (lt_O_S O)
- | apply (H)
- ]
-qed.
-
-
-theorem NdivM_times_M_to_N: \forall n,m:nat.
-O \lt m \to m \divides n \to (n / m) * m = n.
-intros.
-rewrite > plus_n_O.
-apply sym_eq.
-cut (n \mod m = O)
-[ rewrite < Hcut.
- apply div_mod.
- assumption
-| apply divides_to_mod_O;
- assumption.
-]
-qed.
-
-theorem lt_to_divides_to_div_le: \forall a,c:nat.
-O \lt c \to c \divides a \to a/c \le a.
-intros.
-apply (le_times_to_le c (a/c) a)
-[ assumption
-| rewrite > (sym_times c (a/c)).
- rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?)
- [ apply (le_times_n c a ?).
- assumption
- | assumption
- | assumption
- ]
-]
-qed.
-
-
-theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
-\forall a,b:nat.
-O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
-intros.
-elim H2.
-rewrite > H3.
-rewrite > (sym_times a n2).
-rewrite > (div_times_ltO n2 a)
-[ apply (divides_to_lt_O n2 b)
- [ assumption
- | apply (witness n2 b a).
- rewrite > sym_times.
- assumption
- ]
-| assumption
-]
-qed.
-
-(* some properties of div operator between natural numbers *)
-
-theorem separazioneFattoriSuDivisione: \forall a,b,c:nat.
-O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
-intros.
-elim H1.
-rewrite > H2.
-rewrite > (sym_times c n2).
-cut(O \lt c)
-[ rewrite > (div_times_ltO n2 c)
- [ rewrite < assoc_times.
- rewrite > (div_times_ltO (a *n2) c)
- [ reflexivity
- | assumption
- ]
- | assumption
- ]
-| apply (divides_to_lt_O c b);
- assumption.
-]
-qed.
-
-
-theorem div_mod_minus:
-\forall a,b:nat. O \lt b \to
-(a /b)*b = a - (a \mod b).
-intros.
-rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
-[ apply (minus_plus_m_m (times (div a b) b) (mod a b))
-| assumption
-]
-qed.
-
-
-(* A corollary to the division theorem (between natural numbers).
- *
- * Forall a,b,c: Nat, b > O,
- * a/b = c iff (b*c <= a && a < b*(c+1)
- *
- * two parts of the theorem are proved separately
- * - (=>) th_div_interi_2
- * - (<=) th_div_interi_1
- *)
-
-theorem th_div_interi_2: \forall a,b,c:nat.
-O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
-intros.
-split
-[ rewrite < H1.
- rewrite > sym_times.
- rewrite > div_mod_minus
- [ apply (le_minus_m a (a \mod b))
- | assumption
- ]
-| rewrite < (times_n_Sm b c).
- rewrite < H1.
- rewrite > sym_times.
- rewrite > (div_mod a b) in \vdash (? % ?)
- [ rewrite > (sym_plus b ((a/b)*b)).
- apply lt_plus_r.
- apply lt_mod_m_m.
- assumption
- | assumption
- ]
-]
-qed.
-
-
-theorem th_div_interi_1: \forall a,c,b:nat.
-O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
-intros.
-apply (le_to_le_to_eq)
-[ apply (leb_elim (a/b) c);intros
- [ assumption
- | cut (c \lt (a/b))
- [ apply False_ind.
- apply (lt_to_not_le (a \mod b) O)
- [ apply (lt_plus_to_lt_l ((a/b)*b)).
- simplify.
- rewrite < sym_plus.
- rewrite < div_mod
- [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
- [ assumption
- | rewrite > (sym_times (a/b) b).
- apply le_times_r.
- assumption
- ]
- | assumption
- ]
- | apply le_O_n
- ]
- | apply not_le_to_lt.
- assumption
- ]
- ]
-| apply (leb_elim c (a/b));intros
- [ assumption
- | cut((a/b) \lt c)
- [ apply False_ind.
- apply (lt_to_not_le (a \mod b) b)
- [ apply (lt_mod_m_m).
- assumption
- | apply (le_plus_to_le ((a/b)*b)).
- rewrite < (div_mod a b)
- [ apply (trans_le ? (b*c) ?)
- [ rewrite > (sym_times (a/b) b).
- rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
- rewrite < distr_times_plus.
- rewrite > sym_plus.
- simplify in \vdash (? (? ? %) ?).
- apply le_times_r.
- assumption
- | assumption
- ]
- | assumption
- ]
- ]
- | apply not_le_to_lt.
- assumption
- ]
- ]
-]
-qed.
-
-
-theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
-O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
-intros.
-apply sym_eq.
-cut (b*d \le a \land a \lt b*(S d))
-[ elim Hcut.
- apply th_div_interi_1
- [ rewrite > (S_pred b)
- [ rewrite > (S_pred c)
- [ apply (lt_O_times_S_S)
- | assumption
- ]
- | assumption
- ]
- | rewrite > assoc_times.
- rewrite > (sym_times c d).
- rewrite < assoc_times.
- rewrite > (sym_times (b*d) c).
- rewrite > (sym_times a c).
- apply (le_times_r c (b*d) a).
- assumption
- | rewrite > (sym_times a c).
- rewrite > (assoc_times ).
- rewrite > (sym_times c (S d)).
- rewrite < (assoc_times).
- rewrite > (sym_times (b*(S d)) c).
- apply (lt_times_r1 c a (b*(S d)));
- assumption
- ]
-| apply (th_div_interi_2)
- [ assumption
- | apply sym_eq.
- assumption
- ]
-]
-qed.
-
-theorem times_numerator_denominator: \forall a,b,c:nat.
-O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
-intros.
-apply (times_numerator_denominator_aux a b c (a/b))
-[ assumption
-| assumption
-| reflexivity
-]
-qed.
-
-theorem times_mod: \forall a,b,c:nat.
-O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
-intros.
-apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
-[ apply div_mod_spec_intro
- [ apply (lt_mod_m_m (a*c) (b*c)).
- rewrite > (S_pred b)
- [ rewrite > (S_pred c)
- [ apply lt_O_times_S_S
- | assumption
- ]
- | assumption
- ]
- | rewrite > (times_numerator_denominator a b c)
- [ apply (div_mod (a*c) (b*c)).
- rewrite > (S_pred b)
- [ rewrite > (S_pred c)
- [ apply (lt_O_times_S_S)
- | assumption
- ]
- | assumption
- ]
- | assumption
- | assumption
- ]
- ]
-| constructor 1
- [ rewrite > (sym_times b c).
- apply (lt_times_r1 c)
- [ assumption
- | apply (lt_mod_m_m).
- assumption
- ]
- | rewrite < (assoc_times (a/b) b c).
- rewrite > (sym_times a c).
- rewrite > (sym_times ((a/b)*b) c).
- rewrite < (distr_times_plus c ? ?).
- apply eq_f.
- apply (div_mod a b).
- assumption
- ]
-]
-qed.
-
-
-
-
-
-
-
-
-
-
-
include "nat/totient.ma".
include "nat/iteration2.ma".
-include "nat/propr_div_mod_lt_le_totient1_aux.ma".
include "nat/gcd_properties1.ma".
(* This file contains the proof of the following theorem about Euler's totient
The sum of the applications of Phi function over the divisor of a natural
number n is equal to n
*)
-
-(*two easy properties of gcd, directly obtainable from the more general theorem
- eq_gcd_times_times_eqv_times_gcd*)
-theorem gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO:\forall a,b,d:nat.
-O \lt d \to O \lt b \to gcd (b*d) (a*d) = d \to (gcd a b) = (S O).
+theorem eq_div_times_div_times: \forall a,b,c:nat.
+O \lt b \to b \divides a \to b \divides c \to
+a / b * c = a * (c/b).
intros.
-apply (inj_times_r1 d)
-[ assumption
-| rewrite < (times_n_SO d).
- rewrite < (eq_gcd_times_times_eqv_times_gcd a b d).
- rewrite > sym_gcd.
- rewrite > (sym_times d a).
- rewrite > (sym_times d b).
- assumption
-]
-qed.
-
-theorem gcd_SO_to_gcd_times: \forall a,b,c:nat.
-O \lt c \to (gcd a b) = (S O) \to (gcd (a*c) (b*c)) = c.
-intros.
-rewrite > (sym_times a c).
-rewrite > (sym_times b c).
-rewrite > (eq_gcd_times_times_eqv_times_gcd a b c).
-rewrite > H1.
-apply sym_eq.
-apply times_n_SO.
+elim H1.
+elim H2.
+rewrite > H3.
+rewrite > H4.
+rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))).
+rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?).
+rewrite > (lt_O_to_div_times ? ? H).
+rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)).
+rewrite > (sym_times b n2).
+rewrite > assoc_times.
+reflexivity.
qed.
-
-
-(* The proofs of the 6 sub-goals activated after the application of the theorem
- eq_sigma_p_gh in the proof of the main theorem
- *)
-
-
-
-(* 2nd*)
-theorem sum_divisor_totient1_aux2: \forall i,n:nat.
-(S O) \lt n \to i<n*n \to
- (i/n) \divides (pred n) \to
- (i \mod n) \lt (i/n) \to
- (gcd (i \mod n) (i/n)) = (S O) \to
- gcd (pred n) ((i\mod n)* (pred n)/(i/n)) = (pred n) / (i/n).
+
+theorem lt_O_to_divides_to_lt_O_div:
+\forall a,b:nat.
+O \lt b \to a \divides b \to O \lt (b/a).
intros.
-cut (O \lt (pred n))
-[ cut(O \lt (i/n))
- [ rewrite < (NdivM_times_M_to_N (pred n) (i/n)) in \vdash (? ? (? % ?) ?)
- [ rewrite > (sym_times ((pred n)/(i/n)) (i/n)).
- cut ((i \mod n)*(pred n)/(i/n) = (i \mod n) * ((pred n) / (i/n)))
- [ rewrite > Hcut2.
- apply (gcd_SO_to_gcd_times (i/n) (i \mod n) ((pred n)/(i/n)))
- [ apply (lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb (i/n) (pred n));
- assumption
- | rewrite > sym_gcd.
- assumption
- ]
- | apply sym_eq.
- apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n));
- assumption.
- ]
- | assumption
- | assumption
- ]
- | apply (divides_to_lt_O (i/n) (pred n));
- assumption
- ]
-| apply n_gt_Uno_to_O_lt_pred_n.
- assumption.
-]
-qed.
-
-(*3rd*)
-theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat.
-i < n*n \to (divides_b (i/n) (pred n) \land
- (leb (S(i\mod n)) (i/n) \land
- eqb (gcd (i\mod n) (i/n)) (S O))) =true
- \to
- (S (i\mod n)) \le (i/n).
-intros.
-cut (leb (S (i \mod n)) (i/n) = true)
-[ change with (
- match (true) with
- [ true \Rightarrow (S (i \mod n)) \leq (i/n)
- | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
- ).
- rewrite < Hcut.
- apply (leb_to_Prop (S(i \mod n)) (i/n))
-| apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
- apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
- (eqb (gcd (i\mod n) (i/n)) (S O))
- ).
- rewrite > andb_sym in \vdash (? ? (? % ?) ?).
- rewrite < (andb_assoc) in \vdash (? ? % ?).
- assumption
+apply (O_lt_times_to_O_lt ? a).
+rewrite > (divides_to_times_div b a)
+[ assumption
+| apply (divides_to_lt_O a b H H1)
+| assumption
]
qed.
-
-(*the following theorem is just a particular case of the theorem
- divides_times, prooved in primes.ma
- *)
-theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat.
-a \divides b \to a \divides (b*c).
-intros.
-rewrite > (times_n_SO a).
-apply (divides_times).
-assumption.
-apply divides_SO_n.
-qed.
-
-theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
-(S O) \lt n \to i < n*n \to
- (divides_b (i/n) (pred n)
-\land (leb (S(i\mod n)) (i/n)
-\land eqb (gcd (i\mod n) (i/n)) (S O)))
- =true
- \to i\mod n*pred n/(i/n)<(pred n).
-intros.
-apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
- ((i/n)*(pred n) / (i/n))
- (pred n))
-[ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/n)))
- [ apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
- assumption.
- | rewrite > (NdivM_times_M_to_N )
- [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
- [ apply (monotonic_lt_times_variant (pred n))
- [ apply n_gt_Uno_to_O_lt_pred_n.
- assumption
- | change with ((S (i\mod n)) \le (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
- assumption
- ]
- | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
+(*tha main theorem*)
+theorem sigma_p_Sn_divides_b_totient_n': \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
+intros.
+unfold totient.
+apply (trans_eq ? ?
+(sigma_p (S n) (\lambda d:nat.divides_b d n)
+(\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
+[ apply eq_sigma_p1
+ [ intros.
+ reflexivity
+ | intros.
+ apply sym_eq.
+ apply (trans_eq ? ?
+ (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
+ [ apply false_to_eq_sigma_p
+ [ apply lt_to_le.
+ assumption
+ | intros.
+ rewrite > lt_to_leb_false
+ [ reflexivity
+ | apply le_S_S.
assumption
- | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
- apply (divides_times).
- apply divides_n_n.
- apply divides_SO_n
+ ]
]
- | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
- assumption
- | rewrite > (times_n_SO (i/n)).
- rewrite > (sym_times (i \mod n) (pred n)).
- apply (divides_times)
- [ apply divides_b_true_to_divides.
- apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))).
- apply (andb_true_true
- ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)))
- (eqb (gcd (i\mod n) (i/n)) (S O))).
- rewrite < (andb_assoc) in \vdash (? ? % ?).
- assumption
- | apply divides_SO_n
+ | apply eq_sigma_p
+ [ intros.
+ rewrite > le_to_leb_true
+ [ reflexivity
+ | assumption
+ ]
+ | intros.
+ reflexivity
]
]
]
-| rewrite > (sym_times).
- rewrite > (div_times_ltO )
- [ apply (le_n (pred n))
- | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
- apply (aux_S_i_mod_n_le_i_div_n i n);
- assumption.
- ]
-]qed.
-
-
-(*4th*)
-theorem sum_divisor_totient1_aux_4: \forall j,n:nat.
-j \lt (pred n) \to (S O) \lt n \to
-((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n))
- \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n))
- ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n))
- \land (eqb
- (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)
- ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O))))
-=true.
-intros.
-cut (O \lt (pred n))
-[ cut ( O \lt (gcd (pred n) j))
- [ cut (j/(gcd (pred n) j) \lt n)
- [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j)
- [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j)
- [ rewrite > Hcut3.
- rewrite > Hcut4.
- apply andb_t_t_t
- [ apply divides_to_divides_b_true
- [ apply (lt_times_n_to_lt (gcd (pred n) j) O (pred n/gcd (pred n) j))
- [ assumption
- | rewrite > (sym_times O (gcd (pred n) j)).
- rewrite < (times_n_O (gcd (pred n) j)).
- rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+| apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
+ [ apply sym_eq.
+ apply (sigma_p_knm
+ (\lambda x. (S O))
+ (\lambda i,j.j*(n/i))
+ (\lambda p. n / (gcd p n))
+ (\lambda p. p / (gcd p n))
+ );intros
+ [ cut (O \lt (gcd x n))
+ [split
+ [ split
+ [ split
+ [ split
+ [ apply divides_to_divides_b_true
+ [ apply (O_lt_times_to_O_lt ? (gcd x n)).
+ rewrite > (divides_to_times_div n (gcd x n))
[ assumption
| assumption
- | apply (divides_gcd_n (pred n))
+ | apply (divides_gcd_m)
]
+ | rewrite > sym_gcd.
+ apply (divides_times_to_divides_div_gcd).
+ apply (witness n (x * n) x).
+ apply (symmetric_times x n)
]
- | apply (witness (pred n/(gcd (pred n) j)) (pred n) (gcd (pred n) j)).
- rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
- [ reflexivity
- | assumption
- | apply (divides_gcd_n (pred n))
- ]
- ]
- | apply (le_to_leb_true).
- apply lt_S_to_le.
- apply cic:/matita/algebra/finite_groups/lt_S_S.con.
- apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
- [ assumption
- | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
- [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+ | apply (true_to_true_to_andb_true)
+ [ apply (le_to_leb_true).
+ change with (x/(gcd x n) \lt n/(gcd x n)).
+ apply (lt_times_n_to_lt (gcd x n) ? ?)
[ assumption
+ | rewrite > (divides_to_times_div x (gcd x n))
+ [ rewrite > (divides_to_times_div n (gcd x n))
+ [ assumption
+ | assumption
+ | apply divides_gcd_m
+ ]
+ | assumption
+ | apply divides_gcd_n
+ ]
+ ]
+ | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
+ rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
+ [ apply (div_n_n (gcd x n) Hcut)
| assumption
| apply divides_gcd_n
+ | apply divides_gcd_m
]
- | assumption
- | rewrite > sym_gcd.
- apply divides_gcd_n
]
- ]
- | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
- apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j))
- [ assumption
- | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
+ ]
+ | apply (inj_times_l1 (n/(gcd x n)))
+ [ apply lt_O_to_divides_to_lt_O_div
[ assumption
- | simplify.
- rewrite > NdivM_times_M_to_N
+ | apply divides_gcd_m
+ ]
+ | rewrite > associative_times.
+ rewrite > (divides_to_times_div n (n/(gcd x n)))
+ [ apply eq_div_times_div_times
[ assumption
- | assumption
| apply divides_gcd_n
+ | apply divides_gcd_m
]
- ]
- | rewrite > NdivM_times_M_to_N
- [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
- [ reflexivity
- | assumption
- | rewrite > sym_gcd.
- apply divides_gcd_n
- ]
- | assumption
- | apply divides_gcd_n
- ]
- ]
- ]
- | apply (mod_plus_times).
- assumption
- ]
- | apply (div_plus_times).
- assumption
- ]
- | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
- [ assumption
- | rewrite > NdivM_times_M_to_N
- [ apply (lt_to_le_to_lt j (pred n) ?)
- [ assumption
- | apply (lt_to_le).
- apply (lt_to_le_to_lt ? n ?)
- [ change with ((S (pred n)) \le n).
- rewrite < (S_pred n)
- [ apply le_n
- | apply (trans_lt ? (S O) ?)
- [ change with ((S O) \le (S O)).
- apply (le_n (S O))
+ (*rewrite > sym_times.
+ rewrite > (divides_to_eq_times_div_div_times n).
+ rewrite > (divides_to_eq_times_div_div_times x).
+ rewrite > (sym_times n x).
+ reflexivity.
+ assumption.
+ apply divides_gcd_m.
+ apply (divides_to_lt_O (gcd x n)).
+ apply lt_O_gcd.
+ assumption.
+ apply divides_gcd_n.*)
+ | apply lt_O_to_divides_to_lt_O_div
+ [ assumption
+ | apply divides_gcd_m
+ ]
+ | apply (witness ? ? (gcd x n)).
+ rewrite > divides_to_times_div
+ [ reflexivity
| assumption
+ | apply divides_gcd_m
+
]
]
- | rewrite > (times_n_SO n) in \vdash (? % ?).
- apply (le_times n)
- [ apply (le_n n)
- | change with (O \lt (gcd (pred n) j)).
- assumption
- ]
- ]
+ ]
]
- | assumption
- | rewrite > sym_gcd.
- apply (divides_gcd_n)
- ]
- ]
- ]
- | rewrite > sym_gcd.
- apply (lt_O_gcd).
- assumption
- ]
-| apply n_gt_Uno_to_O_lt_pred_n.
- assumption
-]
-qed.
-
-
-
-
-(*5th*)
-theorem sum_divisor_totient1_aux5: \forall a,b,c:nat.
-O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to
-a / b * c / (c/b) = a.
-intros.
-elim H3.
-elim H4.
-cut (O \lt n)
-[ rewrite > H6 in \vdash (? ? (? ? %) ?).
- rewrite > sym_times in \vdash (? ? (? ? %) ?).
- rewrite > (div_times_ltO n b)
- [ cut (n \divides c)
- [ cut (a/b * c /n = a/b * (c/n))
- [ rewrite > Hcut2.
- cut (c/n = b)
- [ rewrite > Hcut3.
- apply (NdivM_times_M_to_N a b);
+ | apply (le_to_lt_to_lt ? n)
+ [ apply cic:/matita/Z/dirichlet_product/le_div.con.
assumption
- | rewrite > H6.
- apply (div_times_ltO b n).
- assumption
- ]
- | elim Hcut1.
- rewrite > H7.
- rewrite < assoc_times in \vdash (? ? (? % ?) ?).
- rewrite > (sym_times ((a/b)*n) n1).
- rewrite < (assoc_times n1 (a/b) n).
- rewrite > (div_times_ltO (n1*(a/b)) n)
- [ rewrite > (sym_times n n1).
- rewrite > (div_times_ltO n1 n)
- [ rewrite > (sym_times (a/b) n1).
- reflexivity
- | assumption
+ | change with ((S n) \le (S n)).
+ apply le_n
]
- | assumption
]
- ]
- | apply (witness n c b).
- rewrite > (sym_times n b).
- assumption
- ]
- | assumption
- ]
-| apply (divides_to_lt_O n c)
- [ assumption
- | apply (witness n c b).
- rewrite > sym_times.
- assumption
- ]
-]
-qed.
-
-
-(*6th*)
-theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
-j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
-intros.
-apply (nat_case1 n)
-[ intros.
- rewrite > H2 in H.
- apply False_ind.
- apply (not_le_Sn_O j H)
-| intros.
- rewrite < (pred_Sn m).
- rewrite < (times_n_Sm (S m) m).
- rewrite > (sym_plus (S m) ((S m) * m)).
- apply le_to_lt_to_plus_lt
- [ rewrite > (sym_times (S m) m).
- apply le_times_l.
- apply (lt_to_divides_to_div_le)
- [ apply (nat_case1 m)
- [ intros.
- rewrite > H3 in H2.
- rewrite > H2 in H1.
- apply False_ind.
- apply (le_to_not_lt (S O) (S O))
- [ apply le_n
- | assumption
- ]
- | intros.
- rewrite > sym_gcd in \vdash (? ? %).
- apply (lt_O_gcd j (S m1)).
- apply (lt_O_S m1)
- ]
- | apply divides_gcd_n
- ]
- | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
- [
- apply lt_to_divides_to_div_le
- [ apply (nat_case1 m)
- [ intros.
- rewrite > H3 in H2.
- rewrite > H2 in H1.
- apply False_ind.
- apply (le_to_not_lt (S O) (S O))
- [ apply le_n
- | assumption
+ | apply (le_to_lt_to_lt ? x)
+ [ apply cic:/matita/Z/dirichlet_product/le_div.con.
+ assumption
+ | apply (trans_lt ? n ?)
+ [ assumption
+ | change with ((S n) \le (S n)).
+ apply le_n
]
- | intros.
- rewrite > sym_gcd in \vdash (? ? %).
- apply (lt_O_gcd j (S m1)).
- apply (lt_O_S m1)
]
- | rewrite > sym_gcd in \vdash (? % ?).
- apply divides_gcd_n
- ]
- | rewrite > H2 in H.
- rewrite < (pred_Sn m) in H.
- apply (trans_lt j m (S m))
- [ assumption.
- | change with ((S m) \le (S m)).
- apply (le_n (S m))
]
- ]
- ]
-]
-qed.
-
-
-
-
-(* The main theorem, adding the hypotesis n > 1 (the cases n= 0
- and n = 1 are dealed as particular cases in theorem
- sum_divisor_totient)
- *)
-theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
-intros.
-unfold totient.
-apply (trans_eq ? ?
-(sigma_p n (\lambda d:nat.divides_b d (pred n))
-(\lambda d:nat.sigma_p n (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
- [ apply eq_sigma_p1
- [ intros.
- reflexivity
- | intros.
- apply sym_eq.
- apply (trans_eq ? ?
- (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
- [ apply false_to_eq_sigma_p
- [ apply lt_to_le.
- assumption
- | intros.
- rewrite > lt_to_leb_false
- [ reflexivity
- | apply le_S_S.
- assumption
- ]
- ]
- | apply eq_sigma_p
- [ intros.
- rewrite > le_to_leb_true
- [ reflexivity
- | assumption
- ]
- | intros.
- reflexivity
- ]
+ | apply (divides_to_lt_O ? n)
+ [ assumption
+ | apply divides_gcd_m
]
- ]
- | rewrite < (sigma_p2' n n
- (\lambda d:nat.divides_b d (pred n))
- (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
- (\lambda x,y.(S O))).
- apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
- [ apply (eq_sigma_p_gh
- (\lambda x:nat. (S O))
- (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) )
- (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
- (n*n)
- (pred n)
- (\lambda x:nat.
- divides_b (x/n) (pred n)
- \land (leb (S (x \mod n)) (x/n)
- \land eqb (gcd (x \mod n) (x/n)) (S O)))
- (\lambda x:nat.true)
- )
- [ intros.
- reflexivity
- | intros.
- cut ((i/n) \divides (pred n))
- [ cut ((i \mod n ) \lt (i/n))
- [ cut ((gcd (i \mod n) (i / n)) = (S O))
- [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
- [ rewrite > Hcut3.
- cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
- [ rewrite > Hcut4.
- cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
- [ rewrite > Hcut5.
- apply sym_eq.
- apply div_mod.
- apply (trans_lt O (S O) n)
- [ apply (lt_O_S O)
- | assumption
- ]
- | elim Hcut.
- rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
- rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
- rewrite > (div_times_ltO n2 (i/n))
- [ rewrite > H3.
- apply div_times_ltO.
- apply (divides_to_lt_O n2 (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply (witness n2 (pred n) (i/n)).
- rewrite > sym_times.
- assumption
- ]
- | apply (divides_to_lt_O (i/n) (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply (witness (i/n) (pred n) n2).
- assumption
- ]
- ]
- ]
- | elim Hcut.
- cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
- [ rewrite > Hcut4.
- rewrite > H3.
- rewrite < (sym_times n2 (i/n)).
- rewrite > (div_times_ltO n2 (i/n))
- [ rewrite > (div_times_ltO (i \mod n) n2)
- [ reflexivity
- | apply (divides_to_lt_O n2 (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply (witness n2 (pred n) (i/n)).
- rewrite > sym_times.
- assumption
- ]
- ]
- | apply (divides_to_lt_O (i/n) (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ ]
+ | cut (i \divides n)
+ [ cut (j \lt i)
+ [ cut ((gcd j i) = (S O) )
+ [ cut ((gcd (j*(n/i)) n) = n/i)
+ [ split
+ [ split
+ [ split
+ [ reflexivity
+ | rewrite > Hcut3.
+ apply (cic:/matita/Z/dirichlet_product/div_div.con);
+ assumption
+ ]
+ | rewrite > Hcut3.
+ rewrite < divides_to_eq_times_div_div_times
+ [ rewrite > div_n_n
+ [ apply sym_eq.
+ apply times_n_SO.
+ | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*)
assumption
- | assumption
- ]
]
- | apply (sym_eq).
- apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*)
assumption
- | assumption
- ]
+ | apply divides_n_n
]
]
- | apply (sum_divisor_totient1_aux2);
- assumption
+ | rewrite < (divides_to_times_div n i) in \vdash (? ? %)
+ [ rewrite > sym_times.
+ apply (lt_times_r1)
+ [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*)
+ assumption
+ | assumption
+ ]
+ | apply (divides_to_lt_O i n); assumption
+ | assumption
+ ]
]
- | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
- apply (andb_true_true
- (eqb (gcd (i\mod n) (i/n)) (S O))
- (leb (S (i\mod n)) (i/n))
- ).
- apply (andb_true_true
- ((eqb (gcd (i\mod n) (i/n)) (S O))
- \land
- (leb (S (i\mod n)) (i/n)))
- (divides_b (i/n) (pred n))
- ).
- rewrite > andb_sym.
- rewrite > andb_sym in \vdash (? ? (? ? %) ?).
- assumption
- ]
- | change with (S (i \mod n) \le (i/n)).
- cut (leb (S (i \mod n)) (i/n) = true)
- [ change with (
- match (true) with
- [ true \Rightarrow (S (i \mod n)) \leq (i/n)
- | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
- ).
- rewrite < Hcut1.
- apply (leb_to_Prop (S(i \mod n)) (i/n))
- | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
- apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
- (eqb (gcd (i\mod n) (i/n)) (S O))
- ).
- rewrite > andb_sym in \vdash (? ? (? % ?) ?).
- rewrite < (andb_assoc) in \vdash (? ? % ?).
- assumption
- ]
- ]
- | apply (divides_b_true_to_divides ).
- apply (andb_true_true (divides_b (i/n) (pred n))
- (leb (S (i\mod n)) (i/n))).
- apply (andb_true_true ( (divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)) )
- (eqb (gcd (i\mod n) (i/n)) (S O))
- ).
- rewrite < andb_assoc.
- assumption.
- ]
- | intros.
- apply (sum_divisor_totient1_aux_3);
- assumption.
- | intros.
- apply (sum_divisor_totient1_aux_4);
- assumption.
- | intros.
- cut (j/(gcd (pred n) j) \lt n)
- [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
- [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
- [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
- [ apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | rewrite > sym_gcd.
- apply lt_O_gcd.
- apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
+ | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?)
+ [ rewrite > (sym_times j).
+ rewrite > times_n_SO in \vdash (? ? ? %).
+ rewrite < Hcut2.
+ apply eq_gcd_times_times_times_gcd.
+ | apply (divides_to_lt_O i n); assumption
| assumption
- | apply divides_gcd_m
- | rewrite > sym_gcd.
- apply divides_gcd_m
]
- | assumption
]
- | assumption
+ | apply eqb_true_to_eq.
+ apply (andb_true_true_r (leb (S j) i)).
+ assumption
]
- | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
- [ apply (lt_to_divides_to_div_le)
- [ rewrite > sym_gcd.
- apply lt_O_gcd.
- apply (n_gt_Uno_to_O_lt_pred_n n).
- assumption
- | apply divides_gcd_m
- ]
- | apply (lt_to_le_to_lt j (pred n) n)
- [ assumption
- | apply le_pred_n
- ]
+ | change with ((S j) \le i).
+ cut((leb (S j) i) = true)
+ [ change with(
+ match (true) with
+ [ true \Rightarrow ((S j) \leq i)
+ | false \Rightarrow ((S j) \nleq i)]
+ ).
+ rewrite < Hcut1.
+ apply (leb_to_Prop)
+ | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).
+ assumption
]
]
- | intros.
- apply (sum_divisor_totient1_aux_6);
- assumption.
+ | apply (divides_b_true_to_divides).
+ assumption
]
- | apply (sigma_p_true).
]
- ]
-qed.
-
-
-(*there's a little difference between the following definition of the
- theorem, and the abstract definition given before.
- in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
- that's why in the definition of the theorem the summary is set equal to
- (pred n).
- *)
-theorem sum_divisor_totient: \forall n.
-sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
-intros.
-apply (nat_case1 n)
-[ intros.
- simplify.
- reflexivity
-| intros.
- apply (nat_case1 m)
- [ intros.
- simplify.
- reflexivity
- | intros.
- rewrite < H1.
- rewrite < H.
- rewrite > (pred_Sn m).
- rewrite < H.
- apply( sum_divisor_totient1).
- rewrite > H.
- rewrite > H1.
- apply cic:/matita/algebra/finite_groups/lt_S_S.con.
- apply lt_O_S
+ | apply (sigma_p_true).
]
]
-qed.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+qed.
+
+
projects / helm.git / commitdiff