let i1, i2 be Integer; ( 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
; 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;