let IT be Nat; :: thesis: ( IT = k gcd n iff ( IT divides k & IT divides n & ( for m being Nat st m divides k & m divides n holds
m divides IT ) ) )
thus ( IT = k gcd n implies ( IT divides k & IT divides n & ( for m being Nat st m divides k & m divides n holds
m divides IT ) ) ) by INT_2:def 2; :: thesis: ( IT divides k & IT divides n & ( for m being Nat st m divides k & m divides n holds
m divides IT ) implies IT = k gcd n )
assume that
A1: IT divides k and
A2: IT divides n and
A3: for m being Nat st m divides k & m divides n holds
m divides IT ; :: thesis: IT = k gcd n
for m being Integer st m divides k & m divides n holds
m divides IT

proof

let m be Integer; :: thesis: ( m divides k & m divides n implies m divides IT )
m in INT by INT_1:def 2;
then consider i being Nat such that
A4: ( m = i or m = - i ) by INT_1:def 1;
assume that
A5: m divides k and
A6: m divides n ; :: thesis: m divides IT
A7: i divides k by A4, A5, INT_2:10;
i divides n by A4, A6, INT_2:10;
then i divides IT by A3, A7;
hence m divides IT by A4, INT_2:10; :: thesis: verum

end;

hence IT = k gcd n by A1, A2, INT_2:def 2; :: thesis: verum