From abb8fb7bac467824eb6f21a540e08599e0824b2c Mon Sep 17 00:00:00 2001 From: Cristian Armentano Date: Thu, 20 Sep 2007 16:29:45 +0000 Subject: [PATCH] Further simplifications to the main theorem about Euler's totient function. --- matita/library/nat/totient1.ma | 57 +++++++++++++--------------------- 1 file changed, 21 insertions(+), 36 deletions(-) diff --git a/matita/library/nat/totient1.ma b/matita/library/nat/totient1.ma index 74018378a..c6b78ec90 100644 --- a/matita/library/nat/totient1.ma +++ b/matita/library/nat/totient1.ma @@ -25,24 +25,7 @@ include "nat/gcd_properties1.ma". number n is equal to n *) -(*simple auxiliary properties*) -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). @@ -140,22 +123,24 @@ apply (trans_eq ? ? ] | rewrite > associative_times. rewrite > (divides_to_div (n/(gcd x n)) n) - [ apply eq_div_times_div_times - [ assumption - | apply divides_gcd_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 (witness ? ? (gcd x n)). rewrite > divides_to_div [ reflexivity @@ -203,10 +188,10 @@ 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 ] @@ -214,7 +199,7 @@ apply (trans_eq ? ? | 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 ] -- 2.39.2