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.
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 (nat_case1 n)
158 rewrite > H2 in H:(? ? %).
159 change in H:(? ? %) with (O).
160 change in H:(%) with ((S i) \le O).
162 apply (not_le_Sn_O i H)
165 [ rewrite > H2 in H1:(%).
166 rewrite > H2 in H:(%).
169 [ rewrite > Hcut in H1:(%).
172 apply (not_eq_true_false H1)
173 | change in H:(%) with((S i) \le (S O)).
175 [ apply (nat_case1 i)
179 rewrite > H3 in Hcut:(%).
181 apply (not_le_Sn_O m1 Hcut)
183 | apply (le_S_S_to_le i O).
187 | change with ((S O) \le (S n1)).
192 | change with ((S (i\mod n)) \le (i/n)).
193 apply (aux_S_i_mod_n_le_i_div_n i n);
196 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
197 apply (aux_S_i_mod_n_le_i_div_n i n);
199 | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
200 apply (divides_times).
204 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
205 apply (aux_S_i_mod_n_le_i_div_n i n);
207 | rewrite > (times_n_SO (i/n)).
208 rewrite > (sym_times (i \mod n) (pred n)).
209 apply (divides_times)
210 [ apply divides_b_true_to_divides.
211 apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))).
212 apply (andb_true_true
213 ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)))
214 (eqb (gcd (i\mod n) (i/n)) (S O))).
215 rewrite < (andb_assoc) in \vdash (? ? % ?).
221 | rewrite > (sym_times).
222 rewrite > (div_times_ltO )
223 [ apply (le_n (pred n)).
225 | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
226 apply (aux_S_i_mod_n_le_i_div_n i n);
233 theorem sum_divisor_totient1_aux_4: \forall j,n:nat.
234 j \lt (pred n) \to (S O) \lt n \to
235 ((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n))
236 \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n))
237 ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n))
239 (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)
240 ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O))))
244 [ cut ( O \lt (gcd (pred n) j))
245 [ cut (j/(gcd (pred n) j) \lt n)
246 [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j)
247 [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j)
251 [ apply divides_to_divides_b_true
252 [ apply (lt_times_n_to_lt (gcd (pred n) j) O (pred n/gcd (pred n) j))
254 | rewrite > (sym_times O (gcd (pred n) j)).
255 rewrite < (times_n_O (gcd (pred n) j)).
256 rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
259 | apply (divides_gcd_n (pred n))
262 | apply (witness (pred n/(gcd (pred n) j)) (pred n) (gcd (pred n) j)).
263 rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
266 | apply (divides_gcd_n (pred n))
269 | apply (le_to_leb_true).
271 apply cic:/matita/algebra/finite_groups/lt_S_S.con.
272 apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
274 | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
275 [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
278 | apply divides_gcd_n
285 | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
286 apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j))
288 | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
291 rewrite > NdivM_times_M_to_N
294 | apply divides_gcd_n
297 | rewrite > NdivM_times_M_to_N
298 [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
305 | apply divides_gcd_n
309 | apply (mod_plus_times).
312 | apply (div_plus_times).
315 | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
317 | rewrite > NdivM_times_M_to_N
318 [ apply (lt_to_le_to_lt j (pred n) ?)
321 apply (lt_to_le_to_lt ? n ?)
322 [ change with ((S (pred n)) \le n).
325 | apply (trans_lt ? (S O) ?)
326 [ change with ((S O) \le (S O)).
331 | rewrite > (times_n_SO n) in \vdash (? % ?).
334 | change with (O \lt (gcd (pred n) j)).
341 apply (divides_gcd_n)
349 | apply n_gt_Uno_to_O_lt_pred_n.
358 theorem sum_divisor_totient1_aux5: \forall a,b,c:nat.
359 O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to
360 a / b * c / (c/b) = a.
365 [ rewrite > H6 in \vdash (? ? (? ? %) ?).
366 rewrite > sym_times in \vdash (? ? (? ? %) ?).
367 rewrite > (div_times_ltO n b)
369 [ cut (a/b * c /n = a/b * (c/n))
373 apply (NdivM_times_M_to_N a b);
376 apply (div_times_ltO b n).
381 rewrite < assoc_times in \vdash (? ? (? % ?) ?).
382 rewrite > (sym_times ((a/b)*n) n1).
383 rewrite < (assoc_times n1 (a/b) n).
384 rewrite > (div_times_ltO (n1*(a/b)) n)
385 [ rewrite > (sym_times n n1).
386 rewrite > (div_times_ltO n1 n)
387 [ rewrite > (sym_times (a/b) n1).
394 | apply (witness n c b).
395 rewrite > (sym_times n b).
400 | apply (nat_case1 n)
403 rewrite > sym_times in H6.
407 change in H with ((S O) \le O).
408 apply (not_le_Sn_O O H)
417 theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
418 j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
424 apply (not_le_Sn_O j H)
426 rewrite < (pred_Sn m).
427 rewrite < (times_n_Sm (S m) m).
428 rewrite > (sym_plus (S m) ((S m) * m)).
429 apply le_to_lt_to_plus_lt
430 [ rewrite > (sym_times (S m) m).
432 apply (lt_to_divides_to_div_le)
433 [ apply (nat_case1 m)
438 apply (le_to_not_lt (S O) (S O))
443 rewrite > sym_gcd in \vdash (? ? %).
444 apply (lt_O_gcd j (S m1)).
447 | apply divides_gcd_n
449 | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
451 apply lt_to_divides_to_div_le
452 [ apply (nat_case1 m)
457 apply (le_to_not_lt (S O) (S O))
462 rewrite > sym_gcd in \vdash (? ? %).
463 apply (lt_O_gcd j (S m1)).
466 | rewrite > sym_gcd in \vdash (? % ?).
470 rewrite < (pred_Sn m) in H.
471 apply (trans_lt j m (S m))
473 | change with ((S m) \le (S m)).
484 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
485 and n = 1 are dealed as particular cases in theorem
488 theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
492 (sigma_p n (\lambda d:nat.divides_b d (pred n))
493 (\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))))
500 (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
501 [ apply false_to_eq_sigma_p
505 rewrite > lt_to_leb_false
513 rewrite > le_to_leb_true
522 | rewrite < (sigma_p2' n n
523 (\lambda d:nat.divides_b d (pred n))
524 (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
525 (\lambda x,y.(S O))).
526 apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
527 [ apply (eq_sigma_p_gh
528 (\lambda x:nat. (S O))
529 (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) )
530 (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
534 divides_b (x/n) (pred n)
535 \land (leb (S (x \mod n)) (x/n)
536 \land eqb (gcd (x \mod n) (x/n)) (S O)))
542 cut ((i/n) \divides (pred n))
543 [ cut ((i \mod n ) \lt (i/n))
544 [ cut ((gcd (i \mod n) (i / n)) = (S O))
545 [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
547 cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
549 cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
553 apply (trans_lt O (S O) n)
558 rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
559 rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
560 rewrite > (div_times_ltO n2 (i/n))
563 apply (divides_to_lt_O n2 (pred n))
564 [ apply (n_gt_Uno_to_O_lt_pred_n n).
566 | apply (witness n2 (pred n) (i/n)).
570 | apply (divides_to_lt_O (i/n) (pred n))
571 [ apply (n_gt_Uno_to_O_lt_pred_n n).
573 | apply (witness (i/n) (pred n) n2).
579 cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
582 rewrite < (sym_times n2 (i/n)).
583 rewrite > (div_times_ltO n2 (i/n))
584 [ rewrite > (div_times_ltO (i \mod n) n2)
586 | apply (divides_to_lt_O n2 (pred n))
587 [ apply (n_gt_Uno_to_O_lt_pred_n n).
589 | apply (witness n2 (pred n) (i/n)).
594 | apply (divides_to_lt_O (i/n) (pred n))
595 [ apply (n_gt_Uno_to_O_lt_pred_n n).
601 apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
602 [ apply (n_gt_Uno_to_O_lt_pred_n n).
608 | apply (sum_divisor_totient1_aux2);
611 | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
612 apply (andb_true_true
613 (eqb (gcd (i\mod n) (i/n)) (S O))
614 (leb (S (i\mod n)) (i/n))
616 apply (andb_true_true
617 ((eqb (gcd (i\mod n) (i/n)) (S O))
619 (leb (S (i\mod n)) (i/n)))
620 (divides_b (i/n) (pred n))
623 rewrite > andb_sym in \vdash (? ? (? ? %) ?).
626 | change with (S (i \mod n) \le (i/n)).
627 cut (leb (S (i \mod n)) (i/n) = true)
630 [ true \Rightarrow (S (i \mod n)) \leq (i/n)
631 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
634 apply (leb_to_Prop (S(i \mod n)) (i/n))
635 | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
636 apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
637 (eqb (gcd (i\mod n) (i/n)) (S O))
639 rewrite > andb_sym in \vdash (? ? (? % ?) ?).
640 rewrite < (andb_assoc) in \vdash (? ? % ?).
644 | apply (divides_b_true_to_divides ).
645 apply (andb_true_true (divides_b (i/n) (pred n))
646 (leb (S (i\mod n)) (i/n))).
647 apply (andb_true_true ( (divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)) )
648 (eqb (gcd (i\mod n) (i/n)) (S O))
650 rewrite < andb_assoc.
654 apply (sum_divisor_totient1_aux_3);
657 apply (sum_divisor_totient1_aux_4);
660 cut (j/(gcd (pred n) j) \lt n)
661 [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
662 [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
663 [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
664 [ apply (n_gt_Uno_to_O_lt_pred_n n).
668 apply (n_gt_Uno_to_O_lt_pred_n n).
671 | apply divides_gcd_m
679 | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
680 [ apply (lt_to_divides_to_div_le)
683 apply (n_gt_Uno_to_O_lt_pred_n n).
685 | apply divides_gcd_m
687 | apply (lt_to_le_to_lt j (pred n) n)
694 apply (sum_divisor_totient1_aux_6);
697 | apply (sigma_p_true).
703 (*there's a little difference between the following definition of the
704 theorem, and the abstract definition given before.
705 in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
706 that's why in the definition of the theorem the summary is set equal to
709 theorem sum_divisor_totient: \forall n.
710 sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
724 rewrite > (pred_Sn m).
726 apply( sum_divisor_totient1).
729 apply cic:/matita/algebra/finite_groups/lt_S_S.con.