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 A1: ( a <> 0 & b <> 0 ) ; :: thesis: ex c, d being Nat st a gcd b = (a * c) - (b * d)
consider m, n being Integer such that
A2: a gcd b = (a * m) + (b * n) by Th34;
set k = [/(max (- (m / b)),(n / a))\] + 1;
( [/(max (- (m / b)),(n / a))\] + 1 > - (m / b) & [/(max (- (m / b)),(n / a))\] + 1 > n / a ) by INT_1:57, XXREAL_0:31;
then ( [/(max (- (m / b)),(n / a))\] + 1 > (- m) / b & [/(max (- (m / b)),(n / a))\] + 1 > n / a ) by XCMPLX_1:188;
then ( ([/(max (- (m / b)),(n / a))\] + 1) * b > - m & ([/(max (- (m / b)),(n / a))\] + 1) * a > n ) by A1, XREAL_1:79;
then ( (([/(max (- (m / b)),(n / a))\] + 1) * b) - (- m) > 0 & (([/(max (- (m / b)),(n / a))\] + 1) * a) - n > 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 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 A2; :: thesis: verum