(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/totient1".
-
include "nat/totient.ma".
include "nat/iteration2.ma".
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 ? ?
[ 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.
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
| 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
[ split
[ reflexivity
| rewrite > Hcut3.
- apply (cic:/matita/Z/dirichlet_product/div_div.con);
+ apply (div_div);
assumption
]
| rewrite > Hcut3.
[ 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
]
]
projects / helm.git / blobdiff