let i1, i2 be Integer; :: thesis: ( i1,i2 are_coprime implies ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1 )
assume A1: i1,i2 are_coprime ; :: thesis: ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
A2: |.i1.| gcd |.i2.| = i1 gcd i2 by INT_2:34
.= 1 by A1, INT_2:def 3 ;
reconsider n1 = |.i1.|, n2 = |.i2.| as Nat ;
consider jj1, jj2 being Integer such that
A3: (jj1 * n1) + (jj2 * n2) = 1 by A2, EULER_1:10, INT_2:def 3;
reconsider jj1 = jj1, jj2 = jj2 as Element of INT.Ring by INT_1:def 2;
per cases ( ( i1 >= 0 & i2 >= 0 ) or ( i1 >= 0 & i2 < 0 ) or ( i1 < 0 & i2 >= 0 ) or ( i1 < 0 & i2 < 0 ) ) ;
suppose ( i1 >= 0 & i2 >= 0 ) ; :: thesis: ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
then B1: ( |.i1.| = i1 & |.i2.| = i2 ) by ABSVALUE:def 1;
take jj1 ; :: thesis: ex j2 being Element of INT.Ring st (i1 * jj1) + (i2 * j2) = 1
take jj2 ; :: thesis: (i1 * jj1) + (i2 * jj2) = 1
thus (i1 * jj1) + (i2 * jj2) = 1 by B1, A3; :: thesis: verum
end;
suppose ( i1 >= 0 & i2 < 0 ) ; :: thesis: ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
then B1: ( |.i1.| = i1 & |.i2.| = - i2 ) by ABSVALUE:def 1;
take jj1 ; :: thesis: ex j2 being Element of INT.Ring st (i1 * jj1) + (i2 * j2) = 1
take - jj2 ; :: thesis: (i1 * jj1) + (i2 * (- jj2)) = 1
thus (i1 * jj1) + (i2 * (- jj2)) = 1 by B1, A3; :: thesis: verum
end;
suppose ( i1 < 0 & i2 >= 0 ) ; :: thesis: ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
then B1: ( |.i1.| = - i1 & |.i2.| = i2 ) by ABSVALUE:def 1;
take - jj1 ; :: thesis: ex j2 being Element of INT.Ring st (i1 * (- jj1)) + (i2 * j2) = 1
take jj2 ; :: thesis: (i1 * (- jj1)) + (i2 * jj2) = 1
thus (i1 * (- jj1)) + (i2 * jj2) = 1 by B1, A3; :: thesis: verum
end;
suppose ( i1 < 0 & i2 < 0 ) ; :: thesis: ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
then B1: ( |.i1.| = - i1 & |.i2.| = - i2 ) by ABSVALUE:def 1;
take - jj1 ; :: thesis: ex j2 being Element of INT.Ring st (i1 * (- jj1)) + (i2 * j2) = 1
take - jj2 ; :: thesis: (i1 * (- jj1)) + (i2 * (- jj2)) = 1
thus (i1 * (- jj1)) + (i2 * (- jj2)) = 1 by B1, A3; :: thesis: verum
end;
end;