let a, b be Nat; 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)
now 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 A3:
(
a <> 0 &
b <> 0 )
;
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 not f <> 0 assume A10:
f <> 0
;
contradictionf =
a - (d * e)
by A6
.=
(a * (1 - (m * e))) + (b * (- (n * e)))
by A8
;
hence
contradiction
by A5, A7, A10;
verum end; consider e,
f being
Nat such that A11:
b = (d * e) + f
and A12:
f < d
by A5, NAT_1:17;
now not f <> 0 assume A13:
f <> 0
;
contradictionf =
b - (d * e)
by A11
.=
(b * (1 - (n * e))) + (a * (- (m * e)))
by A8
;
hence
contradiction
by A5, A12, A13;
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;
verum end; end; end;
hence
ex m, n being Integer st a gcd b = (a * m) + (b * n)
; verum