let i, j be Nat; :: thesis: ( j < i & i < j + j implies i mod j <> 0 )
assume that
A1: j < i and
A2: i < j + j ; :: thesis: i mod j <> 0
A3: i - j < (j + j) - j by A2, XREAL_1:9;
i - j = i -' j by A1, XREAL_1:233;
then A4: (i -' j) mod j = i -' j by A3, NAT_D:24;
assume A5: i mod j = 0 ; :: thesis: contradiction
i = (i - j) + j ;
then i mod j = ((i -' j) + j) mod j by A1, XREAL_1:233
.= ((i -' j) + (j mod j)) mod j by NAT_D:23
.= ((i -' j) + 0) mod j by NAT_D:25
.= (i -' j) mod j ;
hence contradiction by A1, A5, A4, NAT_D:36; :: thesis: verum