This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ELEMENTARY NUMBER THEORY Elementary properties of divisibility The division algorithm 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 ) ) )