let a, b be Nat; :: thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)
A1: for c being Nat ex m, n being Integer st 0 gcd c = (0 * m) + (c * n)

proof

let c be Nat; :: thesis: ex m, n being Integer st 0 gcd c = (0 * m) + (c * n)
take 0 ; :: thesis: ex n being Integer st 0 gcd c = (0 * 0) + (c * n)
take 1 ; :: thesis: 0 gcd c = (0 * 0) + (c * 1)
thus 0 gcd c = (0 * 0) + (c * 1) by NEWTON:52; :: thesis: verum

end;

now :: thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose a = 0 ; :: thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)

hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A1; :: thesis: verum

end;

suppose A2: b = 0 ; :: thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)

then ex m, n being Integer st a gcd b = (0 * m) + (a * n) by A1;
hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A2; :: thesis: verum

end;

suppose A3: ( a <> 0 & b <> 0 ) ; :: thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)

defpred S₁[ set ] means ex m, n being Integer st
( $1 = (a * m) + (b * n) & $1 <> 0 );
a + b = (a * 1) + (b * 1) ;
then A4: ex c being Nat st S₁[c] by A3;
consider d being Nat such that
A5: ( S₁[d] & ( for c being Nat st S₁[c] holds
d <= c ) ) from NAT_1:sch 5(A4);
consider e, f being Nat such that
A6: a = (d * e) + f and
A7: f < d by A5, NAT_1:17;
consider m, n being Integer such that
A8: d = (a * m) + (b * n) by A5;

A9: now :: thesis: not f <> 0

assume A10: f <> 0 ; :: thesis: contradiction
f = a - (d * e) by A6
.= (a * (1 - (m * e))) + (b * (- (n * e))) by A8 ;
hence contradiction by A5, A7, A10; :: thesis: verum

end;

consider e, f being Nat such that
A11: b = (d * e) + f and
A12: f < d by A5, NAT_1:17;

now :: thesis: not f <> 0

assume A13: f <> 0 ; :: thesis: contradiction
f = b - (d * e) by A11
.= (b * (1 - (n * e))) + (a * (- (m * e))) by A8 ;
hence contradiction by A5, A12, A13; :: thesis: verum

end;

then A14: d divides b by A11;
d divides a by A6, A9;
then A15: d divides a gcd b by A14, NAT_D:def 5;
( a gcd b divides a & a gcd b divides b ) by NAT_D:def 5;
then a gcd b divides d by A8, Th5;
hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A8, A15, NAT_D:5; :: thesis: verum

end;

end;

end;

hence ex m, n being Integer st a gcd b = (a * m) + (b * n) ; :: thesis: verum