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 that
A2: a > 0 and
A3: b > 0 ; :: thesis: 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 ; :: 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 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; :: thesis: 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) }
proof
let x be object ; :: 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 A15: ex x9 being Element of NAT st
( x9 = x & ex u being Element of NAT st x9 = u * g ) ;
then consider u being Integer such that
A16: x = u * g ;
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;
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
proof
ex g9 being Element of NAT st
( g9 = g & ex s, t being Integer st g9 = (s * a) + (t * b) ) by A6;
then consider s, t being Integer such that
A21: g = (s * a) + (t * b) ;
let m be Nat; :: thesis: ( m divides |.a.| & m divides |.b.| implies m divides g )
assume that
A22: m divides |.a.| and
A23: m divides |.b.| ; :: thesis: m divides g
consider u being Nat such that
A24: a = m * u by A19, A22;
consider v being Nat such that
A25: b = m * v by A18, A23;
A26: g = m * ((s * u) + (t * v)) by A24, A25, A21;
then (s * u) + (t * v) >= 0 by A6;
then (s * u) + (t * v) is Element of NAT by INT_1:3;
hence m divides g by A26; :: thesis: verum
end;
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; :: thesis: verum
end;
now :: thesis: ( ( ( a = 0 or b = 0 ) & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) or ( a <> 0 & b <> 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) )
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 = |.b.|
proof
let a, b be Integer; :: thesis: ( a = 0 implies a gcd b = |.b.| )
assume a = 0 ; :: thesis: a gcd b = |.b.|
then |.a.| = 0 by ABSVALUE:def 1;
then A30: |.b.| divides |.a.| by Th6;
( a gcd b = |.a.| gcd |.b.| & ( for m being Nat st m divides |.a.| & m divides |.b.| holds
m divides |.b.| ) ) by INT_2:34;
hence a gcd b = |.b.| by A30, Def5; :: thesis: verum
end;
now :: thesis: ( ( a = 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) or ( b = 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) )
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 A31: a gcd b = |.b.| by A29;
now :: thesis: ( ( b >= 0 & a gcd b = (0 * a) + (1 * b) ) or ( b < 0 & a gcd b = (0 * a) + ((- 1) * b) ) )
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 A31, ABSVALUE:def 1; :: thesis: verum
end;
case b < 0 ; :: thesis: a gcd b = (0 * a) + ((- 1) * b)
hence a gcd b = - (b * 1) by A31, 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 A32: a gcd b = |.a.| by A29;
now :: thesis: ( ( a >= 0 & a gcd b = (1 * a) + (0 * b) ) or ( a < 0 & a gcd b = (0 * b) + ((- 1) * a) ) )
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 A32, ABSVALUE:def 1; :: thesis: verum
end;
case a < 0 ; :: thesis: a gcd b = (0 * b) + ((- 1) * a)
hence a gcd b = - (a * 1) by A32, 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 A33: ( a <> 0 & b <> 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
now :: thesis: ( ( a >= 0 & b >= 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) or ( a < 0 & b >= 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) or ( a >= 0 & b < 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) or ( a < 0 & b < 0 & ex s, t being Integer st a gcd b = (s * a) + (t * b) ) )
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, A33; :: thesis: verum
end;
case A34: ( a < 0 & b >= 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then - a > 0 by XREAL_1:58;
then consider s, t being Integer such that
A35: (- a) gcd b = (s * (- a)) + (t * b) by A1, A33, A34;
A36: a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.(- a).| gcd |.b.| by COMPLEX1:52
.= (- a) gcd b by INT_2:34 ;
(s * (- a)) + (t * b) = ((- s) * a) + (t * b) ;
hence ex s, t being Integer st a gcd b = (s * a) + (t * b) by A35, A36; :: thesis: verum
end;
case A37: ( a >= 0 & b < 0 ) ; :: thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then - b > 0 by XREAL_1:58;
then consider s, t being Integer such that
A38: a gcd (- b) = (s * a) + (t * (- b)) by A1, A33, A37;
A39: a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.a.| gcd |.(- b).| by COMPLEX1:52
.= a gcd (- b) by INT_2:34 ;
(s * a) + (t * (- b)) = (s * a) + ((- t) * b) ;
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:58;
then consider s, t being Integer such that
A40: (- a) gcd (- b) = (s * (- a)) + (t * (- b)) by A1;
A41: a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.a.| gcd |.(- b).| by COMPLEX1:52
.= |.(- a).| gcd |.(- b).| by COMPLEX1:52
.= (- a) gcd (- b) by INT_2:34 ;
(s * (- a)) + (t * (- b)) = ((- s) * a) + ((- t) * b) ;
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