let a, b be Integer; :: thesis: 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; :: thesis: ( a > 0 & b > 0 implies ex s, t being Integer st a gcd b = (s * a) + (t * b) )
assume A2: ( a > 0 & b > 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then reconsider a = a, b = b as Element of NAT by INT_1:16;
set M = { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } ;
defpred S₁[ 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) & b = (0 * a) + (1 * b) ) ;
then A3: ( a in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } & b in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } ) ;
then A4: ex k being Nat st S₁[k] by A2;
consider g being Nat such that
A5: ( S₁[g] & ( for n being Nat st S₁[n] holds
g <= n ) ) from NAT_1:sch 5(A4);
consider z being Element of NAT such that
A6: ( z = g & ex s, t being Integer st z = (s * a) + (t * b) ) by A5;
consider s, t being Integer such that
A7: g = (s * a) + (t * b) by A6;
set G = { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } ;
A8: ( abs a = a & abs b = b ) by ABSVALUE:def 1;
A9: { 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) }

proof

A10: for x being set 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 set ; :: thesis: ( 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) } ; :: thesis: x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g }
then consider x' being Element of NAT such that
A11: ( x' = x & ex u, v being Integer st x' = (u * a) + (v * b) ) ;
consider u, v being Integer such that
A12: x = (u * a) + (v * b) by A11;
consider r being Nat such that
A13: ( x' = (g * (x' div g)) + r & r < g ) by A5, NAT_D:def 1;
A14: r in NAT by ORDINAL1:def 13;
r = x' - (g * (x' div g)) by A13
.= ((u * a) + (v * b)) - ((a * (s * (x' div g))) + (b * (t * (x' div g)))) by A7, A11, A12
.= (a * (u + (- (s * (x' div g))))) + (b * (v + (- (t * (x' div g))))) ;
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 A5, A13;
hence x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } by A11, A13; :: thesis: verum

end;

for x being set 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) }

proof

let x be set ; :: thesis: ( x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } implies x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } )
assume x in { zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g } ; :: thesis: x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) }
then consider x' being Element of NAT such that
A15: ( x' = x & ex u being Element of NAT st x' = u * g ) ;
consider u being Integer such that
A16: x = u * g by A15;
x = ((u * s) * a) + ((u * t) * b) by A7, A16;
hence x in { z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b) } by A15; :: thesis: verum

end;

hence { 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 A10, TARSKI:2; :: thesis: verum

end;

then consider a' being Element of NAT such that
A17: ( a' = a & ex s being Element of NAT st a' = s * g ) by A3;
consider b' being Element of NAT such that
A18: ( b' = b & ex t being Element of NAT st b' = t * g ) by A3, A9;
consider u, v being Element of NAT such that
A19: ( a = u * g & b = v * g ) by A17, A18;
A20: ( g divides abs a & g divides abs b ) by A8, A19, NAT_D:def 3;
for m being Nat st m divides abs a & m divides abs b holds
m divides g

proof

let m be Nat; :: thesis: ( m divides abs a & m divides abs b implies m divides g )
assume A21: ( m divides abs a & m divides abs b ) ; :: thesis: m divides g
then consider u being Nat such that
A22: a = m * u by A8, NAT_D:def 3;
consider v being Nat such that
A23: b = m * v by A8, A21, NAT_D:def 3;
consider g' being Element of NAT such that
A24: ( g' = g & ex s, t being Integer st g' = (s * a) + (t * b) ) by A5;
consider s, t being Integer such that
A25: g = (s * a) + (t * b) by A24;
A26: g = m * ((s * u) + (t * v)) by A22, A23, A25;
(s * u) + (t * v) is Element of NAT

proof

(s * u) + (t * v) >= 0 by A5, A26;
hence (s * u) + (t * v) is Element of NAT by INT_1:16; :: thesis: verum

end;

hence m divides g by A26, NAT_D:def 3; :: thesis: verum

end;

then g = (abs a) gcd (abs b) by A20, NAT_D:def 5
.= a gcd b by INT_2:51 ;
hence ex s, t being Integer st a gcd b = (s * a) + (t * b) by A7; :: thesis: verum

end;

now

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

case A28: ( a = 0 or b = 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

A29: for a, b being Integer st a = 0 holds
a gcd b = abs b

proof

let a, b be Integer; :: thesis: ( a = 0 implies a gcd b = abs b )
assume a = 0 ; :: thesis: a gcd b = abs b
then A30: abs a = 0 by ABSVALUE:def 1;
A31: a gcd b = (abs a) gcd (abs b) by INT_2:51;
A32: abs b divides abs a by A30, NAT_D:6;
for m being Nat st m divides abs a & m divides abs b holds
m divides abs b ;
hence a gcd b = abs b by A31, A32, NAT_D:def 5; :: thesis: verum

end;

now

per cases ( a = 0 or b = 0 ) by A28;

case a = 0 ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

then A33: a gcd b = abs b by A29;

now

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

case b >= 0 ; :: thesis: a gcd b = (0 * a) + (1 * b)

hence a gcd b = (0 * a) + (1 * b) by A33, ABSVALUE:def 1; :: thesis: verum

end;

case b < 0 ; :: thesis: a gcd b = (0 * a) + ((- 1) * b)

hence a gcd b = - (b * 1) by A33, ABSVALUE:def 1
.= (0 * a) + ((- 1) * b) ;
:: thesis: verum

end;

end;

end;

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

end;

case b = 0 ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

then A34: a gcd b = abs a by A29;

now

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

case a >= 0 ; :: thesis: a gcd b = (1 * a) + (0 * b)

hence a gcd b = (1 * a) + (0 * b) by A34, ABSVALUE:def 1; :: thesis: verum

end;

case a < 0 ; :: thesis: a gcd b = (0 * b) + ((- 1) * a)

hence a gcd b = - (a * 1) by A34, ABSVALUE:def 1
.= (0 * b) + ((- 1) * a) ;
:: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

case A35: ( a <> 0 & b <> 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

now

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

case ( a >= 0 & b >= 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

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

end;

case ( a < 0 & b >= 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

then ( - a > 0 & b > 0 ) by A35, XREAL_1:60;
then consider s, t being Integer such that
A36: (- a) gcd b = (s * (- a)) + (t * b) by A1;
A37: (s * (- a)) + (t * b) = ((- s) * a) + (t * b) ;
a gcd b = (abs a) gcd (abs b) by INT_2:51
.= (abs (- a)) gcd (abs b) by COMPLEX1:138
.= (- a) gcd b by INT_2:51 ;
hence ex s, t being Integer st a gcd b = (s * a) + (t * b) by A36, A37; :: thesis: verum

end;

case ( a >= 0 & b < 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

then ( - b > 0 & a > 0 ) by A35, XREAL_1:60;
then consider s, t being Integer such that
A38: a gcd (- b) = (s * a) + (t * (- b)) by A1;
A39: (s * a) + (t * (- b)) = (s * a) + ((- t) * b) ;
a gcd b = (abs a) gcd (abs b) by INT_2:51
.= (abs a) gcd (abs (- b)) by COMPLEX1:138
.= a gcd (- b) by INT_2:51 ;
hence ex s, t being Integer st a gcd b = (s * a) + (t * b) by A38, A39; :: thesis: verum

end;

case ( a < 0 & b < 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)

then ( - a > 0 & - b > 0 ) by XREAL_1:60;
then consider s, t being Integer such that
A40: (- a) gcd (- b) = (s * (- a)) + (t * (- b)) by A1;
A41: (s * (- a)) + (t * (- b)) = ((- s) * a) + ((- t) * b) ;
a gcd b = (abs a) gcd (abs b) by INT_2:51
.= (abs a) gcd (abs (- b)) by COMPLEX1:138
.= (abs (- a)) gcd (abs (- b)) by COMPLEX1:138
.= (- a) gcd (- b) by INT_2:51 ;
hence ex s, t being Integer st a gcd b = (s * a) + (t * b) by A40, A41; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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