:: The Divisibility of Integers and Integer Relatively Primes
:: by Rafa{\l} Kwiatek and Grzegorz Zwara
::
:: Received July 10, 1990
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, INT_1, ORDINAL1, COMPLEX1, SUBSET_1, XXREAL_0, CARD_1,
ARYTM_3, ARYTM_1, RELAT_1, NAT_1, XCMPLX_0, INT_2;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_1, COMPLEX1,
XXREAL_0;
constructors XXREAL_0, REAL_1, NAT_1, COMPLEX1, INT_1, CARD_1;
registrations XREAL_0, NAT_1, INT_1, ORDINAL1, CARD_1;
requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
begin
definition
let a be Integer;
redefine func |.a.| -> Element of NAT;
end;
reserve a,b,c for Integer;
theorem :: INT_2:1
a divides b & a divides b + c implies a divides c;
theorem :: INT_2:2 :: NAT_D:9
a divides b implies a divides b * c;
theorem :: INT_2:3
0 divides a iff a = 0;
reserve i,j,k,l for Nat;
definition
let a,b be Integer;
func a lcm b -> Nat means
:: INT_2:def 1
a divides it & b divides it & for m being
Integer st a divides m & b divides m holds it divides m;
commutativity;
end;
theorem :: INT_2:4
a = 0 or b = 0 iff a lcm b = 0;
definition
let a,b be Integer;
func a gcd b -> Nat means
:: INT_2:def 2
it divides a & it divides b &
for m being Integer st m divides a & m divides b holds m divides it;
commutativity;
end;
theorem :: INT_2:5
a = 0 & b = 0 iff a gcd b = 0;
reserve n for Nat;
reserve a,b,c,d,a1,b1,a2,b2,k,l for Integer;
theorem :: INT_2:6
-n is Element of NAT iff n = 0;
registration
let n be non zero Nat;
cluster -n -> non natural;
end;
theorem :: INT_2:7
not -1 is Element of NAT;
theorem :: INT_2:8
a divides -a & -a divides a;
theorem :: INT_2:9
a divides b & b divides c implies a divides c;
theorem :: INT_2:10
(a divides b iff a divides -b) & (a divides b iff -a divides b) &
(a divides b iff -a divides -b) & (a divides -b iff -a divides b);
theorem :: INT_2:11
a divides b & b divides a implies a = b or a = -b;
theorem :: INT_2:12
a divides 0 & 1 divides a & -1 divides a;
theorem :: INT_2:13
a divides 1 or a divides -1 implies a = 1 or a = -1;
theorem :: INT_2:14
a = 1 or a = -1 implies a divides 1 & a divides -1;
theorem :: INT_2:15
a,b are_congruent_mod c iff c divides (a-b);
theorem :: INT_2:16
a divides b iff (|.a.|) divides (|.b.|);
theorem :: INT_2:17
a lcm b is Element of NAT;
theorem :: INT_2:18
a divides a lcm b;
theorem :: INT_2:19
for c st a divides c & b divides c holds a lcm b divides c;
theorem :: INT_2:20
a gcd b is Element of NAT;
theorem :: INT_2:21
a gcd b divides a;
theorem :: INT_2:22
for c st c divides a & c divides b holds c divides (a gcd b);
:: Relative Prime Numbers
definition
let a,b be Integer;
pred a,b are_coprime means
:: INT_2:def 3
a gcd b = 1;
symmetry;
end;
theorem :: INT_2:23
a<>0 or b<>0 implies ex a1,b1 st a = (a gcd b)*a1 & b = (a gcd b)*b1 &
a1,b1 are_coprime;
theorem :: INT_2:24
a,b are_coprime implies (c*a gcd c*b) = |.c.| & c*a gcd
b*c = |.c.| & a*c gcd c*b = |.c.| & a*c gcd b*c = |.c.|;
theorem :: INT_2:25
c divides a*b & a,c are_coprime implies c divides b;
theorem :: INT_2:26
a,c are_coprime & b,c are_coprime implies
a*b,c are_coprime;
::***************************************************************************::
:: PRIME NUMBERS ::
::***************************************************************************::
reserve p,p1,q,l for Nat;
definition
let p be integer Number;
attr p is prime means
:: INT_2:def 4
p > 1 & for n being Nat st n divides p holds n = 1 or n = p;
end;
registration
cluster prime -> natural for integer Number;
end;
theorem :: INT_2:27
0 < b & a divides b implies a <= b;
theorem :: INT_2:28
2 is prime;
theorem :: INT_2:29
not 4 is prime;
registration
cluster prime for Nat;
cluster non zero non prime for Nat;
end;
theorem :: INT_2:30
p is prime & q is prime implies p,q are_coprime or p = q;
theorem :: INT_2:31
l>=2 implies ex p being Element of NAT st p is prime & p divides l;
begin :: Addenda
:: from AMI_4, 2007.06.14, A.T.
theorem :: INT_2:32
for i,j being Integer st i >= 0 & j >= 0 holds
|.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j;
:: old definitions, 2007.11.07, A.T
theorem :: INT_2:33
a lcm b = |.a.| lcm |.b.|;
theorem :: INT_2:34
a gcd b = |.a.| gcd |.b.|;