let a, b, c be Integer; ( a,c are_coprime & b,c are_coprime implies a * b,c are_coprime )
assume that
A1:
a,c are_coprime
and
A2:
b,c are_coprime
; a * b,c are_coprime
A3:
a gcd c = 1
by A1;
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 A3, A4, Def2;
then
( ((a * b) gcd c) gcd a = 1 or ((a * b) gcd c) gcd a = - 1 )
by Th13;
then
a,(a * b) gcd c are_coprime
;
then A6:
(a * b) gcd c divides b
by Th21, Th25;
b gcd c = 1
by A2;
then
(a * b) gcd c divides 1
by A5, A6, Def2;
then
( (a * b) gcd c = 1 or (a * b) gcd c = - 1 )
by Th13;
hence
a * b,c are_coprime
; verum