prmdivdiv

Description: The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015)

		Ref	Expression
	Hypothesis	prmdiv.1	$⊢ R = A^{P - 2} \mod P$
	Assertion	prmdivdiv	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A = R^{P - 2} \mod P$

Proof

Step	Hyp	Ref	Expression
1		prmdiv.1	$⊢ R = A^{P - 2} \mod P$
2		fz1ssfz0	$⊢ (1 \dots P - 1) \subseteq (0 \dots P - 1)$
3		simpr	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A \in (1 \dots P - 1)$
4	2 3	sseldi	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A \in (0 \dots P - 1)$
5		simpl	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to P \in ℙ$
6		elfznn	$⊢ A \in (1 \dots P - 1) \to A \in ℕ$
7	6	adantl	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A \in ℕ$
8	7	nnzd	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A \in ℤ$
9		prmnn	$⊢ P \in ℙ \to P \in ℕ$
10		fzm1ndvds	$⊢ (P \in ℕ \land A \in (1 \dots P - 1)) \to \neg P ∥ A$
11	9 10	sylan	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to \neg P ∥ A$
12	1	prmdiv	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (1 \dots P - 1) \land P ∥ (A R - 1))$
13	5 8 11 12	syl3anc	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to (R \in (1 \dots P - 1) \land P ∥ (A R - 1))$
14	13	simprd	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to P ∥ (A R - 1)$
15	7	nncnd	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A \in ℂ$
16	13	simpld	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to R \in (1 \dots P - 1)$
17		elfznn	$⊢ R \in (1 \dots P - 1) \to R \in ℕ$
18	16 17	syl	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to R \in ℕ$
19	18	nncnd	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to R \in ℂ$
20	15 19	mulcomd	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A R = R A$
21	20	oveq1d	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A R - 1 = R A - 1$
22	14 21	breqtrd	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to P ∥ (R A - 1)$
23		elfzelz	$⊢ R \in (1 \dots P - 1) \to R \in ℤ$
24	16 23	syl	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to R \in ℤ$
25		fzm1ndvds	$⊢ (P \in ℕ \land R \in (1 \dots P - 1)) \to \neg P ∥ R$
26	9 16 25	syl2an2r	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to \neg P ∥ R$
27		eqid	$⊢ R^{P - 2} \mod P = R^{P - 2} \mod P$
28	27	prmdiveq	$⊢ (P \in ℙ \land R \in ℤ \land \neg P ∥ R) \to ((A \in (0 \dots P - 1) \land P ∥ (R A - 1)) \leftrightarrow A = R^{P - 2} \mod P)$
29	5 24 26 28	syl3anc	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to ((A \in (0 \dots P - 1) \land P ∥ (R A - 1)) \leftrightarrow A = R^{P - 2} \mod P)$
30	4 22 29	mpbi2and	$⊢ (P \in ℙ \land A \in (1 \dots P - 1)) \to A = R^{P - 2} \mod P$

Metamath Proof Explorer

Theorem prmdivdiv

Proof