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.
101 theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat.
102 i < n*n \to (divides_b (i/n) (pred n) \land
103 (leb (S(i\mod n)) (i/n) \land
104 eqb (gcd (i\mod n) (i/n)) (S O))) =true
106 (S (i\mod n)) \le (i/n).
108 cut (leb (S (i \mod n)) (i/n) = true)
111 [ true \Rightarrow (S (i \mod n)) \leq (i/n)
112 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
115 apply (leb_to_Prop (S(i \mod n)) (i/n))
116 | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
117 apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
118 (eqb (gcd (i\mod n) (i/n)) (S O))
120 rewrite > andb_sym in \vdash (? ? (? % ?) ?).
121 rewrite < (andb_assoc) in \vdash (? ? % ?).
127 (*the following theorem is just a particular case of the theorem
128 divides_times, prooved in primes.ma
130 theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat.
131 a \divides b \to a \divides (b*c).
133 rewrite > (times_n_SO a).
134 apply (divides_times).
139 theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
141 (divides_b (i/n) (pred n)
142 \land (leb (S(i\mod n)) (i/n)
143 \land eqb (gcd (i\mod n) (i/n)) (S O)))
145 \to i\mod n*pred n/(i/n)<(pred n).
147 apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
148 ((i/n)*(pred n) / (i/n))
150 [ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/n)))
151 [ apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
152 apply (aux_S_i_mod_n_le_i_div_n i n);
154 | rewrite > (NdivM_times_M_to_N )
155 [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
156 [ apply (monotonic_lt_times_variant (pred n))
157 [ apply (nat_case1 n)
159 rewrite > H2 in H:(? ? %).
160 change in H:(? ? %) with (O).
161 change in H:(%) with ((S i) \le O).
163 apply (not_le_Sn_O i H)
166 [ rewrite > H2 in H1:(%).
167 rewrite > H2 in H:(%).
170 [ rewrite > Hcut in H1:(%).
173 apply (not_eq_true_false H1)
174 | change in H:(%) with((S i) \le (S O)).
176 [ apply (nat_case1 i)
180 rewrite > H3 in Hcut:(%).
182 apply (not_le_Sn_O m1 Hcut)
184 | apply (le_S_S_to_le i O).
188 | change with ((S O) \le (S n1)).
193 | change with ((S (i\mod n)) \le (i/n)).
194 apply (aux_S_i_mod_n_le_i_div_n i n);
197 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
198 apply (aux_S_i_mod_n_le_i_div_n i n);
200 | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
201 apply (divides_times).
205 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
206 apply (aux_S_i_mod_n_le_i_div_n i n);
208 | rewrite > (times_n_SO (i/n)).
209 rewrite > (sym_times (i \mod n) (pred n)).
210 apply (divides_times)
211 [ apply divides_b_true_to_divides.
212 apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))).
213 apply (andb_true_true
214 ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)))
215 (eqb (gcd (i\mod n) (i/n)) (S O))).
216 rewrite < (andb_assoc) in \vdash (? ? % ?).
222 | rewrite > (sym_times).
223 rewrite > (div_times_ltO )
224 [ apply (le_n (pred n)).
226 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
227 apply (aux_S_i_mod_n_le_i_div_n i n);
234 theorem sum_divisor_totient1_aux_4: \forall j,n:nat.
235 j \lt (pred n) \to (S O) \lt n \to
236 ((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n))
237 \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n))
238 ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n))
240 (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)
241 ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O))))
245 [ cut ( O \lt (gcd (pred n) j))
246 [ cut (j/(gcd (pred n) j) \lt n)
247 [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j)
248 [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j)
252 [ apply divides_to_divides_b_true
253 [ apply (lt_times_n_to_lt (gcd (pred n) j) O (pred n/gcd (pred n) j))
255 | rewrite > (sym_times O (gcd (pred n) j)).
256 rewrite < (times_n_O (gcd (pred n) j)).
257 rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
260 | apply (divides_gcd_n (pred n))
263 | apply (witness (pred n/(gcd (pred n) j)) (pred n) (gcd (pred n) j)).
264 rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
267 | apply (divides_gcd_n (pred n))
270 | apply (le_to_leb_true).
272 apply cic:/matita/algebra/finite_groups/lt_S_S.con.
273 apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
275 | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
276 [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
279 | apply divides_gcd_n
286 | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
287 apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j))
289 | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
292 rewrite > NdivM_times_M_to_N
295 | apply divides_gcd_n
298 | rewrite > NdivM_times_M_to_N
299 [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
306 | apply divides_gcd_n
310 | apply (mod_plus_times).
313 | apply (div_plus_times).
316 | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
318 | rewrite > NdivM_times_M_to_N
319 [ apply (lt_to_le_to_lt j (pred n) ?)
322 apply (lt_to_le_to_lt ? n ?)
323 [ change with ((S (pred n)) \le n).
326 | apply (trans_lt ? (S O) ?)
327 [ change with ((S O) \le (S O)).
332 | rewrite > (times_n_SO n) in \vdash (? % ?).
335 | change with (O \lt (gcd (pred n) j)).
342 apply (divides_gcd_n)
350 | apply n_gt_Uno_to_O_lt_pred_n.
359 theorem sum_divisor_totient1_aux5: \forall a,b,c:nat.
360 O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to
361 a / b * c / (c/b) = a.
366 [ rewrite > H6 in \vdash (? ? (? ? %) ?).
367 rewrite > sym_times in \vdash (? ? (? ? %) ?).
368 rewrite > (div_times_ltO n b)
370 [ cut (a/b * c /n = a/b * (c/n))
374 apply (NdivM_times_M_to_N a b);
377 apply (div_times_ltO b n).
382 rewrite < assoc_times in \vdash (? ? (? % ?) ?).
383 rewrite > (sym_times ((a/b)*n) n1).
384 rewrite < (assoc_times n1 (a/b) n).
385 rewrite > (div_times_ltO (n1*(a/b)) n)
386 [ rewrite > (sym_times n n1).
387 rewrite > (div_times_ltO n1 n)
388 [ rewrite > (sym_times (a/b) n1).
395 | apply (witness n c b).
396 rewrite > (sym_times n b).
401 | apply (nat_case1 n)
404 rewrite > sym_times in H6.
408 change in H with ((S O) \le O).
409 apply (not_le_Sn_O O H)
420 theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
421 j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
427 apply (not_le_Sn_O j H)
429 rewrite < (pred_Sn m).
430 rewrite < (times_n_Sm (S m) m).
431 rewrite > (sym_plus (S m) ((S m) * m)).
432 apply le_to_lt_to_plus_lt
433 [ rewrite > (sym_times (S m) m).
435 apply (lt_to_divides_to_div_le)
436 [ apply (nat_case1 m)
441 apply (le_to_not_lt (S O) (S O))
446 rewrite > sym_gcd in \vdash (? ? %).
447 apply (lt_O_gcd j (S m1)).
450 | apply divides_gcd_n
452 | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
454 apply lt_to_divides_to_div_le
455 [ apply (nat_case1 m)
460 apply (le_to_not_lt (S O) (S O))
465 rewrite > sym_gcd in \vdash (? ? %).
466 apply (lt_O_gcd j (S m1)).
469 | rewrite > sym_gcd in \vdash (? % ?).
473 rewrite < (pred_Sn m) in H.
474 apply (trans_lt j m (S m))
476 | change with ((S m) \le (S m)).
487 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
488 and n = 1 are dealed as particular cases in theorem
491 theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
495 (sigma_p n (\lambda d:nat.divides_b d (pred n))
496 (\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))))
503 (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
504 [ apply false_to_eq_sigma_p
508 rewrite > lt_to_leb_false
516 rewrite > le_to_leb_true
525 | rewrite < (sigma_p2' n n
526 (\lambda d:nat.divides_b d (pred n))
527 (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
528 (\lambda x,y.(S O))).
529 apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
530 [ apply (eq_sigma_p_gh
531 (\lambda x:nat. (S O))
532 (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) )
533 (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
537 divides_b (x/n) (pred n)
538 \land (leb (S (x \mod n)) (x/n)
539 \land eqb (gcd (x \mod n) (x/n)) (S O)))
545 cut ((i/n) \divides (pred n))
546 [ cut ((i \mod n ) \lt (i/n))
547 [ cut ((gcd (i \mod n) (i / n)) = (S O))
548 [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
550 cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
552 cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
556 apply (trans_lt O (S O) n)
561 rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
562 rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
563 rewrite > (div_times_ltO n2 (i/n))
566 apply (divides_to_lt_O n2 (pred n))
567 [ apply (n_gt_Uno_to_O_lt_pred_n n).
569 | apply (witness n2 (pred n) (i/n)).
573 | apply (divides_to_lt_O (i/n) (pred n))
574 [ apply (n_gt_Uno_to_O_lt_pred_n n).
576 | apply (witness (i/n) (pred n) n2).
582 cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
585 rewrite < (sym_times n2 (i/n)).
586 rewrite > (div_times_ltO n2 (i/n))
587 [ rewrite > (div_times_ltO (i \mod n) n2)
589 | apply (divides_to_lt_O n2 (pred n))
590 [ apply (n_gt_Uno_to_O_lt_pred_n n).
592 | apply (witness n2 (pred n) (i/n)).
597 | apply (divides_to_lt_O (i/n) (pred n))
598 [ apply (n_gt_Uno_to_O_lt_pred_n n).
604 apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
605 [ apply (n_gt_Uno_to_O_lt_pred_n n).
611 | apply (sum_divisor_totient1_aux2);
614 | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
615 apply (andb_true_true
616 (eqb (gcd (i\mod n) (i/n)) (S O))
617 (leb (S (i\mod n)) (i/n))
619 apply (andb_true_true
620 ((eqb (gcd (i\mod n) (i/n)) (S O))
622 (leb (S (i\mod n)) (i/n)))
623 (divides_b (i/n) (pred n))
626 rewrite > andb_sym in \vdash (? ? (? ? %) ?).
629 | change with (S (i \mod n) \le (i/n)).
630 cut (leb (S (i \mod n)) (i/n) = true)
633 [ true \Rightarrow (S (i \mod n)) \leq (i/n)
634 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
637 apply (leb_to_Prop (S(i \mod n)) (i/n))
638 | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
639 apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
640 (eqb (gcd (i\mod n) (i/n)) (S O))
642 rewrite > andb_sym in \vdash (? ? (? % ?) ?).
643 rewrite < (andb_assoc) in \vdash (? ? % ?).
647 | apply (divides_b_true_to_divides ).
648 apply (andb_true_true (divides_b (i/n) (pred n))
649 (leb (S (i\mod n)) (i/n))).
650 apply (andb_true_true ( (divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)) )
651 (eqb (gcd (i\mod n) (i/n)) (S O))
653 rewrite < andb_assoc.
657 apply (sum_divisor_totient1_aux_3);
660 apply (sum_divisor_totient1_aux_4);
663 cut (j/(gcd (pred n) j) \lt n)
664 [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
665 [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
666 [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
667 [ apply (n_gt_Uno_to_O_lt_pred_n n).
671 apply (n_gt_Uno_to_O_lt_pred_n n).
674 | apply divides_gcd_m
682 | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
683 [ apply (lt_to_divides_to_div_le)
686 apply (n_gt_Uno_to_O_lt_pred_n n).
688 | apply divides_gcd_m
690 | apply (lt_to_le_to_lt j (pred n) n)
697 apply (sum_divisor_totient1_aux_6);
700 | apply (sigma_p_true).
706 (*there's a little difference between the following definition of the
707 theorem, and the abstract definition given before.
708 in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
709 that's why in the definition of the theorem the summary is set equal to
712 theorem sum_divisor_totient: \forall n.
713 sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
727 rewrite > (pred_Sn m).
729 apply( sum_divisor_totient1).
732 apply cic:/matita/algebra/finite_groups/lt_S_S.con.