1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/totient1".
17 include "nat/totient.ma".
18 include "nat/iteration2.ma".
19 include "nat/gcd_properties1.ma".
21 (* This file contains the proof of the following theorem about Euler's totient
24 The sum of the applications of Phi function over the divisor of a natural
25 number n is equal to n
28 (*simple auxiliary properties*)
29 theorem lt_O_to_divides_to_lt_O_div:
31 O \lt b \to a \divides b \to O \lt (b/a).
33 apply (O_lt_times_to_O_lt ? a).
34 rewrite > (divides_to_div a b);
39 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.
43 (sigma_p (S n) (\lambda d:nat.divides_b d n)
44 (\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))))
51 (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
52 [ apply false_to_eq_sigma_p
56 rewrite > lt_to_leb_false
64 rewrite > le_to_leb_true
73 | apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
78 (\lambda p. n / (gcd p n))
79 (\lambda p. p / (gcd p n))
81 [ cut (O \lt (gcd x n))
86 [ apply divides_to_divides_b_true
87 [ apply (O_lt_times_to_O_lt ? (gcd x n)).
88 rewrite > (divides_to_div (gcd x n) n)
90 | apply (divides_gcd_m)
93 apply (divides_times_to_divides_div_gcd).
94 apply (witness n (x * n) x).
95 apply (symmetric_times x n)
97 | apply (true_to_true_to_andb_true)
98 [ apply (le_to_leb_true).
99 change with (x/(gcd x n) \lt n/(gcd x n)).
100 apply (lt_times_n_to_lt (gcd x n) ? ?)
102 | rewrite > (divides_to_div (gcd x n) x)
103 [ rewrite > (divides_to_div (gcd x n) n)
105 | apply divides_gcd_m
107 | apply divides_gcd_n
110 | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
111 rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
112 [ apply (div_n_n (gcd x n) Hcut)
114 | apply divides_gcd_n
115 | apply divides_gcd_m
119 | apply (inj_times_l1 (n/(gcd x n)))
120 [ apply lt_O_to_divides_to_lt_O_div
122 | apply divides_gcd_m
124 | rewrite > associative_times.
125 rewrite > (divides_to_div (n/(gcd x n)) n)
126 [ rewrite > sym_times.
127 rewrite > (divides_to_eq_times_div_div_times x)
128 [ apply (inj_times_l1 (gcd x n) Hcut).
129 rewrite > (divides_to_div (gcd x n) (x * n))
130 [ rewrite > assoc_times.
131 rewrite > (divides_to_div (gcd x n) x)
133 | apply divides_gcd_n
135 | apply (trans_divides ? x)
136 [ apply divides_gcd_n
137 | apply (witness ? ? n).
142 | apply divides_gcd_m
144 | apply (witness ? ? (gcd x n)).
145 rewrite > divides_to_div
147 | apply divides_gcd_m
152 | apply (le_to_lt_to_lt ? n)
155 | change with ((S n) \le (S n)).
159 | apply (le_to_lt_to_lt ? x)
162 | apply (trans_lt ? n ?)
164 | change with ((S n) \le (S n)).
169 | apply (divides_to_lt_O ? n)
171 | apply divides_gcd_m
176 [ cut ((gcd j i) = (S O) )
177 [ cut ((gcd (j*(n/i)) n) = n/i)
187 rewrite < divides_to_eq_times_div_div_times
191 | apply lt_O_to_divides_to_lt_O_div;
194 | apply lt_O_to_divides_to_lt_O_div;
199 | rewrite < (divides_to_div i n) in \vdash (? ? %)
200 [ rewrite > sym_times.
202 [ apply lt_O_to_divides_to_lt_O_div;
209 | rewrite < (divides_to_div i n) in \vdash (? ? (? ? %) ?)
210 [ rewrite > (sym_times j).
211 rewrite > times_n_SO in \vdash (? ? ? %).
213 apply eq_gcd_times_times_times_gcd
217 | apply eqb_true_to_eq.
218 apply (andb_true_true_r (leb (S j) i)).
221 | change with ((S j) \le i).
222 cut((leb (S j) i) = true)
225 [ true \Rightarrow ((S j) \leq i)
226 | false \Rightarrow ((S j) \nleq i)]
230 | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).
234 | apply (divides_b_true_to_divides).
238 | apply (sigma_p_true).