X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftotient1.ma;h=e12c85adbe5e171962595ca9f4343d4b36686c81;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=3d6b6fafcfbc1b5817732e3b2d09702b86ee250b;hpb=6d49a181a1b771f797d37b02661b5743aee86ac1;p=helm.git diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma index 3d6b6fafc..e12c85adb 100644 --- a/helm/software/matita/library/nat/totient1.ma +++ b/helm/software/matita/library/nat/totient1.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/totient1". - include "nat/totient.ma". include "nat/iteration2.ma". include "nat/gcd_properties1.ma". @@ -25,37 +23,18 @@ include "nat/gcd_properties1.ma". number n is equal to n *) -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. -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. - +(*simple auxiliary properties*) 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. 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 -] +rewrite > (divides_to_div a b); + assumption. qed. (*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. +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 ? ? @@ -104,9 +83,8 @@ apply (trans_eq ? ? [ 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)) + rewrite > (divides_to_div (gcd x n) n) [ assumption - | assumption | apply (divides_gcd_m) ] | rewrite > sym_gcd. @@ -119,17 +97,15 @@ apply (trans_eq ? ? 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)) + | rewrite > (divides_to_div (gcd x n) x) + [ rewrite > (divides_to_div (gcd x n) n) [ assumption - | assumption | apply divides_gcd_m ] - | assumption | apply divides_gcd_n ] ] - | apply cic:/matita/nat/compare/eq_to_eqb_true.con. + | apply eq_to_eqb_true. rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n)) [ apply (div_n_n (gcd x n) Hcut) | assumption @@ -144,46 +120,42 @@ apply (trans_eq ? ? | apply divides_gcd_m ] | rewrite > associative_times. - rewrite > (divides_to_times_div n (n/(gcd x n))) - [ apply eq_div_times_div_times - [ assumption - | apply divides_gcd_n + rewrite > (divides_to_div (n/(gcd x n)) n) + [ rewrite > sym_times. + rewrite > (divides_to_eq_times_div_div_times x) + [ apply (inj_times_l1 (gcd x n) Hcut). + rewrite > (divides_to_div (gcd x n) (x * n)) + [ rewrite > assoc_times. + rewrite > (divides_to_div (gcd x n) x) + [ apply sym_times + | apply divides_gcd_n + ] + | apply (trans_divides ? x) + [ apply divides_gcd_n + | apply (witness ? ? n). + reflexivity + ] + ] + | assumption | apply divides_gcd_m - ] - (*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 + rewrite > divides_to_div [ reflexivity - | assumption - | apply divides_gcd_m - + | apply divides_gcd_m ] ] ] ] | apply (le_to_lt_to_lt ? n) - [ apply cic:/matita/Z/dirichlet_product/le_div.con. + [ apply le_div. assumption | change with ((S n) \le (S n)). apply le_n ] ] | apply (le_to_lt_to_lt ? x) - [ apply cic:/matita/Z/dirichlet_product/le_div.con. + [ apply le_div. assumption | apply (trans_lt ? n ?) [ assumption @@ -206,7 +178,7 @@ apply (trans_eq ? ? [ split [ reflexivity | rewrite > Hcut3. - apply (cic:/matita/Z/dirichlet_product/div_div.con); + apply (div_div); assumption ] | rewrite > Hcut3. @@ -214,31 +186,29 @@ apply (trans_eq ? ? [ rewrite > div_n_n [ apply sym_eq. apply times_n_SO. - | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*) + | apply lt_O_to_divides_to_lt_O_div; assumption ] - | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*) + | apply lt_O_to_divides_to_lt_O_div; assumption | apply divides_n_n ] ] - | rewrite < (divides_to_times_div n i) in \vdash (? ? %) + | rewrite < (divides_to_div i n) in \vdash (? ? %) [ rewrite > sym_times. apply (lt_times_r1) - [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*) + [ apply lt_O_to_divides_to_lt_O_div; assumption | assumption ] - | apply (divides_to_lt_O i n); assumption | assumption ] ] - | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?) + | rewrite < (divides_to_div i n) 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 + apply eq_gcd_times_times_times_gcd | assumption ] ]