Metamath Proof Explorer

Theorem modprm1div

Description: A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018) (Proof shortened by AV, 30-May-2023)

Ref Expression
Assertion modprm1div ⊢ P ∈ ℙ ∧ A ∈ ℤ → A mod P = 1 ↔ P ∥ A − 1

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
2 modm1div ⊢ P ∈ ℤ ≥ 2 ∧ A ∈ ℤ → A mod P = 1 ↔ P ∥ A − 1
3 1 2 sylan ⊢ P ∈ ℙ ∧ A ∈ ℤ → A mod P = 1 ↔ P ∥ A − 1