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 (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)))
 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 n_gt_Uno_to_O_lt_pred_n.
 157           assumption
 158         | change with ((S (i\mod n)) \le (i/n)).
 159           apply (aux_S_i_mod_n_le_i_div_n i n);
 160             assumption
 161         ]
 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);
 164           assumption
 165       | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
 166         apply (divides_times).
 167         apply divides_n_n.
 168         apply divides_SO_n
 169       ]
 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);
 172         assumption
 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 (? ? % ?).
 182         assumption
 183       | apply divides_SO_n
 184       ]
 185     ]
 186   ]
 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);
 192       assumption.
 193   ]
 194 ]qed.
 195
 196
 197 (*4th*)
 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))
 203         \land (eqb
 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))))
 206 =true.
 207 intros.
 208 cut (O \lt (pred n))
 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)
 213         [ rewrite > Hcut3.
 214           rewrite > Hcut4.
 215           apply andb_t_t_t
 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))
 218               [ assumption
 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))
 222                 [ assumption
 223                 | assumption
 224                 | apply (divides_gcd_n (pred n))
 225                 ]
 226               ]
 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))
 229               [ reflexivity
 230               | assumption
 231               | apply (divides_gcd_n (pred n))
 232               ]
 233             ]
 234           | apply (le_to_leb_true).
 235             apply lt_S_to_le.
 236             apply cic:/matita/algebra/finite_groups/lt_S_S.con.
 237             apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
 238             [ assumption
 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))
 241                 [ assumption
 242                 | assumption
 243                 | apply divides_gcd_n
 244                 ]
 245               | assumption
 246               | rewrite > sym_gcd.
 247                 apply divides_gcd_n
 248               ]
 249             ]
 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))
 252             [ assumption
 253             | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
 254               [ assumption
 255               | simplify.
 256                 rewrite > NdivM_times_M_to_N
 257                 [ assumption
 258                 | assumption
 259                 | apply divides_gcd_n
 260                 ]
 261               ]
 262             | rewrite > NdivM_times_M_to_N
 263               [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
 264                 [ reflexivity
 265                 | assumption
 266                 | rewrite > sym_gcd.
 267                   apply divides_gcd_n
 268                 ]
 269               | assumption
 270               | apply divides_gcd_n
 271               ]
 272             ]
 273           ]
 274         | apply (mod_plus_times).
 275           assumption
 276         ]
 277       | apply (div_plus_times).
 278         assumption
 279       ]
 280     | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
 281       [ assumption
 282       | rewrite > NdivM_times_M_to_N
 283         [ apply (lt_to_le_to_lt j (pred n) ?)
 284           [ assumption
 285           | apply (lt_to_le).
 286             apply (lt_to_le_to_lt ? n ?)
 287             [ change with ((S (pred n)) \le n).
 288               rewrite < (S_pred n)
 289               [ apply le_n
 290               | apply (trans_lt ? (S O)  ?)
 291                 [ change with ((S O) \le (S O)).
 292                   apply (le_n (S O))
 293                 | assumption
 294                 ]
 295               ]
 296             | rewrite > (times_n_SO n) in \vdash (? % ?).
 297               apply (le_times n)
 298               [ apply (le_n n)
 299               | change with (O \lt (gcd (pred n) j)).
 300                 assumption
 301               ]
 302             ]
 303           ]
 304         | assumption
 305         | rewrite > sym_gcd.
 306           apply (divides_gcd_n)
 307         ]
 308       ]
 309     ]
 310   | rewrite > sym_gcd.
 311     apply (lt_O_gcd).
 312     assumption
 313   ]
 314 | apply n_gt_Uno_to_O_lt_pred_n.
 315   assumption
 316 ]
 317 qed.
 318
 319
 320
 321
 322 (*5th*)
 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.
 326 intros.
 327 elim H3.
 328 elim H4.
 329 cut (O \lt n)
 330 [ rewrite > H6 in \vdash (? ? (? ? %) ?).
 331   rewrite > sym_times in \vdash (? ? (? ? %) ?).
 332   rewrite > (div_times_ltO n b)
 333   [ cut (n \divides c)
 334     [ cut (a/b * c /n = a/b * (c/n))
 335       [ rewrite > Hcut2.
 336         cut (c/n = b)
 337         [ rewrite > Hcut3.
 338           apply (NdivM_times_M_to_N a b);
 339             assumption
 340         | rewrite > H6.
 341           apply (div_times_ltO b n).
 342           assumption
 343         ]
 344       | elim Hcut1.
 345         rewrite > H7.
 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).
 353             reflexivity
 354           | assumption
 355           ]
 356         | assumption
 357         ]
 358       ]
 359     | apply (witness n c b).
 360       rewrite > (sym_times n b).
 361       assumption
 362     ]
 363   | assumption
 364   ]
 365 | apply (divides_to_lt_O n c)
 366   [ assumption
 367   | apply (witness n c b).
 368     rewrite > sym_times.
 369     assumption
 370   ]
 371 ]
 372 qed.
 373
 374
 375 (*6th*)
 376 theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
 377 j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
 378 intros.
 379 apply (nat_case1 n)
 380 [ intros.
 381   rewrite > H2 in H.
 382   apply False_ind.
 383   apply (not_le_Sn_O j H)
 384 | intros.
 385   rewrite < (pred_Sn m).
 386   rewrite < (times_n_Sm (S m) m).
 387   rewrite > (sym_plus (S m) ((S m) * m)).
 388   apply le_to_lt_to_plus_lt
 389   [ rewrite > (sym_times (S m) m).
 390     apply le_times_l.
 391     apply (lt_to_divides_to_div_le)
 392     [ apply (nat_case1 m)
 393       [ intros.
 394         rewrite > H3 in H2.
 395         rewrite > H2 in H1.
 396         apply False_ind.
 397         apply (le_to_not_lt (S O) (S O))
 398         [ apply le_n
 399         | assumption
 400         ]
 401       | intros.
 402         rewrite > sym_gcd in \vdash (? ? %).
 403         apply (lt_O_gcd j (S m1)).
 404         apply (lt_O_S m1)
 405       ]
 406     | apply divides_gcd_n
 407     ]
 408   | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
 409     [
 410       apply lt_to_divides_to_div_le
 411       [ apply (nat_case1 m)
 412         [ intros.
 413           rewrite > H3 in H2.
 414           rewrite > H2 in H1.
 415           apply False_ind.
 416           apply (le_to_not_lt (S O) (S O))
 417           [ apply le_n
 418           | assumption
 419           ]
 420         | intros.
 421           rewrite > sym_gcd in \vdash (? ? %).
 422           apply (lt_O_gcd j (S m1)).
 423           apply (lt_O_S m1)
 424         ]
 425       | rewrite > sym_gcd in \vdash (? % ?).
 426         apply divides_gcd_n
 427       ]
 428     | rewrite > H2 in H.
 429       rewrite < (pred_Sn m) in H.
 430       apply (trans_lt j m (S m))
 431       [ assumption.
 432       | change with ((S m) \le (S m)).
 433         apply (le_n (S m))
 434       ]
 435     ]
 436   ]
 437 ]
 438 qed.
 439
 440
 441
 442
 443 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
 444    and n = 1 are dealed as particular cases in theorem
 445    sum_divisor_totient)
 446  *)
 447 theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
 448 intros.
 449 unfold totient.
 450 apply (trans_eq ? ?
 451 (sigma_p n (\lambda d:nat.divides_b d (pred n))
 452 (\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))))
 453   [ apply eq_sigma_p1
 454     [ intros.
 455       reflexivity
 456     | intros.
 457       apply sym_eq.
 458       apply (trans_eq ? ?
 459        (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
 460       [ apply false_to_eq_sigma_p
 461         [ apply lt_to_le.
 462           assumption
 463         | intros.
 464           rewrite > lt_to_leb_false
 465           [ reflexivity
 466           | apply le_S_S.
 467             assumption
 468           ]
 469         ]
 470       | apply eq_sigma_p
 471         [ intros.
 472           rewrite > le_to_leb_true
 473           [ reflexivity
 474           | assumption
 475           ]
 476         | intros.
 477           reflexivity
 478         ]
 479       ]
 480     ]
 481   | rewrite < (sigma_p2' n n
 482                (\lambda d:nat.divides_b d (pred n))
 483                (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
 484                (\lambda x,y.(S O))).
 485     apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
 486     [ apply (eq_sigma_p_gh
 487       (\lambda x:nat. (S O))
 488       (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) )  )
 489       (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
 490       (n*n)
 491       (pred n)
 492       (\lambda x:nat.
 493         divides_b (x/n) (pred n)
 494         \land (leb (S (x \mod n)) (x/n)
 495         \land eqb (gcd (x \mod n) (x/n)) (S O)))
 496       (\lambda x:nat.true)
 497       )
 498       [ intros.
 499         reflexivity
 500       | intros.
 501         cut ((i/n) \divides (pred n))
 502         [ cut ((i \mod n ) \lt (i/n))
 503           [ cut ((gcd (i \mod n) (i / n)) = (S O))
 504             [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
 505               [ rewrite > Hcut3.
 506                 cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
 507                 [ rewrite > Hcut4.
 508                   cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
 509                   [ rewrite > Hcut5.
 510                     apply sym_eq.
 511                     apply div_mod.
 512                     apply (trans_lt O (S O) n)
 513                     [ apply (lt_O_S O)
 514                     | assumption
 515                     ]
 516                   | elim Hcut.
 517                     rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
 518                     rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
 519                     rewrite > (div_times_ltO n2 (i/n))
 520                     [ rewrite > H3.
 521                       apply div_times_ltO.
 522                       apply (divides_to_lt_O n2 (pred n))
 523                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 524                         assumption
 525                       | apply (witness n2 (pred n) (i/n)).
 526                         rewrite > sym_times.
 527                         assumption
 528                       ]
 529                     | apply (divides_to_lt_O (i/n) (pred n))
 530                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 531                         assumption
 532                       | apply (witness (i/n) (pred n) n2).
 533                         assumption
 534                       ]
 535                     ]
 536                   ]
 537                 | elim Hcut.
 538                   cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
 539                   [ rewrite > Hcut4.
 540                     rewrite > H3.
 541                     rewrite < (sym_times n2 (i/n)).
 542                     rewrite > (div_times_ltO n2 (i/n))
 543                     [ rewrite > (div_times_ltO (i \mod n) n2)
 544                       [ reflexivity
 545                       | apply (divides_to_lt_O n2 (pred n))
 546                         [ apply (n_gt_Uno_to_O_lt_pred_n n).
 547                           assumption
 548                         | apply (witness n2 (pred n) (i/n)).
 549                           rewrite > sym_times.
 550                           assumption
 551                         ]
 552                       ]
 553                     | apply (divides_to_lt_O (i/n) (pred n))
 554                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 555                         assumption
 556                       | assumption
 557                       ]
 558                     ]
 559                   | apply (sym_eq).
 560                     apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
 561                     [ apply (n_gt_Uno_to_O_lt_pred_n n).
 562                       assumption
 563                     | assumption
 564                     ]
 565                   ]
 566                 ]
 567               | apply (sum_divisor_totient1_aux2);
 568                 assumption
 569               ]
 570             | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
 571               apply (andb_true_true
 572               (eqb (gcd (i\mod n) (i/n)) (S O))
 573               (leb (S (i\mod n)) (i/n))
 574               ).
 575               apply (andb_true_true
 576                ((eqb (gcd (i\mod n) (i/n)) (S O))
 577                 \land
 578                 (leb (S (i\mod n)) (i/n)))
 579                      (divides_b (i/n) (pred n))
 580               ).
 581               rewrite > andb_sym.
 582               rewrite > andb_sym in \vdash (? ? (? ? %) ?).
 583               assumption
 584             ]
 585           | change with (S (i \mod n) \le (i/n)).
 586             cut (leb (S (i \mod n)) (i/n) = true)
 587             [ change with (
 588                 match (true) with
 589                 [ true  \Rightarrow (S (i \mod n)) \leq (i/n)
 590                 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
 591               ).
 592               rewrite < Hcut1.
 593               apply (leb_to_Prop (S(i \mod n)) (i/n))
 594             | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n))  ).
 595               apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
 596                 (eqb (gcd (i\mod n) (i/n)) (S O))
 597               ).
 598               rewrite > andb_sym in \vdash (? ? (? % ?) ?).
 599               rewrite < (andb_assoc) in \vdash (? ? % ?).
 600               assumption
 601             ]
 602           ]
 603         | apply (divides_b_true_to_divides ).
 604           apply (andb_true_true (divides_b (i/n) (pred n))
 605                           (leb (S (i\mod n)) (i/n))).
 606           apply (andb_true_true ( (divides_b (i/n) (pred n)) \land  (leb (S (i\mod n)) (i/n)) )
 607             (eqb (gcd (i\mod n) (i/n)) (S O))
 608           ).
 609           rewrite < andb_assoc.
 610           assumption.
 611         ]
 612       | intros.
 613         apply (sum_divisor_totient1_aux_3);
 614           assumption.
 615       | intros.
 616         apply (sum_divisor_totient1_aux_4);
 617           assumption.
 618       | intros.
 619         cut (j/(gcd (pred n) j) \lt n)
 620         [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
 621           [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
 622             [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
 623               [ apply (n_gt_Uno_to_O_lt_pred_n n).
 624                 assumption
 625               | rewrite > sym_gcd.
 626                 apply lt_O_gcd.
 627                 apply (n_gt_Uno_to_O_lt_pred_n n).
 628                 assumption
 629               | assumption
 630               | apply divides_gcd_m
 631               | rewrite > sym_gcd.
 632                 apply divides_gcd_m
 633               ]
 634             | assumption
 635             ]
 636           | assumption
 637           ]
 638         | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
 639           [ apply (lt_to_divides_to_div_le)
 640             [ rewrite > sym_gcd.
 641               apply lt_O_gcd.
 642               apply (n_gt_Uno_to_O_lt_pred_n n).
 643               assumption
 644             | apply divides_gcd_m
 645             ]
 646           | apply (lt_to_le_to_lt j (pred n) n)
 647             [ assumption
 648             | apply le_pred_n
 649             ]
 650           ]
 651         ]
 652       | intros.
 653         apply (sum_divisor_totient1_aux_6);
 654           assumption.
 655       ]
 656     | apply (sigma_p_true).
 657     ]
 658   ]
 659 qed.
 660
 661
 662 (*there's a little difference between the following definition of the
 663   theorem, and the abstract definition given before.
 664   in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
 665   that's why in the definition of the theorem the summary is set equal to
 666   (pred n).
 667  *)
 668 theorem sum_divisor_totient: \forall n.
 669 sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
 670 intros.
 671 apply (nat_case1 n)
 672 [ intros.
 673   simplify.
 674   reflexivity
 675 | intros.
 676   apply (nat_case1 m)
 677   [ intros.
 678     simplify.
 679     reflexivity
 680   | intros.
 681     rewrite < H1.
 682     rewrite < H.
 683     rewrite > (pred_Sn m).
 684     rewrite < H.
 685     apply( sum_divisor_totient1).
 686     rewrite > H.
 687     rewrite > H1.
 688     apply cic:/matita/algebra/finite_groups/lt_S_S.con.
 689     apply lt_O_S
 690   ]
 691 ]
 692 qed.
 693
 694
 695
 696
 697
 698
 699
 700
 701
 702
 703
 704
 705
 706
 707
 708
 709
 710