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	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷 ) → ( 𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2	1	jctl	⊢ ( 1 < 𝐷 → ( 1 ∈ ℕ ∧ 1 < 𝐷 ) )
3		ndvdsadd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 1 ∈ ℕ ∧ 1 < 𝐷 ) ) → ( 𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ ( 𝑁 + 1 ) ) )
4	2 3	syl3an3	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷 ) → ( 𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ ( 𝑁 + 1 ) ) )