let i1, i2, i3 be Integer; :: thesis: ( i1,i2 are_congruent_mod i3 implies i1 gcd i3 = i2 gcd i3 )
set d = i2 gcd i3;
reconsider d = i2 gcd i3 as Nat ;
assume i1,i2 are_congruent_mod i3 ; :: thesis: i1 gcd i3 = i2 gcd i3
then i3 divides i1 - i2 ;
then consider i being Integer such that
A1: i1 - i2 = i3 * i ;
A2: d = |.i2.| gcd |.i3.| by INT_2:34;
then d divides |.i2.| by NAT_D:def 5;
then |.d.| divides |.i2.| by ABSVALUE:def 1;
then A3: d divides i2 by INT_2:16;
A4: i2 = i1 - (i3 * i) by A1;
A5: for n being Nat st n divides |.i1.| & n divides |.i3.| holds
n divides d
proof
let n be Nat; :: thesis: ( n divides |.i1.| & n divides |.i3.| implies n divides d )
assume that
A6: n divides |.i1.| and
A7: n divides |.i3.| ; :: thesis: n divides d
|.n.| divides |.i3.| by A7, ABSVALUE:def 1;
then n divides i3 by INT_2:16;
then A8: n divides i3 * i by INT_2:2;
|.n.| divides |.i1.| by A6, ABSVALUE:def 1;
then n divides i1 by INT_2:16;
then n divides i2 by A4, A8, Lm4;
then |.n.| divides |.i2.| by INT_2:16;
then n divides |.i2.| by ABSVALUE:def 1;
hence n divides d by A2, A7, NAT_D:def 5; :: thesis: verum
end;
A9: d divides |.i3.| by A2, NAT_D:def 5;
then |.d.| divides |.i3.| by ABSVALUE:def 1;
then d divides i3 by INT_2:16;
then A10: d divides i3 * i by INT_2:2;
i1 = (i3 * i) + i2 by A1;
then ( |.d.| = d & d divides i1 ) by A3, A10, ABSVALUE:def 1, Th4;
then d divides |.i1.| by INT_2:16;
then |.i1.| gcd |.i3.| = d by A9, A5, NAT_D:def 5;
hence i1 gcd i3 = i2 gcd i3 by INT_2:34; :: thesis: verum