helm/software/matita/library/nat/totient1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/totient1".
  16
  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".
  21
  22 (* This file contains the proof of the following theorem about Euler's totient
  23  * function:
  24
  25    The sum of the applications of Phi function over the divisor of a natural
  26    number n is equal to n
  27  *)
  28
  29 (*two easy properties of gcd, directly obtainable from the more general theorem
  30   eq_gcd_times_times_eqv_times_gcd*)
  31
  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).
  34 intros.
  35 apply (inj_times_r1 d)
  36 [ assumption
  37 | rewrite < (times_n_SO d).
  38   rewrite < (eq_gcd_times_times_eqv_times_gcd a b d).
  39   rewrite > sym_gcd.
  40   rewrite > (sym_times d a).
  41   rewrite > (sym_times d b).
  42   assumption
  43 ]
  44 qed.
  45
  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.
  48 intros.
  49 rewrite > (sym_times a c).
  50 rewrite > (sym_times b c).
  51 rewrite > (eq_gcd_times_times_eqv_times_gcd a b c).
  52 rewrite > H1.
  53 apply sym_eq.
  54 apply times_n_SO.
  55 qed.
  56
  57
  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
  60  *)
  61
  62
  63
  64 (* 2nd*)
  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).
  71 intros.
  72 cut (O \lt (pred n))
  73 [ cut(O \lt (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)))
  77       [ rewrite > Hcut2.
  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));
  80             assumption
  81         | rewrite > sym_gcd.
  82           assumption
  83         ]
  84       | apply sym_eq.
  85         apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n));
  86           assumption.
  87       ]
  88     | assumption
  89     | assumption
  90     ]
  91   | apply (divides_to_lt_O (i/n) (pred n));
  92       assumption
  93   ]
  94 | apply n_gt_Uno_to_O_lt_pred_n.
  95   assumption.
  96 ]
  97 qed.
  98
  99 (*3rd*)
 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
 104          \to
 105          (S (i\mod n)) \le (i/n).
 106 intros.
 107 cut (leb (S (i \mod n)) (i/n) = true)
 108 [ change with (
 109   match (true) with
 110   [ true  \Rightarrow (S (i \mod n)) \leq (i/n)
 111   | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
 112   ).
 113   rewrite < Hcut.
 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))
 118   ).
 119   rewrite > andb_sym in \vdash (? ? (? % ?) ?).
 120   rewrite < (andb_assoc) in \vdash (? ? % ?).
 121   assumption
 122 ]
 123 qed.
 124
 125
 126 (*the following theorem is just a particular case of the theorem
 127   divides_times, prooved in primes.ma
 128  *)
 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).
 131 intros.
 132 rewrite > (times_n_SO a).
 133 apply (divides_times).
 134 assumption.
 135 apply divides_SO_n.
 136 qed.
 137
 138 theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
 139 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)))
 143        =true
 144    \to i\mod n*pred n/(i/n)<(pred n).
 145 intros.
 146 apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
 147                 ((i/n)*(pred n) / (i/n))
 148                  (pred 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);
 152       assumption.
 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)
 157           [ intros.
 158             rewrite > H2 in H:(? ? %).
 159             change in H:(? ? %) with (O).
 160             change in H:(%) with ((S i) \le O).
 161             apply False_ind.
 162             apply (not_le_Sn_O i H)
 163           | intro.
 164             elim m
 165             [ rewrite > H2 in H1:(%).
 166               rewrite > H2 in H:(%).
 167               simplify in H.
 168               cut (i = O)
 169               [ rewrite > Hcut in H1:(%).
 170                 simplify in H1.
 171                 apply False_ind.
 172                 apply (not_eq_true_false H1)
 173               | change in H:(%) with((S i) \le (S O)).
 174                 cut (i \le O )
 175                 [ apply (nat_case1 i)
 176                   [ intros.
 177                     reflexivity
 178                   | intros.
 179                     rewrite > H3 in Hcut:(%).
 180                     apply False_ind.
 181                     apply (not_le_Sn_O m1 Hcut)
 182                   ]
 183                 | apply (le_S_S_to_le i O).
 184                   assumption
 185                 ]
 186               ]
 187             | change with ((S O) \le (S n1)).
 188               apply (le_S_S O n1).
 189               apply (le_O_n n1)
 190             ]
 191           ]
 192         | change with ((S (i\mod n)) \le (i/n)).
 193           apply (aux_S_i_mod_n_le_i_div_n i n);
 194             assumption
 195         ]
 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);
 198           assumption
 199       | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
 200         apply (divides_times).
 201         apply divides_n_n.
 202         apply divides_SO_n
 203       ]
 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);
 206         assumption
 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 (? ? % ?).
 216         assumption
 217       | apply divides_SO_n
 218       ]
 219     ]
 220   ]
 221 | rewrite > (sym_times).
 222   rewrite > (div_times_ltO )
 223   [ apply (le_n (pred n)).
 224
 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);
 227       assumption.
 228   ]
 229 ]qed.
 230
 231
 232 (*4th*)
 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))
 238         \land (eqb
 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))))
 241 =true.
 242 intros.
 243 cut (O \lt (pred n))
 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)
 248         [ rewrite > Hcut3.
 249           rewrite > Hcut4.
 250           apply andb_t_t_t
 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))
 253               [ assumption
 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))
 257                 [ assumption
 258                 | assumption
 259                 | apply (divides_gcd_n (pred n))
 260                 ]
 261               ]
 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))
 264               [ reflexivity
 265               | assumption
 266               | apply (divides_gcd_n (pred n))
 267               ]
 268             ]
 269           | apply (le_to_leb_true).
 270             apply lt_S_to_le.
 271             apply cic:/matita/algebra/finite_groups/lt_S_S.con.
 272             apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
 273             [ assumption
 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))
 276                 [ assumption
 277                 | assumption
 278                 | apply divides_gcd_n
 279                 ]
 280               | assumption
 281               | rewrite > sym_gcd.
 282                 apply divides_gcd_n
 283               ]
 284             ]
 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))
 287             [ assumption
 288             | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
 289               [ assumption
 290               | simplify.
 291                 rewrite > NdivM_times_M_to_N
 292                 [ assumption
 293                 | assumption
 294                 | apply divides_gcd_n
 295                 ]
 296               ]
 297             | rewrite > NdivM_times_M_to_N
 298               [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
 299                 [ reflexivity
 300                 | assumption
 301                 | rewrite > sym_gcd.
 302                   apply divides_gcd_n
 303                 ]
 304               | assumption
 305               | apply divides_gcd_n
 306               ]
 307             ]
 308           ]
 309         | apply (mod_plus_times).
 310           assumption
 311         ]
 312       | apply (div_plus_times).
 313         assumption
 314       ]
 315     | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
 316       [ assumption
 317       | rewrite > NdivM_times_M_to_N
 318         [ apply (lt_to_le_to_lt j (pred n) ?)
 319           [ assumption
 320           | apply (lt_to_le).
 321             apply (lt_to_le_to_lt ? n ?)
 322             [ change with ((S (pred n)) \le n).
 323               rewrite < (S_pred n)
 324               [ apply le_n
 325               | apply (trans_lt ? (S O)  ?)
 326                 [ change with ((S O) \le (S O)).
 327                   apply (le_n (S O))
 328                 | assumption
 329                 ]
 330               ]
 331             | rewrite > (times_n_SO n) in \vdash (? % ?).
 332               apply (le_times n)
 333               [ apply (le_n n)
 334               | change with (O \lt (gcd (pred n) j)).
 335                 assumption
 336               ]
 337             ]
 338           ]
 339         | assumption
 340         | rewrite > sym_gcd.
 341           apply (divides_gcd_n)
 342         ]
 343       ]
 344     ]
 345   | rewrite > sym_gcd.
 346     apply (lt_O_gcd).
 347     assumption
 348   ]
 349 | apply n_gt_Uno_to_O_lt_pred_n.
 350   assumption
 351 ]
 352 qed.
 353
 354
 355
 356
 357 (*5th*)
 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.
 361 intros.
 362 elim H3.
 363 elim H4.
 364 cut (O \lt n)
 365 [ rewrite > H6 in \vdash (? ? (? ? %) ?).
 366   rewrite > sym_times in \vdash (? ? (? ? %) ?).
 367   rewrite > (div_times_ltO n b)
 368   [ cut (n \divides c)
 369     [ cut (a/b * c /n = a/b * (c/n))
 370       [ rewrite > Hcut2.
 371         cut (c/n = b)
 372         [ rewrite > Hcut3.
 373           apply (NdivM_times_M_to_N a b);
 374             assumption
 375         | rewrite > H6.
 376           apply (div_times_ltO b n).
 377           assumption
 378         ]
 379       | elim Hcut1.
 380         rewrite > H7.
 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).
 388             reflexivity
 389           | assumption
 390           ]
 391         | assumption
 392         ]
 393       ]
 394     | apply (witness n c b).
 395       rewrite > (sym_times n b).
 396       assumption
 397     ]
 398   | assumption
 399   ]
 400 | apply (nat_case1 n)
 401   [ intros.
 402     rewrite > H7 in H6.
 403     rewrite > sym_times in H6.
 404     simplify in H6.
 405     rewrite > H6 in H.
 406     apply False_ind.
 407     change in H with ((S O) \le O).
 408     apply (not_le_Sn_O O H)
 409   | intros.
 410     apply (lt_O_S m)
 411   ]
 412 ]
 413 qed.
 414
 415
 416 (*6th*)
 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.
 419 intros.
 420 apply (nat_case1 n)
 421 [ intros.
 422   rewrite > H2 in H.
 423   apply False_ind.
 424   apply (not_le_Sn_O j H)
 425 | intros.
 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).
 431     apply le_times_l.
 432     apply (lt_to_divides_to_div_le)
 433     [ apply (nat_case1 m)
 434       [ intros.
 435         rewrite > H3 in H2.
 436         rewrite > H2 in H1.
 437         apply False_ind.
 438         apply (le_to_not_lt (S O) (S O))
 439         [ apply le_n
 440         | assumption
 441         ]
 442       | intros.
 443         rewrite > sym_gcd in \vdash (? ? %).
 444         apply (lt_O_gcd j (S m1)).
 445         apply (lt_O_S m1)
 446       ]
 447     | apply divides_gcd_n
 448     ]
 449   | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
 450     [
 451       apply lt_to_divides_to_div_le
 452       [ apply (nat_case1 m)
 453         [ intros.
 454           rewrite > H3 in H2.
 455           rewrite > H2 in H1.
 456           apply False_ind.
 457           apply (le_to_not_lt (S O) (S O))
 458           [ apply le_n
 459           | assumption
 460           ]
 461         | intros.
 462           rewrite > sym_gcd in \vdash (? ? %).
 463           apply (lt_O_gcd j (S m1)).
 464           apply (lt_O_S m1)
 465         ]
 466       | rewrite > sym_gcd in \vdash (? % ?).
 467         apply divides_gcd_n
 468       ]
 469     | rewrite > H2 in H.
 470       rewrite < (pred_Sn m) in H.
 471       apply (trans_lt j m (S m))
 472       [ assumption.
 473       | change with ((S m) \le (S m)).
 474         apply (le_n (S m))
 475       ]
 476     ]
 477   ]
 478 ]
 479 qed.
 480
 481
 482
 483
 484 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
 485    and n = 1 are dealed as particular cases in theorem
 486    sum_divisor_totiet)
 487  *)
 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).
 489 intros.
 490 unfold totient.
 491 apply (trans_eq ? ?
 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))))
 494   [ apply eq_sigma_p1
 495     [ intros.
 496       reflexivity
 497     | intros.
 498       apply sym_eq.
 499       apply (trans_eq ? ?
 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
 502         [ apply lt_to_le.
 503           assumption
 504         | intros.
 505           rewrite > lt_to_leb_false
 506           [ reflexivity
 507           | apply le_S_S.
 508             assumption
 509           ]
 510         ]
 511       | apply eq_sigma_p
 512         [ intros.
 513           rewrite > le_to_leb_true
 514           [ reflexivity
 515           | assumption
 516           ]
 517         | intros.
 518           reflexivity
 519         ]
 520       ]
 521     ]
 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))) )
 531       (n*n)
 532       (pred n)
 533       (\lambda x:nat.
 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)))
 537       (\lambda x:nat.true)
 538       )
 539       [ intros.
 540         reflexivity
 541       | intros.
 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)))
 546               [ rewrite > Hcut3.
 547                 cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
 548                 [ rewrite > Hcut4.
 549                   cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
 550                   [ rewrite > Hcut5.
 551                     apply sym_eq.
 552                     apply div_mod.
 553                     apply (trans_lt O (S O) n)
 554                     [ apply (lt_O_S O)
 555                     | assumption
 556                     ]
 557                   | elim Hcut.
 558                     rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
 559                     rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
 560                     rewrite > (div_times_ltO n2 (i/n))
 561                     [ rewrite > H3.
 562                       apply div_times_ltO.
 563                       apply (divides_to_lt_O n2 (pred n))
 564                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 565                         assumption
 566                       | apply (witness n2 (pred n) (i/n)).
 567                         rewrite > sym_times.
 568                         assumption
 569                       ]
 570                     | apply (divides_to_lt_O (i/n) (pred n))
 571                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 572                         assumption
 573                       | apply (witness (i/n) (pred n) n2).
 574                         assumption
 575                       ]
 576                     ]
 577                   ]
 578                 | elim Hcut.
 579                   cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
 580                   [ rewrite > Hcut4.
 581                     rewrite > H3.
 582                     rewrite < (sym_times n2 (i/n)).
 583                     rewrite > (div_times_ltO n2 (i/n))
 584                     [ rewrite > (div_times_ltO (i \mod n) n2)
 585                       [ reflexivity
 586                       | apply (divides_to_lt_O n2 (pred n))
 587                         [ apply (n_gt_Uno_to_O_lt_pred_n n).
 588                           assumption
 589                         | apply (witness n2 (pred n) (i/n)).
 590                           rewrite > sym_times.
 591                           assumption
 592                         ]
 593                       ]
 594                     | apply (divides_to_lt_O (i/n) (pred n))
 595                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 596                         assumption
 597                       | assumption
 598                       ]
 599                     ]
 600                   | apply (sym_eq).
 601                     apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
 602                     [ apply (n_gt_Uno_to_O_lt_pred_n n).
 603                       assumption
 604                     | assumption
 605                     ]
 606                   ]
 607                 ]
 608               | apply (sum_divisor_totient1_aux2);
 609                 assumption
 610               ]
 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))
 615               ).
 616               apply (andb_true_true
 617                ((eqb (gcd (i\mod n) (i/n)) (S O))
 618                 \land
 619                 (leb (S (i\mod n)) (i/n)))
 620                      (divides_b (i/n) (pred n))
 621               ).
 622               rewrite > andb_sym.
 623               rewrite > andb_sym in \vdash (? ? (? ? %) ?).
 624               assumption
 625             ]
 626           | change with (S (i \mod n) \le (i/n)).
 627             cut (leb (S (i \mod n)) (i/n) = true)
 628             [ change with (
 629                 match (true) with
 630                 [ true  \Rightarrow (S (i \mod n)) \leq (i/n)
 631                 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
 632               ).
 633               rewrite < Hcut1.
 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))
 638               ).
 639               rewrite > andb_sym in \vdash (? ? (? % ?) ?).
 640               rewrite < (andb_assoc) in \vdash (? ? % ?).
 641               assumption
 642             ]
 643           ]
 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))
 649           ).
 650           rewrite < andb_assoc.
 651           assumption.
 652         ]
 653       | intros.
 654         apply (sum_divisor_totient1_aux_3);
 655           assumption.
 656       | intros.
 657         apply (sum_divisor_totient1_aux_4);
 658           assumption.
 659       | intros.
 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).
 665                 assumption
 666               | rewrite > sym_gcd.
 667                 apply lt_O_gcd.
 668                 apply (n_gt_Uno_to_O_lt_pred_n n).
 669                 assumption
 670               | assumption
 671               | apply divides_gcd_m
 672               | rewrite > sym_gcd.
 673                 apply divides_gcd_m
 674               ]
 675             | assumption
 676             ]
 677           | assumption
 678           ]
 679         | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
 680           [ apply (lt_to_divides_to_div_le)
 681             [ rewrite > sym_gcd.
 682               apply lt_O_gcd.
 683               apply (n_gt_Uno_to_O_lt_pred_n n).
 684               assumption
 685             | apply divides_gcd_m
 686             ]
 687           | apply (lt_to_le_to_lt j (pred n) n)
 688             [ assumption
 689             | apply le_pred_n
 690             ]
 691           ]
 692         ]
 693       | intros.
 694         apply (sum_divisor_totient1_aux_6);
 695           assumption.
 696       ]
 697     | apply (sigma_p_true).
 698     ]
 699   ]
 700 qed.
 701
 702
 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
 707   (pred n).
 708  *)
 709 theorem sum_divisor_totient: \forall n.
 710 sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
 711 intros.
 712 apply (nat_case1 n)
 713 [ intros.
 714   simplify.
 715   reflexivity
 716 | intros.
 717   apply (nat_case1 m)
 718   [ intros.
 719     simplify.
 720     reflexivity
 721   | intros.
 722     rewrite < H1.
 723     rewrite < H.
 724     rewrite > (pred_Sn m).
 725     rewrite < H.
 726     apply( sum_divisor_totient1).
 727     rewrite > H.
 728     rewrite > H1.
 729     apply cic:/matita/algebra/finite_groups/lt_S_S.con.
 730     apply lt_O_S
 731   ]
 732 ]
 733 qed.
 734
 735
 736
 737
 738
 739
 740
 741
 742
 743
 744
 745
 746
 747
 748
 749
 750
 751