let a, b, c be Nat; ( a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime implies a * b,c are_coprime )
assume that
A1:
a <> 0
and
A2:
c <> 0
and
A3:
a,c are_coprime
and
A4:
b,c are_coprime
; a * b,c are_coprime
A5:
a gcd c = 1
by A3, INT_2:def 3;
A6:
(a * b) gcd c divides c
by NAT_D:def 5;
((a * b) gcd c) gcd a divides (a * b) gcd c
by NAT_D:def 5;
then
( ((a * b) gcd c) gcd a divides a & ((a * b) gcd c) gcd a divides c )
by A6, NAT_D:4, NAT_D:def 5;
then
((a * b) gcd c) gcd a divides 1
by A5, NEWTON:50;
then A7:
((a * b) gcd c) gcd a <= 0 + 1
by NAT_D:7;
((a * b) gcd c) gcd a <> 0
by A1, NEWTON:58;
then
((a * b) gcd c) gcd a = 1
by A7, NAT_1:9;
then
( (a * b) gcd c divides a * b & a,(a * b) gcd c are_coprime )
by INT_2:def 3, NAT_D:def 5;
then A8:
(a * b) gcd c divides b
by Th13;
b gcd c = 1
by A4, INT_2:def 3;
then
(a * b) gcd c divides 1
by A6, A8, NEWTON:50;
then A9:
(a * b) gcd c <= 0 + 1
by NAT_D:7;
(a * b) gcd c > 0
by A2, NEWTON:58;
then
(a * b) gcd c = 1
by A9, NAT_1:9;
hence
a * b,c are_coprime
by INT_2:def 3; verum