This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem modprminv

Description: Show an explicit expression for the modular inverse of A mod P . This is an application of prmdiv . (Contributed by Alexander van der Vekens, 15-May-2018)

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

Proof

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