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 (nat_case1 n)
 366   [ intros.
 367     rewrite > H7 in H6.
 368     rewrite > sym_times in H6.
 369     simplify in H6.
 370     rewrite > H6 in H.
 371     apply False_ind.
 372     change in H with ((S O) \le O).
 373     apply (not_le_Sn_O O H)
 374   | intros.
 375     apply (lt_O_S m)
 376   ]
 377 ]
 378 qed.
 379
 380
 381 (*6th*)
 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.
 384 intros.
 385 apply (nat_case1 n)
 386 [ intros.
 387   rewrite > H2 in H.
 388   apply False_ind.
 389   apply (not_le_Sn_O j H)
 390 | intros.
 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).
 396     apply le_times_l.
 397     apply (lt_to_divides_to_div_le)
 398     [ apply (nat_case1 m)
 399       [ intros.
 400         rewrite > H3 in H2.
 401         rewrite > H2 in H1.
 402         apply False_ind.
 403         apply (le_to_not_lt (S O) (S O))
 404         [ apply le_n
 405         | assumption
 406         ]
 407       | intros.
 408         rewrite > sym_gcd in \vdash (? ? %).
 409         apply (lt_O_gcd j (S m1)).
 410         apply (lt_O_S m1)
 411       ]
 412     | apply divides_gcd_n
 413     ]
 414   | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
 415     [
 416       apply lt_to_divides_to_div_le
 417       [ apply (nat_case1 m)
 418         [ intros.
 419           rewrite > H3 in H2.
 420           rewrite > H2 in H1.
 421           apply False_ind.
 422           apply (le_to_not_lt (S O) (S O))
 423           [ apply le_n
 424           | assumption
 425           ]
 426         | intros.
 427           rewrite > sym_gcd in \vdash (? ? %).
 428           apply (lt_O_gcd j (S m1)).
 429           apply (lt_O_S m1)
 430         ]
 431       | rewrite > sym_gcd in \vdash (? % ?).
 432         apply divides_gcd_n
 433       ]
 434     | rewrite > H2 in H.
 435       rewrite < (pred_Sn m) in H.
 436       apply (trans_lt j m (S m))
 437       [ assumption.
 438       | change with ((S m) \le (S m)).
 439         apply (le_n (S m))
 440       ]
 441     ]
 442   ]
 443 ]
 444 qed.
 445
 446
 447
 448
 449 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
 450    and n = 1 are dealed as particular cases in theorem
 451    sum_divisor_totient)
 452  *)
 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).
 454 intros.
 455 unfold totient.
 456 apply (trans_eq ? ?
 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))))
 459   [ apply eq_sigma_p1
 460     [ intros.
 461       reflexivity
 462     | intros.
 463       apply sym_eq.
 464       apply (trans_eq ? ?
 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
 467         [ apply lt_to_le.
 468           assumption
 469         | intros.
 470           rewrite > lt_to_leb_false
 471           [ reflexivity
 472           | apply le_S_S.
 473             assumption
 474           ]
 475         ]
 476       | apply eq_sigma_p
 477         [ intros.
 478           rewrite > le_to_leb_true
 479           [ reflexivity
 480           | assumption
 481           ]
 482         | intros.
 483           reflexivity
 484         ]
 485       ]
 486     ]
 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))) )
 496       (n*n)
 497       (pred n)
 498       (\lambda x:nat.
 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)))
 502       (\lambda x:nat.true)
 503       )
 504       [ intros.
 505         reflexivity
 506       | intros.
 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)))
 511               [ rewrite > Hcut3.
 512                 cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
 513                 [ rewrite > Hcut4.
 514                   cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
 515                   [ rewrite > Hcut5.
 516                     apply sym_eq.
 517                     apply div_mod.
 518                     apply (trans_lt O (S O) n)
 519                     [ apply (lt_O_S O)
 520                     | assumption
 521                     ]
 522                   | elim Hcut.
 523                     rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
 524                     rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
 525                     rewrite > (div_times_ltO n2 (i/n))
 526                     [ rewrite > H3.
 527                       apply div_times_ltO.
 528                       apply (divides_to_lt_O n2 (pred n))
 529                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 530                         assumption
 531                       | apply (witness n2 (pred n) (i/n)).
 532                         rewrite > sym_times.
 533                         assumption
 534                       ]
 535                     | apply (divides_to_lt_O (i/n) (pred n))
 536                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 537                         assumption
 538                       | apply (witness (i/n) (pred n) n2).
 539                         assumption
 540                       ]
 541                     ]
 542                   ]
 543                 | elim Hcut.
 544                   cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
 545                   [ rewrite > Hcut4.
 546                     rewrite > H3.
 547                     rewrite < (sym_times n2 (i/n)).
 548                     rewrite > (div_times_ltO n2 (i/n))
 549                     [ rewrite > (div_times_ltO (i \mod n) n2)
 550                       [ reflexivity
 551                       | apply (divides_to_lt_O n2 (pred n))
 552                         [ apply (n_gt_Uno_to_O_lt_pred_n n).
 553                           assumption
 554                         | apply (witness n2 (pred n) (i/n)).
 555                           rewrite > sym_times.
 556                           assumption
 557                         ]
 558                       ]
 559                     | apply (divides_to_lt_O (i/n) (pred n))
 560                       [ apply (n_gt_Uno_to_O_lt_pred_n n).
 561                         assumption
 562                       | assumption
 563                       ]
 564                     ]
 565                   | apply (sym_eq).
 566                     apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
 567                     [ apply (n_gt_Uno_to_O_lt_pred_n n).
 568                       assumption
 569                     | assumption
 570                     ]
 571                   ]
 572                 ]
 573               | apply (sum_divisor_totient1_aux2);
 574                 assumption
 575               ]
 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))
 580               ).
 581               apply (andb_true_true
 582                ((eqb (gcd (i\mod n) (i/n)) (S O))
 583                 \land
 584                 (leb (S (i\mod n)) (i/n)))
 585                      (divides_b (i/n) (pred n))
 586               ).
 587               rewrite > andb_sym.
 588               rewrite > andb_sym in \vdash (? ? (? ? %) ?).
 589               assumption
 590             ]
 591           | change with (S (i \mod n) \le (i/n)).
 592             cut (leb (S (i \mod n)) (i/n) = true)
 593             [ change with (
 594                 match (true) with
 595                 [ true  \Rightarrow (S (i \mod n)) \leq (i/n)
 596                 | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
 597               ).
 598               rewrite < Hcut1.
 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))
 603               ).
 604               rewrite > andb_sym in \vdash (? ? (? % ?) ?).
 605               rewrite < (andb_assoc) in \vdash (? ? % ?).
 606               assumption
 607             ]
 608           ]
 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))
 614           ).
 615           rewrite < andb_assoc.
 616           assumption.
 617         ]
 618       | intros.
 619         apply (sum_divisor_totient1_aux_3);
 620           assumption.
 621       | intros.
 622         apply (sum_divisor_totient1_aux_4);
 623           assumption.
 624       | intros.
 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).
 630                 assumption
 631               | rewrite > sym_gcd.
 632                 apply lt_O_gcd.
 633                 apply (n_gt_Uno_to_O_lt_pred_n n).
 634                 assumption
 635               | assumption
 636               | apply divides_gcd_m
 637               | rewrite > sym_gcd.
 638                 apply divides_gcd_m
 639               ]
 640             | assumption
 641             ]
 642           | assumption
 643           ]
 644         | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
 645           [ apply (lt_to_divides_to_div_le)
 646             [ rewrite > sym_gcd.
 647               apply lt_O_gcd.
 648               apply (n_gt_Uno_to_O_lt_pred_n n).
 649               assumption
 650             | apply divides_gcd_m
 651             ]
 652           | apply (lt_to_le_to_lt j (pred n) n)
 653             [ assumption
 654             | apply le_pred_n
 655             ]
 656           ]
 657         ]
 658       | intros.
 659         apply (sum_divisor_totient1_aux_6);
 660           assumption.
 661       ]
 662     | apply (sigma_p_true).
 663     ]
 664   ]
 665 qed.
 666
 667
 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
 672   (pred n).
 673  *)
 674 theorem sum_divisor_totient: \forall n.
 675 sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
 676 intros.
 677 apply (nat_case1 n)
 678 [ intros.
 679   simplify.
 680   reflexivity
 681 | intros.
 682   apply (nat_case1 m)
 683   [ intros.
 684     simplify.
 685     reflexivity
 686   | intros.
 687     rewrite < H1.
 688     rewrite < H.
 689     rewrite > (pred_Sn m).
 690     rewrite < H.
 691     apply( sum_divisor_totient1).
 692     rewrite > H.
 693     rewrite > H1.
 694     apply cic:/matita/algebra/finite_groups/lt_S_S.con.
 695     apply lt_O_S
 696   ]
 697 ]
 698 qed.
 699
 700
 701
 702
 703
 704
 705
 706
 707
 708
 709
 710
 711
 712
 713
 714
 715
 716