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 Th27;
set k = [/(max ((- (m / b)),(n / a)))\] + 1;
[/(max ((- (m / b)),(n / a)))\] + 1 > n / a by INT_1:32, XXREAL_0:31;
then ([/(max ((- (m / b)),(n / a)))\] + 1) * a > n by A1, XREAL_1:77;
then A4: (([/(max ((- (m / b)),(n / a)))\] + 1) * a) - n > 0 by XREAL_1:50;
[/(max ((- (m / b)),(n / a)))\] + 1 > - (m / b) by INT_1:32, XXREAL_0:31;
then [/(max ((- (m / b)),(n / a)))\] + 1 > (- m) / b by XCMPLX_1:187;
then ([/(max ((- (m / b)),(n / a)))\] + 1) * b > - m by A2, XREAL_1:77;
then (([/(max ((- (m / b)),(n / a)))\] + 1) * b) - (- m) > 0 by XREAL_1:50;
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:3;
(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