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