matita/matita/lib/arithmetics/fermat_little_theorem.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/exp.ma".
  13 include "arithmetics/gcd.ma".
  14 include "arithmetics/permutation.ma".
  15 include "arithmetics/congruence.ma".
  16 include "arithmetics/sigma_pi.ma".
  17
  18 theorem permut_S_mod: ∀n:nat. permut (S_mod (S n)) n.
  19 #n %
  20   [#i #lein @le_S_S_to_le @lt_mod_m_m //
  21   |#i #j #lein #lejn #Heq @injective_S
  22    <(lt_to_eq_mod i (S n)) [2: @le_S_S @lein]
  23    <(lt_to_eq_mod j (S n)) [2: @le_S_S @lejn]
  24    cases (le_to_or_lt_eq … lein) #Hi
  25    cases (le_to_or_lt_eq … lejn) #Hj
  26     [(* i < n, j< n *)
  27      <mod_S
  28       [<mod_S
  29         [@Heq |@le_S_S >lt_to_eq_mod // @le_S // |//]
  30       |@le_S_S >lt_to_eq_mod // @le_S //
  31       |//
  32       ]
  33     |(* i < n, j=n *)
  34      @False_ind @(absurd ?? (not_eq_O_S (i \mod (S n))))
  35      @sym_eq <(mod_n_n (S n)) [2://]
  36      <Hj in ⊢ (???(?%?)); <mod_S
  37       [@Heq |>lt_to_eq_mod [@le_S_S @Hi |@le_S_S @lt_to_le @Hi]|//]
  38     |(* i = n, j < n *)
  39      @False_ind @(absurd ?? (not_eq_O_S (j \mod (S n))))
  40      <(mod_n_n (S n)) [2://]
  41      <Hi in ⊢ (??(?%?)?); <mod_S
  42       [@Heq |>lt_to_eq_mod [@le_S_S @Hj |@le_S_S @lt_to_le @Hj]|//]
  43     |(* i = n, j= n*)
  44      >Hi >Hj %
  45     ]
  46   ]
  47 qed.
  48
  49 theorem prime_to_not_divides_fact: ∀p.prime p → ∀n.n < p → p ∤ n!.
  50 #p #primep #n elim n
  51   [normalize #_ % #divp @(absurd (p ≤1))
  52     [@divides_to_le // |@lt_to_not_le @prime_to_lt_SO //]
  53   |#n1 #Hind #ltn1 whd in match (fact ?); % #Hdiv
  54    cases (divides_times_to_divides … Hdiv)
  55     [-Hdiv #Hdiv @(absurd … Hdiv) @Hind @lt_to_le //
  56     |-Hdiv #Hdiv @(absurd … (p ≤ S n1))
  57       [@divides_to_le // |@lt_to_not_le //]
  58     |@primep
  59     ]
  60   ]
  61 qed.
  62
  63 theorem permut_mod: ∀p,a:nat. prime p →
  64   p ∤ a → permut (λn.(mod (a*n) p)) (pred p).
  65 #p #a #primep #ndiv %
  66   [#i #lei @le_S_S_to_le @(transitive_le ? p)
  67     [@lt_mod_m_m @prime_to_lt_O //
  68     |>S_pred [//| @prime_to_lt_O //]
  69     ]
  70   |#i #j #lei #lej #H cases (decidable_lt i j)
  71     [(* i < j *) #ltij
  72      @False_ind @(absurd (j-i < p))
  73       [<(S_pred p) [2:@prime_to_lt_O //]
  74        @le_S_S @le_plus_to_minus @(transitive_le … lej) //
  75       |@le_to_not_lt @divides_to_le [@lt_plus_to_minus_r //]
  76        cut (p ∣ a ∨ p ∣ (j-i))
  77         [2:* [#Hdiv @False_ind /2/ | //]]
  78        @divides_times_to_divides // >distributive_times_minus
  79        @eq_mod_to_divides // @prime_to_lt_O //
  80       ]
  81     |#Hij cases (le_to_or_lt_eq … (not_lt_to_le … Hij)) -Hij #Hij
  82       [(* j < i *)
  83        @False_ind @(absurd (i-j < p))
  84         [<(S_pred p) [2:@prime_to_lt_O //]
  85          @le_S_S @le_plus_to_minus @(transitive_le … lei) //
  86         |@le_to_not_lt @divides_to_le [@lt_plus_to_minus_r //]
  87          cut (p ∣ a ∨ p ∣ (i-j))
  88           [2:* [#Hdiv @False_ind /2/ | //]]
  89          @divides_times_to_divides // >distributive_times_minus
  90          @eq_mod_to_divides // @prime_to_lt_O //
  91         ]
  92       |(* i = j *) //
  93       ]
  94     ]
  95   ]
  96 qed.
  97
  98 theorem eq_fact_pi_p:∀n.
  99   fact n = ∏_{i ∈ [1,S n[ } i.
 100 #n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue
 101   [cut (S n1 -1 = n1) [normalize //] #Hcut
 102    <plus_n_Sm <plus_n_O @eq_f <Hcut in ⊢ (???%); // | % ]
 103 qed.
 104
 105 theorem congruent_pi: ∀f,n,p.O < p →
 106   congruent (∏_{i < n}(f i)) (∏_{i < n} (mod (f i) p)) p.
 107 #f #n elim n // #n1 #Hind #p #posp >bigop_Strue //
 108 @congruent_times // [@congruent_n_mod_n // |@Hind //]
 109 qed.
 110
 111 theorem congruent_exp_pred_SO: ∀p,a:nat. prime p → ¬ divides p a →
 112 congruent (exp a (pred p)) (S O) p.
 113 #p #a #primep #ndiv
 114 cut (0 < a)
 115   [lapply ndiv cases a // * #div0 @False_ind @div0 @(quotient ? 0 0) //] #posa
 116 cut (O < p) [@prime_to_lt_O //] #posp
 117 cut (O < pred p) [@le_S_S_to_le >S_pred [@prime_to_lt_SO //| @posp] ] #pospred
 118 @(divides_to_congruent … posp)
 119   [@lt_O_exp //
 120   |cut (divides p (exp a (pred p)-1) ∨ divides p (pred p)!)
 121     [@divides_times_to_divides // >commutative_times
 122      >distributive_times_minus <times_n_1
 123      >eq_fact_pi_p >commutative_times
 124      cut (pred p = S (pred p) -1) [//] #Hpred >Hpred in match (exp a ?);
 125      >exp_pi_bc @congruent_to_divides //
 126      @(transitive_congruent p ? (∏_{i ∈ [1,S(pred p)[ }(a*i \mod p)))
 127       [@(congruent_pi (λm.a*(m +1))) //
 128       |cut (∏_{i ∈ [1,S(pred p)[ } i =  ∏_{i ∈ [1,S(pred p)[ } (a*i\mod p))
 129         [2: #Heq <Heq @congruent_n_n]
 130        >(bigop_I_gen 1 (S (pred p)) … 1 timesA) //
 131        >(bigop_I_gen 1 (S (pred p)) … 1 timesA) //
 132        @sym_eq @(bigop_iso … timesAC)
 133        lapply (permut_mod … primep ndiv) #Hpermut
 134        %{(λi.a*i \mod p)} %{(invert_permut (pred p) (λi.a*i \mod p))} %
 135         [%
 136           [#i #lti #_ %
 137           |#i #lti #posi %
 138             [%
 139               [>(S_pred … posp) @lt_mod_m_m //
 140               |>le_to_leb_true //
 141                cases (le_to_or_lt_eq … (le_O_n (a*i \mod p))) [//]
 142                #H @False_ind @(absurd ? (mod_O_to_divides …(sym_eq  … H))) //
 143                @(not_to_not … ndiv) #Hdiv cases(divides_times_to_divides … Hdiv)
 144                // #divpi @False_ind @(absurd ? lti) @le_to_not_lt
 145                >(S_pred … posp) @divides_to_le // @leb_true_to_le
 146                @(andb_true_l … posi)
 147               ]
 148             |@invert_permut_f [@le_S_S_to_le //|cases Hpermut // ]
 149             ]
 150           ]
 151         |lapply (permut_invert_permut … Hpermut) *
 152          #le_invert_permut #inj_inv_permut
 153          #i #lti #posi %
 154           [%
 155             [@le_S_S @le_invert_permut @le_S_S_to_le //
 156             |>le_to_leb_true //
 157              cases (le_to_or_lt_eq …
 158                (le_O_n (invert_permut (pred p) (λi.a*i \mod p) i))) [//]
 159              #H @False_ind
 160              cut (a*0 \mod p = 0) [<times_n_O //] #H0
 161              cut (a*0 \mod p = a*(invert_permut (pred p) (λi.a*i \mod p) i) \mod p)
 162                [@(eq_f ?? (λi.a*i \mod p)) //]
 163              >H0 >(f_invert_permut (λi.a*i \mod p) … Hpermut) [2:@le_S_S_to_le //]
 164              #eq0i <eq0i in posi; normalize #H destruct (H)
 165             ]
 166           |@f_invert_permut [@le_S_S_to_le //| @Hpermut ]
 167           ]
 168         ]
 169       ]
 170     |* // #Hdiv @False_ind
 171      @(absurd ? Hdiv (prime_to_not_divides_fact p primep (pred p) ?))
 172      @le_S_S_to_le >S_pred //
 173     ]
 174   ]
 175 qed.
 176