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

now

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 ( abs m = m & abs 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 abs 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 abs 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 ( abs m = - m & abs 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