Metamath Proof Explorer

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 ⊢ N ∈ ℤ ∧ D ∈ ℕ ∧ 1 < D → D ∥ N → ¬ D ∥ N + 1

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 1 jctl ⊢ 1 < D → 1 ∈ ℕ ∧ 1 < D
3 ndvdsadd ⊢ N ∈ ℤ ∧ D ∈ ℕ ∧ 1 ∈ ℕ ∧ 1 < D → D ∥ N → ¬ D ∥ N + 1
4 2 3 syl3an3 ⊢ N ∈ ℤ ∧ D ∈ ℕ ∧ 1 < D → D ∥ N → ¬ D ∥ N + 1