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 S1[ 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 S1[c] by A3;
consider d being Nat such that
A5: ( S1[d] & ( for c being Nat st S1[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