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