let a, b, c be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

assume that

A1: a <> 0 and

A2: c <> 0 and

A3: a,c are_coprime and

A4: b,c are_coprime ; :: thesis: 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; :: thesis: verum