let a, b, c be Integer; :: thesis: ( a,b are_coprime implies ( (c * a) gcd (c * b) = |.c.| & (c * a) gcd (b * c) = |.c.| & (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| ) )
assume a,b are_coprime ; :: thesis: ( (c * a) gcd (c * b) = |.c.| & (c * a) gcd (b * c) = |.c.| & (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| )
then A1: a gcd b = 1 ;
thus A2: (c * a) gcd (c * b) = |.c.| :: thesis: ( (c * a) gcd (b * c) = |.c.| & (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| )
proof
(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 b = d * l by A6, XCMPLX_1:5;
then A10: d divides b ;
a = d * k by A7, A9, XCMPLX_1:5;
then d divides a ;
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, Th13;
then ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = (- c) * 1 ) ;
then A11: |.((c * a) gcd (c * b)).| = |.c.| by COMPLEX1:52;
thus (c * a) gcd (c * b) = |.c.| by A11, 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
end;
hence (c * a) gcd (b * c) = |.c.| ; :: thesis: ( (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| )
thus ( (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| ) by A2; :: thesis: verum