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