let a, b, m be Nat; :: thesis: ( a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime implies m,(a * b) mod m are_relative_prime )
assume A1: ( a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime ) ; :: thesis: m,(a * b) mod m are_relative_prime
then A2: a * b,m are_relative_prime by EULER_1:15;
consider t being Nat such that
A3: a * b = (m * t) + ((a * b) mod m) and
(a * b) mod m < m by A1, NAT_D:def 2;
a * b <> a * 0 by A1, XCMPLX_1:5;
then A4: ((a * b) + ((- t) * m)) gcd m = (a * b) gcd m by A1, EULER_1:17;
(a * b) gcd m = 1 by A2, INT_2:def 4;
hence m,(a * b) mod m are_relative_prime by A3, A4, INT_2:def 4; :: thesis: verum