let n, p be Nat; :: thesis: ( p > 0 & n divides p & n <> 1 & n <> p implies ( 1 < n & n < p ) )
assume A1: ( p > 0 & n divides p ) ; :: thesis: ( not n <> 1 or not n <> p or ( 1 < n & n < p ) )
assume A2: n <> 1 ; :: thesis: ( not n <> p or ( 1 < n & n < p ) )
assume A3: n <> p ; :: thesis: ( 1 < n & n < p )
n <> 0 by A1, INT_2:3;
hence 1 < n by A2, NAT_1:25; :: thesis: n < p
n <= p by A1, NAT_D:7;
hence n < p by A3, XXREAL_0:1; :: thesis: verum