let a, b, m be Nat; ( 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 that
A1:
a <> 0
and
A2:
b <> 0
and
A3:
m <> 0
and
A4:
( a,m are_relative_prime & b,m are_relative_prime )
; m,(a * b) mod m are_relative_prime
a * b,m are_relative_prime
by A1, A3, A4, EULER_1:15;
then A5:
(a * b) gcd m = 1
by INT_2:def 4;
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, XCMPLX_1:5;
then
((a * b) + ((- t) * m)) gcd m = (a * b) gcd m
by EULER_1:17;
hence
m,(a * b) mod m are_relative_prime
by A6, A5, INT_2:def 4; verum