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;

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 ) )
;

end;

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;hence ex s, t being Integer st (s * i1) + (t * j1) = 1 by A1, EULER_1:10; :: thesis: verum

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;( 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

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;( - 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

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;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