1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/fermat_little_theorem".
19 include "nat/permutation.ma".
20 include "nat/congruence.ma".
22 theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
23 intro.unfold permut.split.intros.
26 change with (S i) \mod (S n) < S n.
28 simplify.apply le_S_S.apply le_O_n.
31 rewrite < lt_to_eq_mod i (S n).
32 rewrite < lt_to_eq_mod j (S n).
40 apply H2.simplify.apply le_S_S.apply le_O_n.
41 rewrite > lt_to_eq_mod.
42 simplify.apply le_S_S.assumption.
43 simplify.apply le_S_S.assumption.
44 simplify.apply le_S_S.apply le_O_n.
45 rewrite > lt_to_eq_mod.
46 simplify.apply le_S_S.assumption.
47 simplify.apply le_S_S.assumption.
52 apply not_eq_O_S (i \mod (S n)).
54 rewrite < mod_n_n (S n).
55 rewrite < H4 in \vdash (? ? ? (? %?)).
56 rewrite < mod_S.assumption.
57 simplify.apply le_S_S.apply le_O_n.
58 rewrite > lt_to_eq_mod.
59 simplify.apply le_S_S.assumption.
60 simplify.apply le_S_S.assumption.
61 simplify.apply le_S_S.apply le_O_n.
65 apply not_eq_O_S (j \mod (S n)).
66 rewrite < mod_n_n (S n).
67 rewrite < H3 in \vdash (? ? (? %?) ?).
68 rewrite < mod_S.assumption.
69 simplify.apply le_S_S.apply le_O_n.
70 rewrite > lt_to_eq_mod.
71 simplify.apply le_S_S.assumption.
72 simplify.apply le_S_S.assumption.
73 simplify.apply le_S_S.apply le_O_n.
78 apply le_to_or_lt_eq.assumption.
79 apply le_to_or_lt_eq.assumption.
80 simplify.apply le_S_S.assumption.
81 simplify.apply le_S_S.assumption.
85 theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
88 change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
89 unfold S_mod in \vdash (? ? ? (? % ?)).
90 rewrite > lt_to_eq_mod.
91 apply eq_f.apply H.apply trans_lt ? (S n1).
92 simplify. apply le_n.assumption.assumption.
96 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
97 n \lt p \to \not divides p n!.
98 intros 3.elim n.simplify.intros.
99 apply lt_to_not_le (S O) p.
100 unfold prime in H.elim H.
101 assumption.apply divides_to_le.simplify.apply le_n.
103 change with (divides p ((S n1)*n1!)) \to False.
105 cut divides p (S n1) \lor divides p n1!.
106 elim Hcut.apply lt_to_not_le (S n1) p.
108 apply divides_to_le.simplify.apply le_S_S.apply le_O_n.
110 apply trans_lt ? (S n1).simplify. apply le_n.
111 assumption.assumption.
112 apply divides_times_to_divides.
113 assumption.assumption.
116 theorem permut_mod: \forall p,a:nat. prime p \to
117 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
118 unfold permut.intros.
119 split.intros.apply le_S_S_to_le.
121 change with mod (a*i) p < p.
123 simplify in H.elim H.
124 simplify.apply trans_le ? (S (S O)).
125 apply le_n_Sn.assumption.
126 rewrite < S_pred.apply le_n.
129 apply trans_lt ? (S O).simplify.apply le_n.assumption.
131 apply nat_compare_elim i j.
138 apply le_plus_to_minus.
139 apply trans_le ? (pred p).assumption.
144 apply trans_lt ? (S O).simplify.apply le_n.assumption.
145 apply le_to_not_lt p (j-i).
146 apply divides_to_le.simplify.
147 apply le_SO_minus.assumption.
148 cut divides p a \lor divides p (j-i).
149 elim Hcut.apply False_ind.apply H1.assumption.assumption.
150 apply divides_times_to_divides.assumption.
151 rewrite > distr_times_minus.
152 apply eq_mod_to_divides.
155 apply trans_lt ? (S O).simplify.apply le_n.assumption.
166 apply le_plus_to_minus.
167 apply trans_le ? (pred p).assumption.
172 apply trans_lt ? (S O).simplify.apply le_n.assumption.
173 apply le_to_not_lt p (i-j).
174 apply divides_to_le.simplify.
175 apply le_SO_minus.assumption.
176 cut divides p a \lor divides p (i-j).
177 elim Hcut.apply False_ind.apply H1.assumption.assumption.
178 apply divides_times_to_divides.assumption.
179 rewrite > distr_times_minus.
180 apply eq_mod_to_divides.
183 apply trans_lt ? (S O).simplify.apply le_n.assumption.
187 theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
188 congruent (exp a (pred p)) (S O) p.
193 apply divides_to_congruent.
195 change with O < exp a (pred p).
196 apply lt_O_exp.assumption.
197 cut divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!.
201 apply prime_to_not_divides_fact p H (pred p).
202 change with S (pred p) \le p.
203 rewrite < S_pred.apply le_n.
204 assumption.assumption.
205 apply divides_times_to_divides.
207 rewrite > times_minus_l.
208 rewrite > sym_times (S O).
209 rewrite < times_n_SO.
210 rewrite > S_pred (pred p).
211 rewrite > eq_fact_pi.
212 (* in \vdash (? ? (? % ?)). *)
214 apply congruent_to_divides.
216 apply transitive_congruent p ?
217 (pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)).
218 apply congruent_pi (\lambda m. a*m).
220 cut pi (pred(pred p)) (\lambda m.m) (S O)
221 = pi (pred(pred p)) (\lambda m.a*m \mod p) (S O).
222 rewrite > Hcut3.apply congruent_n_n.
223 rewrite < eq_map_iter_i_pi.
224 rewrite < eq_map_iter_i_pi.
225 apply permut_to_eq_map_iter_i.
228 rewrite < plus_n_Sm.rewrite < plus_n_O.
230 apply permut_mod.assumption.
231 assumption.assumption.
233 rewrite > Hcut3.rewrite < times_n_O.
234 apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
235 apply le_S_S_to_le.assumption.
237 change with (S O) \le pred p.
238 apply le_S_S_to_le.rewrite < S_pred.
239 unfold prime in H.elim H.assumption.assumption.
240 unfold prime in H.elim H.apply trans_lt ? (S O).
241 simplify.apply le_n.assumption.
242 cut O < a \lor O = a.
243 elim Hcut.assumption.
244 apply False_ind.apply H1.
246 apply witness ? ? O.apply times_n_O.
247 apply le_to_or_lt_eq.