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.| )

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

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

hence
(c * a) gcd (b * c) = |.c.|
; :: thesis: ( (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.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.| )

.= |.0.| by ABSVALUE:2 ;

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

end;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

(0 * a) gcd (0 * b) =
0
by Th5
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;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

.= |.0.| by ABSVALUE:2 ;

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

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