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

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

hence
i,j are_coprime
; :: thesis: verumset IJ = i gcd j;

A4: i gcd j <> j

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;A4: i gcd j <> j

proof

i gcd j divides j
by NAT_D:def 5;
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;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

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