Metamath Proof Explorer

Theorem modprminveq

Description: The modular inverse of A mod P is unique. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Hypothesis modprminv.1 ⊢ R = A P − 2 mod P
Assertion modprminveq ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ ¬ P ∥ A → S ∈ 0 … P − 1 ∧ A ⁢ S mod P = 1 ↔ S = R

Proof

Step Hyp Ref Expression
1 modprminv.1 ⊢ R = A P − 2 mod P
2 elfzelz ⊢ S ∈ 0 … P − 1 → S ∈ ℤ
3 zmulcl ⊢ A ∈ ℤ ∧ S ∈ ℤ → A ⁢ S ∈ ℤ
4 2 3 sylan2 ⊢ A ∈ ℤ ∧ S ∈ 0 … P − 1 → A ⁢ S ∈ ℤ
5 modprm1div ⊢ P ∈ ℙ ∧ A ⁢ S ∈ ℤ → A ⁢ S mod P = 1 ↔ P ∥ A ⁢ S − 1
6 4 5 sylan2 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ S ∈ 0 … P − 1 → A ⁢ S mod P = 1 ↔ P ∥ A ⁢ S − 1
7 6 expr ⊢ P ∈ ℙ ∧ A ∈ ℤ → S ∈ 0 … P − 1 → A ⁢ S mod P = 1 ↔ P ∥ A ⁢ S − 1
8 7 3adant3 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ ¬ P ∥ A → S ∈ 0 … P − 1 → A ⁢ S mod P = 1 ↔ P ∥ A ⁢ S − 1
9 8 pm5.32d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ ¬ P ∥ A → S ∈ 0 … P − 1 ∧ A ⁢ S mod P = 1 ↔ S ∈ 0 … P − 1 ∧ P ∥ A ⁢ S − 1
10 1 prmdiveq ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ ¬ P ∥ A → S ∈ 0 … P − 1 ∧ P ∥ A ⁢ S − 1 ↔ S = R
11 9 10 bitrd ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ ¬ P ∥ A → S ∈ 0 … P − 1 ∧ A ⁢ S mod P = 1 ↔ S = R