:: The Divisibility of Integers and Integer Relatively Primes
:: by Rafa{\l} Kwiatek and Grzegorz Zwara
::
:: Received July 10, 1990
:: Copyright (c) 1990-2026 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, NEWTON;
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;
definitions INT_1;
expansions INT_1;
theorems INT_1, ABSVALUE, NAT_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0,
ORDINAL1;
schemes NAT_1;
begin
definition
let a be Integer;
redefine func |.a.| -> Element of NAT; :: redefines |. (COMPLEX1, definition)
coherence
proof
per cases;
suppose
A1: a >= 0;
then |.a.| = a by ABSVALUE:def 1;
hence thesis by A1,INT_1:3;
end;
suppose
a < 0;
then |.a.| = -a & -a > 0 by ABSVALUE:def 1,XREAL_1:58;
hence thesis by INT_1:3;
end;
end;
end;
reserve a,b,c for Integer;
theorem Th1:
a divides b & a divides b + c implies a divides c
proof
given u being Integer such that
A1: b = a * u;
given t being Integer such that
A2: b + c = a * t;
c = a*(t - u) by A1,A2;
hence thesis;
end;
theorem Th2: :: NAT_D:9
a divides b implies a divides b * c
proof
assume a divides b;
then consider l being Integer such that
A1: b = a * l;
a * l * c = a * (l * c);
hence thesis by A1;
end;
theorem
0 divides a iff a = 0;
Lm1: a divides -a & -a divides a
proof
-a = a*(-1);
hence a divides -a;
a = (-a)*(-1);
hence thesis;
end;
Lm2: a divides b & b divides c implies a divides c
proof
assume that
A1: a divides b and
A2: b divides c;
consider k being Integer such that
A3: b = a*k by A1;
consider l being Integer such that
A4: c = b*l by A2;
c = a*(k*l) by A3,A4;
hence thesis;
end;
Lm3: a divides b iff a divides -b
proof
thus a divides b implies a divides -b
proof
assume
A1: a divides b;
b divides -b by Lm1;
hence thesis by A1,Lm2;
end;
assume
A2: a divides -b;
-b divides b by Lm1;
hence thesis by A2,Lm2;
end;
Lm4: a divides b iff -a divides b
proof
thus a divides b implies -a divides b
proof
assume
A1: a divides b;
-a divides a by Lm1;
hence thesis by A1,Lm2;
end;
assume
A2: -a divides b;
a divides -a by Lm1;
hence thesis by A2,Lm2;
end;
Lm5: a divides 0 & 1 divides a & -1 divides a
proof
0 = a*0;
hence a divides 0;
a = 1*a;
hence 1 divides a;
a = (-1)*(-a);
hence thesis;
end;
Lm6: a divides b & a divides c implies a divides b mod c
proof
assume that
A1: a divides b and
A2: a divides c;
A3: now
assume c <> 0;
then
A4: b = c * (b div c) + (b mod c) by INT_1:59;
a divides c * (b div c) by A2,Th2;
hence thesis by A1,A4,Th1;
end;
now
assume c = 0;
then b mod c = 0;
hence thesis by Lm5;
end;
hence thesis by A3;
end;
reserve i,j,k,l for Nat;
Lm7: k divides l iff ex t being Nat st l = k * t
proof
hereby
assume
A1: k divides l;
thus ex t being Nat st l = k * t
proof
consider t being Integer such that
A2: l = k * t by A1;
per cases;
suppose
0 < l;
then 0 <= t by A2;
then reconsider t as Element of NAT by INT_1:3;
take t;
thus l = k * t by A2;
end;
suppose
A3: l = 0;
take 0;
thus l = k*0 by A3;
end;
end;
end;
assume ex t being Nat st l = k * t;
hence thesis;
end;
Lm8: i divides j & j divides i implies i = j
proof
assume i divides j;
then consider a such that
A1: j = i*a;
assume j divides i;
then consider b such that
A2: i = j*b;
i<>0 implies i = j
proof
A3: i >= 0;
assume
A4: i<>0;
1*i = i*(a*b) by A1,A2;
then a*b = 1 by A4,XCMPLX_1:5;
then i = j*1 or i = j*(-1) by A2,INT_1:9;
hence thesis by A4,A3;
end;
hence thesis by A1;
end;
definition
let a,b be Integer;
func a lcm b -> Nat means
:Def1:
a divides it & b divides it & for m being
Integer st a divides m & b divides m holds it divides m;
existence
proof
per cases;
suppose
A1: a = 0 or b = 0;
take 0;
thus a divides 0 & b divides 0 by Lm5;
thus thesis by A1;
end;
suppose
A2: a <> 0 & b <> 0;
defpred P[Nat] means a divides $1 & b divides $1 & $1 <> 0;
a*b in INT by INT_1:def 2;
then consider k being Nat such that
A3: a*b = k or a*b = -k by INT_1:def 1;
b divides a*b;
then
A4: b divides k by A3,Lm3;
a divides a*b;
then
A5: a divides k by A3,Lm3;
k <> 0 by A2,A3,XCMPLX_1:6;
then
A6: ex k being Nat st P[k] by A5,A4;
consider k being Nat such that
A7: P[k] and
A8: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A6);
take k;
thus a divides k & b divides k by A7;
let m be Integer;
m in INT by INT_1:def 2;
then consider n being Nat such that
A9: m = n or m = - n by INT_1:def 1;
assume that
A10: a divides m and
A11: b divides m;
b divides n by A9,A11,Lm3;
then
A12: b divides n mod k by A7,Lm6;
A13: k > 0 by A7;
n mod k in NAT by INT_1:3;
then reconsider i = n mod k as Nat;
assume
A14: not k divides m;
A15: now
assume i = 0;
then n - (n div k) * k = 0 by A7,INT_1:def 10;
then k divides n;
hence contradiction by A9,A14,Lm3;
end;
a divides n by A9,A10,Lm3;
then a divides n mod k by A7,Lm6;
hence contradiction by A8,A13,A12,A15,INT_1:58;
end;
end;
uniqueness
proof
let IT1,IT2 be Nat;
assume a divides IT1 & b divides IT1 &
( for m being Integer st a divides m & b divides m holds IT1 divides m) &
a divides IT2 & ( b divides IT2 &
for m being Integer st a divides m & b divides m holds IT2 divides m );
then IT1 divides IT2 & IT2 divides IT1;
hence thesis by Lm8;
end;
commutativity;
end;
theorem Th4:
a = 0 or b = 0 iff a lcm b = 0
proof
A1: b = 0 implies (a lcm b) = 0
proof
assume b = 0;
then 0 divides (a lcm b) by Def1;
hence thesis;
end;
A2: (a lcm b) = 0 implies a = 0 or b = 0
proof
A3: b divides b implies b divides b*a;
assume
A4: a lcm b = 0;
a divides a implies a divides a*b;
then 0 divides a*b by A4,A3,Def1;
hence thesis by XCMPLX_1:6;
end;
a = 0 implies a lcm b = 0
proof
assume a = 0;
then 0 divides (a lcm b) by Def1;
hence thesis;
end;
hence thesis by A1,A2;
end;
Lm9: 0 < j & i divides j implies i <= j
proof
assume that
A1: 0 < j and
A2: i divides j;
consider l such that
A3: j = i * l by A2,Lm7;
l <> 0 by A1,A3;
then consider k such that
A4: l = k + 1 by NAT_1:6;
i * (k + 1) = i + i * k;
hence thesis by A3,A4,NAT_1:11;
end;
definition
let a,b be Integer;
func a gcd b -> Nat means
:Def2:
it divides a & it divides b &
for m being Integer st m divides a & m divides b holds m divides it;
existence
proof
per cases;
suppose
A1: a = 0;
b in INT by INT_1:def 2;
then consider k being Nat such that
A2: b = k or b = -k by INT_1:def 1;
take k;
thus k divides a & k divides b by A1,A2,Lm4,Lm5;
let m be Integer;
assume that
m divides a and
A3: m divides b;
thus thesis by A2,A3,Lm3;
end;
suppose
A4: b = 0;
a in INT by INT_1:def 2;
then consider k being Nat such that
A5: a = k or a = -k by INT_1:def 1;
take k;
thus k divides a & k divides b by A4,A5,Lm4,Lm5;
let m be Integer;
assume that
A6: m divides a and
m divides b;
thus thesis by A5,A6,Lm3;
end;
suppose
A7: a <> 0 & b <> 0;
defpred P[Nat] means $1 divides a & $1 divides b & $1 <> 0;
A8: a divides a*b;
a*b in INT by INT_1:def 2;
then consider k being Nat such that
A9: a*b = k or a*b = -k by INT_1:def 1;
k <> 0 by A7,A9,XCMPLX_1:6;
then
A10: k > 0;
A11: for i being Nat st P[i] holds i <= k
proof
let i be Nat;
assume P[i];
then i divides a*b by A8,Lm2;
hence thesis by A9,Lm3,A10,Lm9;
end;
1 divides a & 1 divides b by Lm5;
then
A12: ex k being Nat st P[k];
consider k being Nat such that
A13: P[k] and
A14: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A11,A12);
take k;
thus k divides a & k divides b by A13;
let m be Integer;
assume that
A15: m divides a and
A16: m divides b;
m in INT by INT_1:def 2;
then consider n being Nat such that
A17: m = n or m = - n by INT_1:def 1;
set i = n lcm k;
A18: k divides i by Def1;
now
assume i = 0;
then n = 0 or k = 0 by Th4;
hence contradiction by A7,A13,A17,A15;
end;
then 0 < i;
then
A19: k <= i by A18,Lm9;
n divides b by A17,A16,Lm4;
then
A20: n lcm k divides b by A13,Def1;
n divides a by A17,A15,Lm4;
then n lcm k divides a by A13,Def1;
then k >= n lcm k by A14,A20;
then k = i by A19,XXREAL_0:1;
then
A21: n divides k by Def1;
assume not m divides k;
hence contradiction by A17,A21,Lm4;
end;
end;
uniqueness
proof
let IT1,IT2 be Nat;
assume IT1 divides a & IT1 divides b &
( for m being Integer st m divides a & m divides b holds m divides IT1)
& IT2 divides a & (
IT2 divides b & for m being Integer st m divides a & m divides b holds
m divides IT2 );
then IT1 divides IT2 & IT2 divides IT1;
hence thesis by Lm8;
end;
commutativity;
end;
theorem Th5:
a = 0 & b = 0 iff a gcd b = 0
proof
0 divides 0 gcd 0 by Def2;
hence a = 0 & b = 0 implies a gcd b = 0;
assume a gcd b = 0;
then 0 divides a & 0 divides b by Def2;
hence thesis;
end;
reserve n for Nat;
reserve a,b,c,d,a1,b1,a2,b2,k,l for Integer;
theorem Th6:
-n is Element of NAT iff n = 0
proof
thus -n is Element of NAT implies n = 0
proof
assume -n is Element of NAT;
then -n>=0 & n+(-n)>=0+n;
hence thesis;
end;
thus thesis;
end;
registration
let n be non zero Nat;
cluster -n -> non natural;
coherence
proof
not -n is Element of NAT by Th6;
hence thesis by ORDINAL1:def 12;
end;
end;
theorem
not -1 is Element of NAT;
theorem
a divides -a & -a divides a by Lm1;
theorem
a divides b & b divides c implies a divides c by Lm2;
theorem Th10:
(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)
proof
A1: a divides b implies a divides -b
proof
assume
A2: a divides b;
b divides -b by Lm1;
hence thesis by A2,Lm2;
end;
A3: a divides -b implies a divides b
proof
assume
A4: a divides -b;
-b divides b by Lm1;
hence thesis by A4,Lm2;
end;
hence a divides b iff a divides -b by A1;
A5: -a divides b implies a divides b
proof
assume
A6: -a divides b;
a divides -a by Lm1;
hence thesis by A6,Lm2;
end;
A7: -a divides -b implies a divides b
proof
assume
A8: -a divides -b;
-b divides b by Lm1;
hence thesis by A5,A8,Lm2;
end;
A9: a divides b implies -a divides b
proof
assume
A10: a divides b;
-a divides a by Lm1;
hence thesis by A10,Lm2;
end;
hence a divides b iff -a divides b by A5;
a divides b implies -a divides -b
proof
assume
A11: a divides b;
-a divides a by Lm1;
hence thesis by A1,A11,Lm2;
end;
hence a divides b iff -a divides -b by A7;
thus thesis by A1,A3,A9,A5;
end;
theorem
a divides b & b divides a implies a = b or a = -b
proof
assume that
A1: a divides b and
A2: b divides a;
consider a1 such that
A3: b = a*a1 by A1;
consider b1 such that
A4: a = b*b1 by A2;
a<>0 implies a = b or a = -b
proof
assume
A5: a<>0;
1*a = a*(a1*b1) by A3,A4;
then a1*b1 = 1 by A5,XCMPLX_1:5;
then a = b*1 or a = b*(-1) by A4,INT_1:9;
hence thesis;
end;
hence thesis by A1;
end;
theorem
a divides 0 & 1 divides a & -1 divides a by Lm5;
theorem
a divides 1 or a divides -1 implies a = 1 or a = -1 by INT_1:9,10;
theorem
a = 1 or a = -1 implies a divides 1 & a divides -1 by Lm5;
theorem
a,b are_congruent_mod c iff c divides a-b;
theorem
a divides b iff |.a.| divides |.b.|
proof
thus a divides b implies |.a.| divides |.b.|
proof
assume a divides b;
then consider c such that
A1: b = a*c;
|.b.| = |.a.|*|.c.| by A1,COMPLEX1:65;
hence thesis;
end;
assume |.a.| divides |.b.|;
then consider m being Integer such that
A2: |.b.| = |.a.|*m;
A3: a>=0 implies a divides b
proof
assume a>=0;
then
A4: |.b.| = a*m by A2,ABSVALUE:def 1;
per cases;
suppose b<0;
then -b = a*m by A4,ABSVALUE:def 1;
then b = a*(-m);
hence thesis;
end;
suppose b>=0;
then b = a*m by A4,ABSVALUE:def 1;
hence thesis;
end;
end;
a<0 implies a divides b
proof
assume a<0;
then
A5: |.b.| = (-a)*m by A2,ABSVALUE:def 1;
per cases;
suppose b<0;
then -b = -(a*m) by A5,ABSVALUE:def 1;
hence thesis;
end;
suppose b>=0;
then b = a*(-m) by A5,ABSVALUE:def 1;
hence thesis;
end;
end;
hence thesis by A3;
end;
theorem
a lcm b is Element of NAT by ORDINAL1:def 12;
theorem
a divides a lcm b by Def1;
theorem
for c st a divides c & b divides c holds a lcm b divides c by Def1;
theorem
a gcd b is Element of NAT by ORDINAL1:def 12;
theorem Th21:
a gcd b divides a by Def2;
theorem
for c st c divides a & c divides b holds c divides a gcd b by Def2;
:: Relative Prime Numbers
definition
let a,b be Integer;
pred a,b are_coprime means
a gcd b = 1;
symmetry;
end;
theorem
a <> 0 or b <> 0 implies
ex a1,b1 st a = (a gcd b)*a1 & b = (a gcd b)*b1 & a1,b1 are_coprime
proof
assume a<>0 or b<>0;
then
A1: a gcd b <>0 by Th5;
(a gcd b) divides a by Def2;
then consider a1 such that
A2: a = (a gcd b)*a1;
a gcd b divides b by Def2;
then consider b1 such that
A3: b = (a gcd b)*b1;
a1 gcd b1 divides b1 by Def2;
then consider b2 such that
A4: b1 = (a1 gcd b1)*b2;
b = ((a gcd b)*(a1 gcd b1))*b2 by A3,A4;
then
A5: (a gcd b)*(a1 gcd b1) divides b;
(a1 gcd b1) divides a1 by Def2;
then consider a2 such that
A6: a1 = (a1 gcd b1)*a2;
a = ((a gcd b)*(a1 gcd b1))*a2 by A2,A6;
then (a gcd b)*(a1 gcd b1) divides a;
then (a gcd b)*(a1 gcd b1) divides (a gcd b) by A5,Def2;
then consider c such that
A7: a gcd b = ((a gcd b)*(a1 gcd b1))*c;
(a gcd b)*1 = (a gcd b)*((a1 gcd b1)*c) by A7;
then 1 = (a1 gcd b1)*c by A1,XCMPLX_1:5;
then a1,b1 are_coprime by INT_1:9;
hence thesis by A2,A3;
end;
theorem Th24:
a,b are_coprime implies c*a gcd c*b = |.c.|
proof
assume
A1: a,b are_coprime;
(c*a gcd c*b) divides c*b by Def2;
then consider l such that
A3: c*b = (c*a gcd c*b)*l;
(c*a gcd c*b) divides c*a by Def2;
then consider k such that
A4: c*a = (c*a gcd c*b)*k;
c divides c*a & c divides c*b;
then c divides (c*a gcd c*b) by Def2;
then consider d such that
A5: c*a gcd c*b = c*d;
A6: c*b = c*(d*l) by A5,A3;
A7: c*a = c*(d*k) by A5,A4;
A8: c <>0 implies c*a gcd c*b = |.c.|
proof
assume
A9: c <>0;
then
A10: d divides b by A6,XCMPLX_1:5;
d divides a by A7,A9,XCMPLX_1:5;
then d divides 1 by A1,A10,Def2;
then c*a gcd c*b = c*1 or c*a gcd c*b = c*(-1) by A5,INT_1:9;
then c*a gcd c*b = c*1 or c*a gcd c*b = (-c)*1;
then |.c*a gcd c*b.| = |.c.| by COMPLEX1:52;
hence thesis by ABSVALUE:def 1;
end;
0*a gcd 0*b = 0 by Th5
.= |.0.| by ABSVALUE:2;
hence thesis by A8;
end;
theorem Th25:
c divides a*b & a,c are_coprime implies c divides b
proof
assume that
A1: c divides a*b and
A2: a,c are_coprime;
c divides c*b;
then
A3: c divides (a*b gcd c*b) by A1,Def2;
A4: a*b gcd c*b = |.b.| by A2,Th24;
b<0 implies c divides b
proof
assume b<0;
then c divides (-b) by A4,A3,ABSVALUE:def 1;
hence thesis by Th10;
end;
hence thesis by A4,A3,ABSVALUE:def 1;
end;
theorem
a,c are_coprime & b,c are_coprime implies a*b,c are_coprime
proof
assume that
A1: a,c are_coprime and
A2: b,c are_coprime;
A4: ((a*b gcd c) gcd a) divides a by Def2;
A5: (a*b gcd c) divides c by Def2;
((a*b gcd c) gcd a) divides (a*b gcd c) by Def2;
then ((a*b gcd c) gcd a) divides c by A5,Lm2;
then ((a*b gcd c) gcd a) divides 1 by A1,A4,Def2;
then a,(a*b gcd c) are_coprime by INT_1:9;
then (a*b gcd c) divides b by Th21,Th25;
then (a*b gcd c) divides 1 by A2,A5,Def2;
hence thesis by INT_1:9;
end;
::***************************************************************************::
:: PRIME NUMBERS ::
::***************************************************************************::
reserve p,p1,q,l for Nat;
definition
let p be Integer;
attr p is prime means
p > 1 & for n being Nat st n divides p holds n = 1 or n = p;
end;
registration
cluster prime -> natural for Integer;
coherence
proof
let p be Integer;
assume p is prime; then
p in NAT by INT_1:3;
hence thesis;
end;
end;
theorem Th27:
0 < b & a divides b implies a <= b
proof
assume
A1: 0 < b;
assume a divides b;
then consider c such that
A2: b = a * c;
per cases;
suppose
a <= 0;
hence thesis by A1;
end;
suppose
A3: a > 0;
then c > 0 by A1,A2;
then c >= 0+1 by INT_1:7;
hence thesis by A2,A3,XREAL_1:151;
end;
end;
theorem Th28:
2 is prime
proof
thus 2>1;
let n be Nat;
assume
A1: n divides 2;
then n <= 2 by Th27;
then n = 0 or ... or n = 2;
hence thesis by A1;
end;
theorem Th29:
not 4 is prime
proof
ex n st n divides 4 & n<>1 & n<>4
proof
take 2;
4 = 2*2;
hence thesis;
end;
hence thesis;
end;
registration
cluster prime for Nat;
existence by Th28;
cluster non zero non prime for Nat;
existence by Th29;
end;
definition
mode Prime is prime Nat;
end;
theorem
p is prime & q is prime implies p,q are_coprime or p = q
proof
assume that
A1: p is prime and
A2: q is prime;
A3: (p gcd q) divides q by Def2;
assume
A4: not p,q are_coprime;
(p gcd q) divides p by Def2;
then p gcd q = p by A1,A4;
hence thesis by A2,A4,A3;
end;
theorem
for n being Nat holds
n >= 2 implies ex p being Element of NAT st p is prime & p divides n
proof
defpred P[Nat] means ex p st p is prime & p divides $1;
A1: for k being Nat st k>=2 holds (for n being Nat st n>=2 holds n<k implies
P[n]) implies P[k]
proof
let k be Nat;
assume
A2: k>=2;
assume
A3: for n being Nat st n>=2 holds n<k implies ex p st p is prime & p divides n;
A4: k+1-1>1+1-1 by A2,NAT_1:13;
not k is prime implies ex p being Element of NAT st p is prime & p
divides k
proof
assume not k is prime;
then consider m being Nat such that
A5: m divides k and
A6: m<>1 and
A7: m<>k by A4;
m<>0 by A5,A7;
then m>0;
then m>=0+1 by NAT_1:13;
then m>1 by A6,XXREAL_0:1;
then
A8: m>=1+1 by NAT_1:13;
m<=k by A2,A5,Th27;
then m<k by A7,XXREAL_0:1;
then consider p1 such that
A9: p1 is prime & p1 divides m by A3,A8;
reconsider p1 as Element of NAT by ORDINAL1:def 12;
take p1;
thus thesis by A5,A9,Lm2;
end;
hence thesis;
end;
A10: for k being Nat st k>=2 holds P[k] from NAT_1:sch 9(A1);
let n be Nat;
assume n >= 2;
then consider p such that
A11: p is prime & p divides n by A10;
reconsider p as Element of NAT by ORDINAL1:def 12;
take p;
thus thesis by A11;
end;
begin :: Addenda
:: from AMI_4, 2007.06.14, A.T.
theorem
for i,j being Integer st i >= 0 & j >= 0 holds
|.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j
proof
let i,j be Integer;
assume i >= 0 & j >= 0;
then |.i.| = i & |.j.| = j by ABSVALUE:def 1;
hence thesis;
end;
:: old definitions, 2007.11.07, A.T
theorem
a lcm b = |.a.| lcm |.b.|
proof
A1: |.b.| = b or |.b.| = -b by ABSVALUE:1;
A2: |.a.| = a or |.a.| = -a by ABSVALUE:1;
A3: now
let m be Integer;
assume |.a.| divides m & |.b.| divides m;
then a divides m & b divides m by A2,A1,Th10;
hence a lcm b divides m by Def1;
end;
b divides a lcm b by Def1;
then
A4: |.b.| divides a lcm b by A1,Th10;
a divides a lcm b by Def1;
then |.a.| divides a lcm b by A2,Th10;
hence thesis by A4,A3,Def1;
end;
theorem
a gcd b = |.a.| gcd |.b.|
proof
A1: |.b.| = b or |.b.| = -b by ABSVALUE:1;
A2: |.a.| = a or |.a.| = -a by ABSVALUE:1;
A3: now
let m be Integer;
assume m divides |.a.| & m divides |.b.|;
then m divides a & m divides b by A2,A1,Th10;
hence m divides a gcd b by Def2;
end;
a gcd b divides b by Def2;
then
A4: a gcd b divides |.b.| by A1,Th10;
a gcd b divides a by Def2;
then a gcd b divides |.a.| by A2,Th10;
hence thesis by A4,A3,Def2;
end;