let a, b, c be Integer; :: thesis: ( a,b are_coprime implies (c * a) gcd (c * b) = |.c.| )
assume A1: a,b are_coprime ; :: thesis: (c * a) gcd (c * b) = |.c.|
(c * a) gcd (c * b) divides c * b by Def2;
then consider l being Integer such that
A3: c * b = ((c * a) gcd (c * b)) * l ;
(c * a) gcd (c * b) divides c * a by Def2;
then consider k being Integer 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 being Integer 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 ; :: thesis: (c * a) gcd (c * b) = |.c.|
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 (c * a) gcd (c * b) = |.c.| by ABSVALUE:def 1; :: thesis: verum

end;

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