Metamath Proof Explorer

Theorem m1dvdsndvds

Description: If an integer minus 1 is divisible by a prime number, the integer itself is not divisible by this prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018)

Ref Expression
Assertion m1dvdsndvds ⊢ P ∈ ℙ ∧ A ∈ ℤ → P ∥ A − 1 → ¬ P ∥ A

Proof

Step Hyp Ref Expression
1 ax-1ne0 ⊢ 1 ≠ 0
2 1 neii ⊢ ¬ 1 = 0
3 eqeq1 ⊢ 1 = A mod P → 1 = 0 ↔ A mod P = 0
4 3 eqcoms ⊢ A mod P = 1 → 1 = 0 ↔ A mod P = 0
5 2 4 mtbii ⊢ A mod P = 1 → ¬ A mod P = 0
6 5 a1i ⊢ P ∈ ℙ ∧ A ∈ ℤ → A mod P = 1 → ¬ A mod P = 0
7 modprm1div ⊢ P ∈ ℙ ∧ A ∈ ℤ → A mod P = 1 ↔ P ∥ A − 1
8 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
9 dvdsval3 ⊢ P ∈ ℕ ∧ A ∈ ℤ → P ∥ A ↔ A mod P = 0
10 8 9 sylan ⊢ P ∈ ℙ ∧ A ∈ ℤ → P ∥ A ↔ A mod P = 0
11 10 bicomd ⊢ P ∈ ℙ ∧ A ∈ ℤ → A mod P = 0 ↔ P ∥ A
12 11 notbid ⊢ P ∈ ℙ ∧ A ∈ ℤ → ¬ A mod P = 0 ↔ ¬ P ∥ A
13 6 7 12 3imtr3d ⊢ P ∈ ℙ ∧ A ∈ ℤ → P ∥ A − 1 → ¬ P ∥ A