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 \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (1 \dots P - 1) \land A R \mod P = 1)$

Proof

Step	Hyp	Ref	Expression
1		modprminv.1	$⊢ R = A^{P - 2} \mod P$
2	1	prmdiv	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (1 \dots P - 1) \land P ∥ (A R - 1))$
3		elfzelz	$⊢ R \in (1 \dots P - 1) \to R \in ℤ$
4		zmulcl	$⊢ (A \in ℤ \land R \in ℤ) \to A R \in ℤ$
5	3 4	sylan2	$⊢ (A \in ℤ \land R \in (1 \dots P - 1)) \to A R \in ℤ$
6		modprm1div	$⊢ (P \in ℙ \land A R \in ℤ) \to (A R \mod P = 1 \leftrightarrow P ∥ (A R - 1))$
7	5 6	sylan2	$⊢ (P \in ℙ \land (A \in ℤ \land R \in (1 \dots P - 1))) \to (A R \mod P = 1 \leftrightarrow P ∥ (A R - 1))$
8	7	expr	$⊢ (P \in ℙ \land A \in ℤ) \to (R \in (1 \dots P - 1) \to (A R \mod P = 1 \leftrightarrow P ∥ (A R - 1)))$
9	8	3adant3	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (1 \dots P - 1) \to (A R \mod P = 1 \leftrightarrow P ∥ (A R - 1)))$
10	9	pm5.32d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ((R \in (1 \dots P - 1) \land A R \mod P = 1) \leftrightarrow (R \in (1 \dots P - 1) \land P ∥ (A R - 1)))$
11	2 10	mpbird	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (1 \dots P - 1) \land A R \mod P = 1)$