Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### The Divisibility of Integers and Integer Relatively Primes

by
Rafal Kwiatek, and
Grzegorz Zwara

MML identifier: INT_2
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM_3, INT_1, ARYTM_1, ABSVALUE, FILTER_0, INT_2;
notation SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1, GROUP_1;
constructors REAL_1, NAT_1, GROUP_1, XBOOLE_0;
clusters INT_1, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, ARITHM;

begin

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::     SOME PROPERTIES ON FUNCTIONS: HCF & LCM FOR NATURAL NUMBERS        ::
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

reserve a,b,c,d,e,f,g,h,z for Nat;

canceled 2;

theorem :: INT_2:3
0 divides a iff a = 0;

theorem :: INT_2:4
a = 0 or b = 0 iff a lcm b = 0;

theorem :: INT_2:5
a = 0 & b = 0 iff a hcf b = 0;

theorem :: INT_2:6
a*b = (a lcm b)*(a hcf b);

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::                 SOME PROPERTIES OF INTEGER NUMBERS                   ::
::                              LCM,HCF                                 ::
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

reserve m,n for Nat;
reserve a,b,c,d,a1,b1,a2,b2,k,l for Integer;

canceled;

theorem :: INT_2:8
-n is Nat iff n = 0;

theorem :: INT_2:9
not -1 is Nat;

theorem :: INT_2:10
0 divides a iff a = 0;

theorem :: INT_2:11
a divides -a & -a divides a;

theorem :: INT_2:12
a divides b implies a divides b*c;

theorem :: INT_2:13
a divides b & b divides c implies a divides c;

theorem :: INT_2:14
(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:15
a divides b & b divides a implies a = b or a = -b;

theorem :: INT_2:16
a divides 0 & 1 divides a & -1 divides a;

theorem :: INT_2:17
a divides 1 or a divides -1 implies a = 1 or a = -1;

theorem :: INT_2:18
a = 1 or a = -1 implies a divides 1 & a divides -1;

theorem :: INT_2:19
a,b are_congruent_mod c iff c divides (a-b);

theorem :: INT_2:20
abs(a) is Nat;

theorem :: INT_2:21
a divides b iff (abs(a)) divides (abs(b));

::::::::::::::::::
::     LCM      ::
::::::::::::::::::

definition let a,b;
canceled;

func a lcm' b -> Integer equals
:: INT_2:def 2
abs(a) lcm abs(b);
commutativity;
end;

canceled;

theorem :: INT_2:23
a lcm' b is Nat;

canceled;

theorem :: INT_2:25
a divides (a lcm' b);

theorem :: INT_2:26
b divides (a lcm' b);

theorem :: INT_2:27
for c st a divides c & b divides c holds (a lcm' b) divides c;

::::::::::::::::::
::      GCD     ::
::::::::::::::::::

definition let a,b;
func a gcd b -> Integer equals
:: INT_2:def 3
abs(a) hcf abs(b);
commutativity;
end;

canceled;

theorem :: INT_2:29
a gcd b is Nat;

canceled;

theorem :: INT_2:31
(a gcd b) divides a;

theorem :: INT_2:32
(a gcd b) divides b;

theorem :: INT_2:33
for c st c divides a & c divides b holds c divides (a gcd b);

theorem :: INT_2:34
a = 0 or b = 0 iff a lcm' b = 0;

theorem :: INT_2:35
a = 0 & b = 0 iff a gcd b = 0;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::                      RELATIVE PRIME NUMBERS                            ::
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition let a,b;
pred a,b are_relative_prime means
:: INT_2:def 4
a gcd b = 1;
symmetry;
end;

canceled 2;

theorem :: INT_2:38
a<>0 or b<>0 implies ex a1,b1 st
a = (a gcd b)*a1 & b = (a gcd b)*b1 & a1,b1 are_relative_prime;

theorem :: INT_2:39
a,b are_relative_prime implies (c*a gcd c*b) = abs(c)
& c*a gcd b*c = abs(c) & a*c gcd c*b = abs(c) & a*c gcd b*c = abs(c);

theorem :: INT_2:40
c divides a*b & a,c are_relative_prime implies c divides b;

theorem :: INT_2:41
a,c are_relative_prime & b,c are_relative_prime implies
a*b,c are_relative_prime;

::***************************************************************************::
::                           PRIME NUMBERS                                   ::
::***************************************************************************::

reserve p,p1,q,k,l for Nat;
reserve x for Real;
reserve X for Subset of REAL;

definition let p;
attr p is prime means
:: INT_2:def 5
p>1 &
for n holds n divides p implies n = 1 or n = p;
end;

definition let m,n;
pred m,n are_relative_prime means
:: INT_2:def 6
m hcf n = 1;
end;

canceled 2;

theorem :: INT_2:44
2 is prime;

canceled;

theorem :: INT_2:46
ex p st not p is prime;

theorem :: INT_2:47
p is prime & q is prime implies p,q are_relative_prime or p = q;

scheme Ind1 { a() -> Nat,P[Nat] } : for k st k>=a() holds P[k] provided
P[a()] and
for k st k>=a() & P[k] holds P[k+1];

scheme Comp_Ind1 { a() -> Nat,P[Nat] } : for k st k>=a() holds P[k] provided
for k st k>=a() & (for n st n>=a() & n<k holds P[n]) holds P[k];

theorem :: INT_2:48
l>=2 implies ex p st p is prime & p divides l;
```