let a, b, c be Integer; :: thesis: ( 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 ) )
assume a,b are_relative_prime ; :: thesis: ( (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 )
then A1: a gcd b = 1 by Def4;
thus A2: (c * a) gcd (c * b) = abs c :: thesis: ( (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c )

proof

(c * a) gcd (c * b) divides c * b by Def3;
then consider l being Integer such that
A3: c * b = ((c * a) gcd (c * b)) * l by INT_1:def 9;
(c * a) gcd (c * b) divides c * a by Def3;
then consider k being Integer such that
A4: c * a = ((c * a) gcd (c * b)) * k by INT_1:def 9;
( c divides c * a & c divides c * b ) by Th2;
then c divides (c * a) gcd (c * b) by Def3;
then consider d being Integer such that
A5: (c * a) gcd (c * b) = c * d by INT_1:def 9;
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) = abs c )

proof

assume A9: c <> 0 ; :: thesis: (c * a) gcd (c * b) = abs c
then b = d * l by A6, XCMPLX_1:5;
then A10: d divides b by INT_1:def 9;
a = d * k by A7, A9, XCMPLX_1:5;
then d divides a by INT_1:def 9;
then d divides 1 by A1, A10, Def3;
then ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = c * (- 1) ) by A5, Th17;
then ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = (- c) * 1 ) ;
then A11: abs ((c * a) gcd (c * b)) = abs c by COMPLEX1:138;
(c * a) gcd (c * b) >= 0 by NAT_1:2;
hence (c * a) gcd (c * b) = abs c by A11, ABSVALUE:def 1; :: thesis: verum

end;

(0 * a) gcd (0 * b) = 0 by Th5
.= abs 0 by ABSVALUE:7 ;
hence (c * a) gcd (c * b) = abs c by A8; :: thesis: verum

end;

hence (c * a) gcd (b * c) = abs c ; :: thesis: ( (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c )
thus ( (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) by A2; :: thesis: verum