let n, m be Nat; :: thesis: ( m <> 1 & m divides n implies not m divides n + 1 )
assume that
A1: m <> 1 and
A2: m divides n and
A3: m divides n + 1 ; :: thesis: contradiction
consider t being Nat such that
A4: n = m * t by A2, NAT_D:def 3;
consider s being Nat such that
A5: n + 1 = m * s by A3, NAT_D:def 3;
t <= s
proof
(n + 1) * t = (m * s) * t by A5
.= n * s by A4 ;
then A6: t = (n * s) / (n + 1) by XCMPLX_1:89
.= s * (n / (n + 1)) by XCMPLX_1:74 ;
assume A7: t > s ; :: thesis: contradiction
s > 0 by A5;
hence contradiction by A7, A6, Th37, XREAL_1:157; :: thesis: verum
end;
then reconsider r = s - t as Element of NAT by INT_1:5;
1 = (m * s) - (m * t) by A4, A5;
then 1 = m * r ;
hence contradiction by A1, NAT_1:15; :: thesis: verum