let i1, i2, i3 be Integer; ( 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
; 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
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; verum