Theorem ndvdsp1

Description: Special case of ndvdsadd . If an integer D greater than 1 divides N , it does not divide N + 1 . (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Assertion	ndvdsp1	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\wedge 1<D\right)\to \left(D\parallel N\to \neg D\parallel \left(N+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2	1	jctl	$$⊢1<D\to \left(1\in \mathbb{N}\wedge 1<D\right)$$
3		ndvdsadd	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\wedge \left(1\in \mathbb{N}\wedge 1<D\right)\right)\to \left(D\parallel N\to \neg D\parallel \left(N+1\right)\right)$$
4	2 3	syl3an3	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{N}\wedge 1<D\right)\to \left(D\parallel N\to \neg D\parallel \left(N+1\right)\right)$$