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

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

Metamath Proof Explorer