let a, c, b be Nat; ( a <> 0 & c <> 0 & a,c are_relative_prime & b,c are_relative_prime implies a * b,c are_relative_prime )
assume that
A1:
a <> 0
and
A2:
c <> 0
and
A3:
a,c are_relative_prime
and
A4:
b,c are_relative_prime
; a * b,c are_relative_prime
A5:
a gcd c = 1
by A3, INT_2:def 4;
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:63;
then A7:
((a * b) gcd c) gcd a <= 0 + 1
by NAT_D:7;
((a * b) gcd c) gcd a <> 0
by A1, NEWTON:71;
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_relative_prime )
by INT_2:def 4, NAT_D:def 5;
then A8:
(a * b) gcd c divides b
by Th14;
b gcd c = 1
by A4, INT_2:def 4;
then
(a * b) gcd c divides 1
by A6, A8, NEWTON:63;
then A9:
(a * b) gcd c <= 0 + 1
by NAT_D:7;
(a * b) gcd c > 0
by A2, NEWTON:71;
then
(a * b) gcd c = 1
by A9, NAT_1:9;
hence
a * b,c are_relative_prime
by INT_2:def 4; verum