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:65; :: thesis: verum

end;

now

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 consider m, n being Integer such that
A3: a gcd b = (0 * m) + (a * n) by A1;
thus ex m, n being Integer st a gcd b = (a * m) + (b * n) by A2, A3; :: thesis: verum

end;

suppose S: ( 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 A5: ex c being Nat st S₁[c] by S;
consider d being Nat such that
A6: ( S₁[d] & ( for c being Nat st S₁[c] holds
d <= c ) ) from NAT_1:sch 5(A5);
consider m, n being Integer such that
A8: d = (a * m) + (b * n) by A6;
consider e, f being Nat such that
A9: ( a = (d * e) + f & f < d ) by A6, NAT_1:17;

now

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

end;

then A11: d divides a by A9, NAT_D:def 3;
consider e, f being Nat such that
A12: ( b = (d * e) + f & f < d ) by A6, NAT_1:17;

now

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

end;

then d divides b by A12, NAT_D:def 3;
then A14: d divides a gcd b by A11, 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, Th10;
hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A8, A14, NAT_D:5; :: thesis: verum

end;

end;

end;

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