let i, j be Nat; :: thesis: ( i <> 0 & i < j & j is prime implies i,j are_coprime )
assume that
A1: i <> 0 and
A2: i < j and
A3: j is prime ; :: thesis: i,j are_coprime

now :: thesis: i,j are_coprime

set IJ = i gcd j;
A4: i gcd j <> j

proof

assume i gcd j = j ; :: thesis: contradiction
then j divides i by NAT_D:def 5;
then consider n being Nat such that
A5: i = j * n by NAT_D:def 3;
n <> 0 by A1, A5;
then j * n >= j * 1 by NAT_1:14, XREAL_1:64;
hence contradiction by A2, A5; :: thesis: verum

end;

i gcd j divides j by NAT_D:def 5;
then ( i gcd j = 1 or i gcd j = j ) by A3, INT_2:def 4;
hence i,j are_coprime by A4, INT_2:def 3; :: thesis: verum

end;

hence i,j are_coprime ; :: thesis: verum