let i1, j1 be Integer; :: thesis: ( i1,j1 are_coprime implies ex s, t being Integer st (s * i1) + (t * j1) = 1 )
assume A1: i1,j1 are_coprime ; :: thesis: ex s, t being Integer st (s * i1) + (t * j1) = 1
then B1: j1 gcd i1 = 1 by INT_2:def 3;
per cases ( ( i1 >= 0 & j1 >= 0 ) or ( i1 >= 0 & j1 < 0 ) or ( i1 < 0 & j1 >= 0 ) or ( i1 < 0 & j1 < 0 ) ) ;
suppose ( i1 >= 0 & j1 >= 0 ) ; :: thesis: ex s, t being Integer st (s * i1) + (t * j1) = 1
then ( i1 in NAT & j1 in NAT ) by INT_1:3;
hence ex s, t being Integer st (s * i1) + (t * j1) = 1 by A1, EULER_1:10; :: thesis: verum
end;
suppose A3: ( i1 >= 0 & j1 < 0 ) ; :: thesis: ex s, t being Integer st (s * i1) + (t * j1) = 1
set j2 = - j1;
( i1 in NAT & - j1 in NAT ) by A3, INT_1:3;
then reconsider i1 = i1, j2 = - j1 as Nat ;
i1 gcd j2 = |.i1.| gcd |.(- j1).|
.= i1 gcd |.j1.| by COMPLEX1:52
.= 1 by B1, INT_6:14 ;
then consider s, t being Integer such that
A5: (s * i1) + (t * j2) = 1 by EULER_1:10, INT_2:def 3;
(s * i1) + ((- t) * j1) = 1 by A5;
hence ex s, t being Integer st (s * i1) + (t * j1) = 1 ; :: thesis: verum
end;
suppose A6: ( i1 < 0 & j1 >= 0 ) ; :: thesis: ex s, t being Integer st (s * i1) + (t * j1) = 1
set i2 = - i1;
( - i1 in NAT & j1 in NAT ) by A6, INT_1:3;
then reconsider i2 = - i1, j1 = j1 as Nat ;
i2 gcd j1 = |.(- i1).| gcd |.j1.|
.= |.i1.| gcd j1 by COMPLEX1:52
.= 1 by B1, INT_6:14 ;
then consider s, t being Integer such that
A8: (s * i2) + (t * j1) = 1 by EULER_1:10, INT_2:def 3;
((- s) * i1) + (t * j1) = 1 by A8;
hence ex s, t being Integer st (s * i1) + (t * j1) = 1 ; :: thesis: verum
end;
suppose A9: ( i1 < 0 & j1 < 0 ) ; :: thesis: ex s, t being Integer st (s * i1) + (t * j1) = 1
set i2 = - i1;
set j2 = - j1;
( - i1 in NAT & - j1 in NAT ) by A9, INT_1:3;
then reconsider i2 = - i1, j2 = - j1 as Nat ;
i2 gcd j2 = |.(- i1).| gcd |.(- j1).|
.= |.i1.| gcd |.(- j1).| by COMPLEX1:52
.= |.i1.| gcd |.j1.| by COMPLEX1:52
.= |.i1.| gcd j1 by INT_6:14
.= 1 by B1, INT_6:14 ;
then consider s, t being Integer such that
A11: (s * i2) + (t * j2) = 1 by EULER_1:10, INT_2:def 3;
((- s) * i1) + ((- t) * j1) = 1 by A11;
hence ex s, t being Integer st (s * i1) + (t * j1) = 1 ; :: thesis: verum
end;
end;