let m, n be Integer; :: thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
m gcd n = |.m.| gcd |.n.| by INT_2:34;
then consider m1, n1 being Integer such that
A1: (|.m.| * m1) + (|.n.| * n1) = m gcd n by Th27;

now :: thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)

per cases ( ( m >= 0 & n >= 0 ) or ( m >= 0 & n < 0 ) or ( m < 0 & n >= 0 ) or ( m < 0 & n < 0 ) ) ;

suppose ( m >= 0 & n >= 0 ) ; :: thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)

then ( |.m.| = m & |.n.| = n ) by ABSVALUE:def 1;
hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) by A1; :: thesis: verum

end;

suppose A2: ( m >= 0 & n < 0 ) ; :: thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)

then |.n.| = - n by ABSVALUE:def 1;
then m gcd n = (m * m1) + (n * (- n1)) by A1, A2, ABSVALUE:def 1;
hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; :: thesis: verum

end;

suppose A3: ( m < 0 & n >= 0 ) ; :: thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)

then |.m.| = - m by ABSVALUE:def 1;
then m gcd n = (m * (- m1)) + (n * n1) by A1, A3, ABSVALUE:def 1;
hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; :: thesis: verum

end;

suppose ( m < 0 & n < 0 ) ; :: thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)

then ( |.m.| = - m & |.n.| = - n ) by ABSVALUE:def 1;
then m gcd n = (m * (- m1)) + (n * (- n1)) by A1;
hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; :: thesis: verum

end;

end;

end;

hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; :: thesis: verum