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/propr_div_mod_lt_le_totient1_aux.ma".
20 include "nat/gcd_properties1.ma".
22 (* This file contains the proof of the following theorem about Euler's totient
25 The sum of the applications of Phi function over the divisor of a natural
26 number n is equal to n
29 (*two easy properties of gcd, directly obtainable from the more general theorem
30 eq_gcd_times_times_eqv_times_gcd*)
32 theorem gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO:\forall a,b,d:nat.
33 O \lt d \to O \lt b \to gcd (b*d) (a*d) = d \to (gcd a b) = (S O).
35 apply (inj_times_r1 d)
37 | rewrite < (times_n_SO d).
38 rewrite < (eq_gcd_times_times_eqv_times_gcd a b d).
40 rewrite > (sym_times d a).
41 rewrite > (sym_times d b).
46 theorem gcd_SO_to_gcd_times: \forall a,b,c:nat.
47 O \lt c \to (gcd a b) = (S O) \to (gcd (a*c) (b*c)) = c.
49 rewrite > (sym_times a c).
50 rewrite > (sym_times b c).
51 rewrite > (eq_gcd_times_times_eqv_times_gcd a b c).
58 (* The proofs of the 6 sub-goals activated after the application of the theorem
59 eq_sigma_p_gh in the proof of the main theorem
65 theorem sum_divisor_totient1_aux2: \forall i,n:nat.
66 (S O) \lt n \to i<n*n \to
67 (i/n) \divides (pred n) \to
68 (i \mod n) \lt (i/n) \to
69 (gcd (i \mod n) (i/n)) = (S O) \to
70 gcd (pred n) ((i\mod n)* (pred n)/(i/n)) = (pred n) / (i/n).
74 [ rewrite < (NdivM_times_M_to_N (pred n) (i/n)) in \vdash (? ? (? % ?) ?)
75 [ rewrite > (sym_times ((pred n)/(i/n)) (i/n)).
76 cut ((i \mod n)*(pred n)/(i/n) = (i \mod n) * ((pred n) / (i/n)))
78 apply (gcd_SO_to_gcd_times (i/n) (i \mod n) ((pred n)/(i/n)))
79 [ apply (lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb (i/n) (pred n));
85 apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n));
91 | apply (divides_to_lt_O (i/n) (pred n));
94 | apply n_gt_Uno_to_O_lt_pred_n.
100 theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat.
101 i < n*n \to (divides_b (i/n) (pred n) \land
102 (leb (S(i\mod n)) (i/n) \land
103 eqb (gcd (i\mod n) (i/n)) (S O))) =true
105 (S (i\mod n)) \le (i/n).
107 cut (leb (S (i \mod n)) (i/n) = true)
110 [ true \Rightarrow (S (i \mod n)) \leq (i/n)
111 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
114 apply (leb_to_Prop (S(i \mod n)) (i/n))
115 | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
116 apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
117 (eqb (gcd (i\mod n) (i/n)) (S O))
119 rewrite > andb_sym in \vdash (? ? (? % ?) ?).
120 rewrite < (andb_assoc) in \vdash (? ? % ?).
126 (*the following theorem is just a particular case of the theorem
127 divides_times, prooved in primes.ma
129 theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat.
130 a \divides b \to a \divides (b*c).
132 rewrite > (times_n_SO a).
133 apply (divides_times).
138 theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
139 (S O) \lt n \to i < n*n \to
140 (divides_b (i/n) (pred n)
141 \land (leb (S(i\mod n)) (i/n)
142 \land eqb (gcd (i\mod n) (i/n)) (S O)))
144 \to i\mod n*pred n/(i/n)<(pred n).
146 apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
147 ((i/n)*(pred n) / (i/n))
149 [ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/n)))
150 [ apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
151 apply (aux_S_i_mod_n_le_i_div_n i n);
153 | rewrite > (NdivM_times_M_to_N )
154 [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
155 [ apply (monotonic_lt_times_variant (pred n))
156 [ apply n_gt_Uno_to_O_lt_pred_n.
158 | change with ((S (i\mod n)) \le (i/n)).
159 apply (aux_S_i_mod_n_le_i_div_n i n);
162 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
163 apply (aux_S_i_mod_n_le_i_div_n i n);
165 | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
166 apply (divides_times).
170 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
171 apply (aux_S_i_mod_n_le_i_div_n i n);
173 | rewrite > (times_n_SO (i/n)).
174 rewrite > (sym_times (i \mod n) (pred n)).
175 apply (divides_times)
176 [ apply divides_b_true_to_divides.
177 apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))).
178 apply (andb_true_true
179 ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)))
180 (eqb (gcd (i\mod n) (i/n)) (S O))).
181 rewrite < (andb_assoc) in \vdash (? ? % ?).
187 | rewrite > (sym_times).
188 rewrite > (div_times_ltO )
189 [ apply (le_n (pred n))
190 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
191 apply (aux_S_i_mod_n_le_i_div_n i n);
198 theorem sum_divisor_totient1_aux_4: \forall j,n:nat.
199 j \lt (pred n) \to (S O) \lt n \to
200 ((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n))
201 \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n))
202 ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n))
204 (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)
205 ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O))))
209 [ cut ( O \lt (gcd (pred n) j))
210 [ cut (j/(gcd (pred n) j) \lt n)
211 [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j)
212 [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j)
216 [ apply divides_to_divides_b_true
217 [ apply (lt_times_n_to_lt (gcd (pred n) j) O (pred n/gcd (pred n) j))
219 | rewrite > (sym_times O (gcd (pred n) j)).
220 rewrite < (times_n_O (gcd (pred n) j)).
221 rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
224 | apply (divides_gcd_n (pred n))
227 | apply (witness (pred n/(gcd (pred n) j)) (pred n) (gcd (pred n) j)).
228 rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
231 | apply (divides_gcd_n (pred n))
234 | apply (le_to_leb_true).
236 apply cic:/matita/algebra/finite_groups/lt_S_S.con.
237 apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
239 | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
240 [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
243 | apply divides_gcd_n
250 | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
251 apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j))
253 | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
256 rewrite > NdivM_times_M_to_N
259 | apply divides_gcd_n
262 | rewrite > NdivM_times_M_to_N
263 [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
270 | apply divides_gcd_n
274 | apply (mod_plus_times).
277 | apply (div_plus_times).
280 | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
282 | rewrite > NdivM_times_M_to_N
283 [ apply (lt_to_le_to_lt j (pred n) ?)
286 apply (lt_to_le_to_lt ? n ?)
287 [ change with ((S (pred n)) \le n).
290 | apply (trans_lt ? (S O) ?)
291 [ change with ((S O) \le (S O)).
296 | rewrite > (times_n_SO n) in \vdash (? % ?).
299 | change with (O \lt (gcd (pred n) j)).
306 apply (divides_gcd_n)
314 | apply n_gt_Uno_to_O_lt_pred_n.
323 theorem sum_divisor_totient1_aux5: \forall a,b,c:nat.
324 O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to
325 a / b * c / (c/b) = a.
330 [ rewrite > H6 in \vdash (? ? (? ? %) ?).
331 rewrite > sym_times in \vdash (? ? (? ? %) ?).
332 rewrite > (div_times_ltO n b)
334 [ cut (a/b * c /n = a/b * (c/n))
338 apply (NdivM_times_M_to_N a b);
341 apply (div_times_ltO b n).
346 rewrite < assoc_times in \vdash (? ? (? % ?) ?).
347 rewrite > (sym_times ((a/b)*n) n1).
348 rewrite < (assoc_times n1 (a/b) n).
349 rewrite > (div_times_ltO (n1*(a/b)) n)
350 [ rewrite > (sym_times n n1).
351 rewrite > (div_times_ltO n1 n)
352 [ rewrite > (sym_times (a/b) n1).
359 | apply (witness n c b).
360 rewrite > (sym_times n b).
365 | apply (nat_case1 n)
368 rewrite > sym_times in H6.
372 change in H with ((S O) \le O).
373 apply (not_le_Sn_O O H)
382 theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
383 j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
389 apply (not_le_Sn_O j H)
391 rewrite < (pred_Sn m).
392 rewrite < (times_n_Sm (S m) m).
393 rewrite > (sym_plus (S m) ((S m) * m)).
394 apply le_to_lt_to_plus_lt
395 [ rewrite > (sym_times (S m) m).
397 apply (lt_to_divides_to_div_le)
398 [ apply (nat_case1 m)
403 apply (le_to_not_lt (S O) (S O))
408 rewrite > sym_gcd in \vdash (? ? %).
409 apply (lt_O_gcd j (S m1)).
412 | apply divides_gcd_n
414 | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
416 apply lt_to_divides_to_div_le
417 [ apply (nat_case1 m)
422 apply (le_to_not_lt (S O) (S O))
427 rewrite > sym_gcd in \vdash (? ? %).
428 apply (lt_O_gcd j (S m1)).
431 | rewrite > sym_gcd in \vdash (? % ?).
435 rewrite < (pred_Sn m) in H.
436 apply (trans_lt j m (S m))
438 | change with ((S m) \le (S m)).
449 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
450 and n = 1 are dealed as particular cases in theorem
453 theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
457 (sigma_p n (\lambda d:nat.divides_b d (pred n))
458 (\lambda d:nat.sigma_p n (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
465 (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
466 [ apply false_to_eq_sigma_p
470 rewrite > lt_to_leb_false
478 rewrite > le_to_leb_true
487 | rewrite < (sigma_p2' n n
488 (\lambda d:nat.divides_b d (pred n))
489 (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
490 (\lambda x,y.(S O))).
491 apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
492 [ apply (eq_sigma_p_gh
493 (\lambda x:nat. (S O))
494 (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) )
495 (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
499 divides_b (x/n) (pred n)
500 \land (leb (S (x \mod n)) (x/n)
501 \land eqb (gcd (x \mod n) (x/n)) (S O)))
507 cut ((i/n) \divides (pred n))
508 [ cut ((i \mod n ) \lt (i/n))
509 [ cut ((gcd (i \mod n) (i / n)) = (S O))
510 [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
512 cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
514 cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
518 apply (trans_lt O (S O) n)
523 rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
524 rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
525 rewrite > (div_times_ltO n2 (i/n))
528 apply (divides_to_lt_O n2 (pred n))
529 [ apply (n_gt_Uno_to_O_lt_pred_n n).
531 | apply (witness n2 (pred n) (i/n)).
535 | apply (divides_to_lt_O (i/n) (pred n))
536 [ apply (n_gt_Uno_to_O_lt_pred_n n).
538 | apply (witness (i/n) (pred n) n2).
544 cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
547 rewrite < (sym_times n2 (i/n)).
548 rewrite > (div_times_ltO n2 (i/n))
549 [ rewrite > (div_times_ltO (i \mod n) n2)
551 | apply (divides_to_lt_O n2 (pred n))
552 [ apply (n_gt_Uno_to_O_lt_pred_n n).
554 | apply (witness n2 (pred n) (i/n)).
559 | apply (divides_to_lt_O (i/n) (pred n))
560 [ apply (n_gt_Uno_to_O_lt_pred_n n).
566 apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
567 [ apply (n_gt_Uno_to_O_lt_pred_n n).
573 | apply (sum_divisor_totient1_aux2);
576 | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
577 apply (andb_true_true
578 (eqb (gcd (i\mod n) (i/n)) (S O))
579 (leb (S (i\mod n)) (i/n))
581 apply (andb_true_true
582 ((eqb (gcd (i\mod n) (i/n)) (S O))
584 (leb (S (i\mod n)) (i/n)))
585 (divides_b (i/n) (pred n))
588 rewrite > andb_sym in \vdash (? ? (? ? %) ?).
591 | change with (S (i \mod n) \le (i/n)).
592 cut (leb (S (i \mod n)) (i/n) = true)
595 [ true \Rightarrow (S (i \mod n)) \leq (i/n)
596 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
599 apply (leb_to_Prop (S(i \mod n)) (i/n))
600 | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
601 apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
602 (eqb (gcd (i\mod n) (i/n)) (S O))
604 rewrite > andb_sym in \vdash (? ? (? % ?) ?).
605 rewrite < (andb_assoc) in \vdash (? ? % ?).
609 | apply (divides_b_true_to_divides ).
610 apply (andb_true_true (divides_b (i/n) (pred n))
611 (leb (S (i\mod n)) (i/n))).
612 apply (andb_true_true ( (divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)) )
613 (eqb (gcd (i\mod n) (i/n)) (S O))
615 rewrite < andb_assoc.
619 apply (sum_divisor_totient1_aux_3);
622 apply (sum_divisor_totient1_aux_4);
625 cut (j/(gcd (pred n) j) \lt n)
626 [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
627 [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
628 [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
629 [ apply (n_gt_Uno_to_O_lt_pred_n n).
633 apply (n_gt_Uno_to_O_lt_pred_n n).
636 | apply divides_gcd_m
644 | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
645 [ apply (lt_to_divides_to_div_le)
648 apply (n_gt_Uno_to_O_lt_pred_n n).
650 | apply divides_gcd_m
652 | apply (lt_to_le_to_lt j (pred n) n)
659 apply (sum_divisor_totient1_aux_6);
662 | apply (sigma_p_true).
668 (*there's a little difference between the following definition of the
669 theorem, and the abstract definition given before.
670 in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
671 that's why in the definition of the theorem the summary is set equal to
674 theorem sum_divisor_totient: \forall n.
675 sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
689 rewrite > (pred_Sn m).
691 apply( sum_divisor_totient1).
694 apply cic:/matita/algebra/finite_groups/lt_S_S.con.