let a, b be Integer; ex s, t being Integer st a gcd b = (s * a) + (t * b)
A1:
for a, b being Integer st a > 0 & b > 0 holds
ex s, t being Integer st a gcd b = (s * a) + (t * b)
proof
let a,
b be
Integer;
( a > 0 & b > 0 implies ex s, t being Integer st a gcd b = (s * a) + (t * b) )
assume that A2:
a > 0
and A3:
b > 0
;
ex s, t being Integer st a gcd b = (s * a) + (t * b)
reconsider a =
a,
b =
b as
Element of
NAT by A2, A3, INT_1:3;
set M =
{ z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } ;
defpred S1[
Nat]
means ( $1
in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } & $1
<> 0 );
a = (1 * a) + (0 * b)
;
then A4:
a in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
;
then A5:
ex
k being
Nat st
S1[
k]
by A2;
consider g being
Nat such that A6:
(
S1[
g] & ( for
n being
Nat st
S1[
n] holds
g <= n ) )
from NAT_1:sch 5(A5);
set G =
{ zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } ;
ex
z being
Element of
NAT st
(
z = g & ex
s,
t being
Integer st
z = (s * a) + (t * b) )
by A6;
then consider s,
t being
Integer such that A7:
g = (s * a) + (t * b)
;
A8:
for
x being
object st
x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } holds
x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g }
proof
let x be
object ;
( x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } implies x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } )
assume
x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
;
x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g }
then consider x9 being
Element of
NAT such that A9:
x9 = x
and A10:
ex
u,
v being
Integer st
x9 = (u * a) + (v * b)
;
consider u,
v being
Integer such that A11:
x = (u * a) + (v * b)
by A9, A10;
consider r being
Nat such that A12:
x9 = (g * (x9 div g)) + r
and A13:
r < g
by A6, Def1;
A14:
r in NAT
by ORDINAL1:def 12;
r =
x9 - (g * (x9 div g))
by A12
.=
(a * (u + (- (s * (x9 div g))))) + (b * (v + (- (t * (x9 div g)))))
by A7, A9, A11
;
then
r in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
by A14;
then
r = 0
by A6, A13;
hence
x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g }
by A9, A12;
verum
end;
for
x being
object st
x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } holds
x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
then A17:
{ zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } = { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
by A8, TARSKI:2;
A18:
|.b.| = b
by ABSVALUE:def 1;
A19:
|.a.| = a
by ABSVALUE:def 1;
A20:
for
m being
Nat st
m divides |.a.| &
m divides |.b.| holds
m divides g
b = (0 * a) + (1 * b)
;
then
b in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
;
then
ex
b9 being
Element of
NAT st
(
b9 = b & ex
t being
Element of
NAT st
b9 = t * g )
by A17;
then A27:
g divides |.b.|
by A18;
ex
a9 being
Element of
NAT st
(
a9 = a & ex
s being
Element of
NAT st
a9 = s * g )
by A4, A17;
then
g divides |.a.|
by A19;
then g =
|.a.| gcd |.b.|
by A27, A20, Def5
.=
a gcd b
by INT_2:34
;
hence
ex
s,
t being
Integer st
a gcd b = (s * a) + (t * b)
by A7;
verum
end;
hence
ex s, t being Integer st a gcd b = (s * a) + (t * b)
; verum