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 notation "hvbox(n break ≅_{p} m)"
19 non associative with precedence 45
20 for @{ 'congruent $n $m $p }.
22 interpretation "congruent" 'congruent n m p = (congruent n m p).
24 theorem congruent_n_n: ∀n,p:nat.congruent n n p.
27 theorem transitive_congruent: ∀p. transitive ? (λn,m. congruent n m p).
30 theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
31 #n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
32 % // @lt_mod_m_m @(ltn_to_ltO … ltnm)
35 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
36 #n #p #posp >(div_mod (n \mod p) p) in ⊢ (??%?);
37 >(eq_div_O ? p) // @lt_mod_m_m //
40 theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m →
41 n \mod p = (n \mod (m*p)) \mod p.
43 @(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
44 [@div_mod_spec_div_mod //
46 >distributive_times_plus_r >associative_plus <div_mod //
50 theorem congruent_n_mod_n: ∀n,p. 0 < p →
51 congruent n (n \mod p) p.
52 #n #p #posp @mod_mod //
55 theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m →
56 congruent n (n \mod (m*p)) p.
57 #n #p #posp @mod_times_mod
60 theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p →
61 n = r*p+m → congruent n m p.
63 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
64 [@div_mod_spec_div_mod //
66 >commutative_times >distributive_times_plus >commutative_times
67 >(commutative_times p) >associative_plus //
71 theorem divides_to_congruent: ∀n,m,p:nat. 0 < p → m ≤ n →
72 divides p (n - m) → congruent n m p.
73 #n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
74 >commutative_plus @minus_to_plus //
77 theorem congruent_to_divides: ∀n,m,p:nat.
78 0 < p → congruent n m p → divides p (n - m).
79 #n #m #p #posp #Hcong %{((n / p)-(m / p))}
80 >commutative_times >(div_mod n p) in ⊢ (??%?);
81 >(div_mod m p) in ⊢ (??%?); //
84 theorem mod_times: ∀n,m,p. 0 < p →
85 mod (n*m) p = mod ((mod n p)*(mod m p)) p.
87 @(eq_times_plus_to_congruent ? ? p
88 ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
89 @(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
90 @(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
91 (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
92 [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d)
93 [#a #b #c #d >(distributive_times_plus_r (c+d) a b)
94 >(distributive_times_plus a c d)
95 >(distributive_times_plus b c d) //] #Hcut
98 [<associative_times >(associative_times (n/p) p (m \mod p))
99 >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
100 >distributive_times_plus_r //
106 theorem congruent_times: ∀n,m,n1,m1,p. O < p → congruent n n1 p →
107 congruent m m1 p → congruent (n*m) (n1*m1) p.
108 #n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
109 >(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //