The abstract of the Mizar article:

The Divisibility of Integers and Integer Relatively Primes

by

Rafal Kwiatek, and

Grzegorz Zwara

Received July 10, 1990

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;