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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/primes.ma".
14 definition S_mod ≝ λn,m:nat. S m \mod n.
16 definition congruent ≝ λn,m,p:nat. mod n p = mod m p.
18 interpretation "congruent" 'congruent n m p = (congruent n m p).
20 theorem congruent_n_n: ∀n,p:nat.congruent n n p.
23 theorem transitive_congruent: ∀p. transitive ? (λn,m. congruent n m p).
26 theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
27 #n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
28 % // @lt_mod_m_m @(ltn_to_ltO … ltnm)
31 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
32 #n #p #posp >(div_mod (n \mod p) p) in ⊢ (??%?);
33 >(eq_div_O ? p) // @lt_mod_m_m //
36 theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m →
37 n \mod p = (n \mod (m*p)) \mod p.
39 @(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
40 [@div_mod_spec_div_mod //
42 >distributive_times_plus_r >associative_plus <div_mod //
46 theorem congruent_n_mod_n: ∀n,p. 0 < p →
47 congruent n (n \mod p) p.
48 #n #p #posp @mod_mod //
51 theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m →
52 congruent n (n \mod (m*p)) p.
53 #n #p #posp @mod_times_mod
56 theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p →
57 n = r*p+m → congruent n m p.
59 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
60 [@div_mod_spec_div_mod //
62 >commutative_times >distributive_times_plus >commutative_times
63 >(commutative_times p) >associative_plus //
67 theorem divides_to_congruent: ∀n,m,p:nat. 0 < p → m ≤ n →
68 divides p (n - m) → congruent n m p.
69 #n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
70 >commutative_plus @minus_to_plus //
73 theorem congruent_to_divides: ∀n,m,p:nat.
74 0 < p → congruent n m p → divides p (n - m).
75 #n #m #p #posp #Hcong %{((n / p)-(m / p))}
76 >commutative_times >(div_mod n p) in ⊢ (??%?);
77 >(div_mod m p) in ⊢ (??%?); //
80 theorem mod_times: ∀n,m,p. 0 < p →
81 mod (n*m) p = mod ((mod n p)*(mod m p)) p.
83 @(eq_times_plus_to_congruent ? ? p
84 ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
85 @(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
86 @(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
87 (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
88 [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d)
89 [#a #b #c #d >(distributive_times_plus_r (c+d) a b)
90 >(distributive_times_plus a c d)
91 >(distributive_times_plus b c d) //] #Hcut
94 [<associative_times >(associative_times (n/p) p (m \mod p))
95 >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
96 >distributive_times_plus_r //
102 theorem congruent_times: ∀n,m,n1,m1,p. O < p → congruent n n1 p →
103 congruent m m1 p → congruent (n*m) (n1*m1) p.
104 #n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
105 >(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //