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 theorem eq_div_times_div_times: \forall a,b,c:nat.
29 O \lt b \to b \divides a \to b \divides c \to
30 a / b * c = a * (c/b).
36 rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))).
37 rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?).
38 rewrite > (lt_O_to_div_times ? ? H).
39 rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)).
40 rewrite > (sym_times b n2).
41 rewrite > assoc_times.
45 theorem lt_O_to_divides_to_lt_O_div:
47 O \lt b \to a \divides b \to O \lt (b/a).
49 apply (O_lt_times_to_O_lt ? a).
50 rewrite > (divides_to_times_div b a)
52 | apply (divides_to_lt_O a b H H1)
58 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.
62 (sigma_p (S n) (\lambda d:nat.divides_b d n)
63 (\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))))
70 (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
71 [ apply false_to_eq_sigma_p
75 rewrite > lt_to_leb_false
83 rewrite > le_to_leb_true
92 | apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
97 (\lambda p. n / (gcd p n))
98 (\lambda p. p / (gcd p n))
100 [ cut (O \lt (gcd x n))
105 [ apply divides_to_divides_b_true
106 [ apply (O_lt_times_to_O_lt ? (gcd x n)).
107 rewrite > (divides_to_times_div n (gcd x n))
110 | apply (divides_gcd_m)
113 apply (divides_times_to_divides_div_gcd).
114 apply (witness n (x * n) x).
115 apply (symmetric_times x n)
117 | apply (true_to_true_to_andb_true)
118 [ apply (le_to_leb_true).
119 change with (x/(gcd x n) \lt n/(gcd x n)).
120 apply (lt_times_n_to_lt (gcd x n) ? ?)
122 | rewrite > (divides_to_times_div x (gcd x n))
123 [ rewrite > (divides_to_times_div n (gcd x n))
126 | apply divides_gcd_m
129 | apply divides_gcd_n
132 | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
133 rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
134 [ apply (div_n_n (gcd x n) Hcut)
136 | apply divides_gcd_n
137 | apply divides_gcd_m
141 | apply (inj_times_l1 (n/(gcd x n)))
142 [ apply lt_O_to_divides_to_lt_O_div
144 | apply divides_gcd_m
146 | rewrite > associative_times.
147 rewrite > (divides_to_times_div n (n/(gcd x n)))
148 [ apply eq_div_times_div_times
150 | apply divides_gcd_n
151 | apply divides_gcd_m
153 (*rewrite > sym_times.
154 rewrite > (divides_to_eq_times_div_div_times n).
155 rewrite > (divides_to_eq_times_div_div_times x).
156 rewrite > (sym_times n x).
160 apply (divides_to_lt_O (gcd x n)).
163 apply divides_gcd_n.*)
164 | apply lt_O_to_divides_to_lt_O_div
166 | apply divides_gcd_m
168 | apply (witness ? ? (gcd x n)).
169 rewrite > divides_to_times_div
172 | apply divides_gcd_m
178 | apply (le_to_lt_to_lt ? n)
179 [ apply cic:/matita/Z/dirichlet_product/le_div.con.
181 | change with ((S n) \le (S n)).
185 | apply (le_to_lt_to_lt ? x)
186 [ apply cic:/matita/Z/dirichlet_product/le_div.con.
188 | apply (trans_lt ? n ?)
190 | change with ((S n) \le (S n)).
195 | apply (divides_to_lt_O ? n)
197 | apply divides_gcd_m
202 [ cut ((gcd j i) = (S O) )
203 [ cut ((gcd (j*(n/i)) n) = n/i)
209 apply (cic:/matita/Z/dirichlet_product/div_div.con);
213 rewrite < divides_to_eq_times_div_div_times
217 | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*)
220 | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*)
225 | rewrite < (divides_to_times_div n i) in \vdash (? ? %)
226 [ rewrite > sym_times.
228 [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*)
232 | apply (divides_to_lt_O i n); assumption
236 | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?)
237 [ rewrite > (sym_times j).
238 rewrite > times_n_SO in \vdash (? ? ? %).
240 apply eq_gcd_times_times_times_gcd.
241 | apply (divides_to_lt_O i n); assumption
245 | apply eqb_true_to_eq.
246 apply (andb_true_true_r (leb (S j) i)).
249 | change with ((S j) \le i).
250 cut((leb (S j) i) = true)
253 [ true \Rightarrow ((S j) \leq i)
254 | false \Rightarrow ((S j) \nleq i)]
258 | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).
262 | apply (divides_b_true_to_divides).
266 | apply (sigma_p_true).