let a, b, m be Nat; :: thesis: ( a <> 0 & b <> 0 & m <> 0 & a,m are_coprime & b,m are_coprime implies m,(a * b) mod m are_coprime )
assume that
A1: a <> 0 and
A2: b <> 0 and
A3: m <> 0 and
A4: ( a,m are_coprime & b,m are_coprime ) ; :: thesis: m,(a * b) mod m are_coprime
a * b,m are_coprime by A1, A3, A4, EULER_1:14;
then A5: (a * b) gcd m = 1 ;
consider t being Nat such that
A6: a * b = (m * t) + ((a * b) mod m) and
(a * b) mod m < m by A3, NAT_D:def 2;
a * b <> a * 0 by A1, A2;
then ((a * b) + ((- t) * m)) gcd m = (a * b) gcd m by EULER_1:16;
hence m,(a * b) mod m are_coprime by A6, A5; :: thesis: verum