let a, b be Nat; :: thesis: ( a <> 0 & b <> 0 implies ex c, d being Nat st a gcd b = (a * c) - (b * d) )
assume that
A1: a <> 0 and
A2: b <> 0 ; :: thesis: ex c, d being Nat st a gcd b = (a * c) - (b * d)
consider m, n being Integer such that
A3: a gcd b = (a * m) + (b * n) by Th34;
set k = [/(max (- (m / b)),(n / a))\] + 1;
[/(max (- (m / b)),(n / a))\] + 1 > n / a by INT_1:57, XXREAL_0:31;
then ([/(max (- (m / b)),(n / a))\] + 1) * a > n by A1, XREAL_1:79;
then A4: (([/(max (- (m / b)),(n / a))\] + 1) * a) - n > 0 by XREAL_1:52;
[/(max (- (m / b)),(n / a))\] + 1 > - (m / b) by INT_1:57, XXREAL_0:31;
then [/(max (- (m / b)),(n / a))\] + 1 > (- m) / b by XCMPLX_1:188;
then ([/(max (- (m / b)),(n / a))\] + 1) * b > - m by A2, XREAL_1:79;
then (([/(max (- (m / b)),(n / a))\] + 1) * b) - (- m) > 0 by XREAL_1:52;
then reconsider e = (([/(max (- (m / b)),(n / a))\] + 1) * b) + m, d = (([/(max (- (m / b)),(n / a))\] + 1) * a) - n as Element of NAT by A4, INT_1:16;
(a * e) - (b * d) = ((a * m) + 0 ) + (b * n) ;
hence ex c, d being Nat st a gcd b = (a * c) - (b * d) by A3; :: thesis: verum