let x, y, n be Integer; :: thesis: ( x,n are_coprime & x,y are_congruent_mod n implies y,n are_coprime )

assume that

A1: x,n are_coprime and

A2: x,y are_congruent_mod n and

A3: not y,n are_coprime ; :: thesis: contradiction

consider z being Integer such that

A4: n * z = x - y by A2, INT_1:def 5;

set gcdyn = y gcd n;

A5: y gcd n divides y by INT_2:21;

A6: y gcd n divides n by INT_2:21;

y gcd n divides n * z by INT_2:2, INT_2:21;

then y gcd n divides (n * z) + y by A5, WSIERP_1:4;

then y gcd n divides x gcd n by A4, A6, INT_2:22;

then y gcd n divides 1 by A1, INT_2:def 3;

then A7: ( y gcd n = 1 or y gcd n = - 1 ) by INT_2:13;

0 <= y gcd n ;

hence contradiction by A3, A7, INT_2:def 3; :: thesis: verum

assume that

A1: x,n are_coprime and

A2: x,y are_congruent_mod n and

A3: not y,n are_coprime ; :: thesis: contradiction

consider z being Integer such that

A4: n * z = x - y by A2, INT_1:def 5;

set gcdyn = y gcd n;

A5: y gcd n divides y by INT_2:21;

A6: y gcd n divides n by INT_2:21;

y gcd n divides n * z by INT_2:2, INT_2:21;

then y gcd n divides (n * z) + y by A5, WSIERP_1:4;

then y gcd n divides x gcd n by A4, A6, INT_2:22;

then y gcd n divides 1 by A1, INT_2:def 3;

then A7: ( y gcd n = 1 or y gcd n = - 1 ) by INT_2:13;

0 <= y gcd n ;

hence contradiction by A3, A7, INT_2:def 3; :: thesis: verum