reumodprminv

Description: For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018)

		Ref	Expression
	Assertion	reumodprminv	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to \exists! i \in (1 \dots P - 1) N i \mod P = 1$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to P \in ℙ$
2		elfzoelz	$⊢ N \in (1 ..^P) \to N \in ℤ$
3	2	adantl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to N \in ℤ$
4		prmnn	$⊢ P \in ℙ \to P \in ℕ$
5		prmz	$⊢ P \in ℙ \to P \in ℤ$
6		fzoval	$⊢ P \in ℤ \to (1 ..^P) = (1 \dots P - 1)$
7	5 6	syl	$⊢ P \in ℙ \to (1 ..^P) = (1 \dots P - 1)$
8	7	eleq2d	$⊢ P \in ℙ \to (N \in (1 ..^P) \leftrightarrow N \in (1 \dots P - 1))$
9	8	biimpa	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to N \in (1 \dots P - 1)$
10		fzm1ndvds	$⊢ (P \in ℕ \land N \in (1 \dots P - 1)) \to \neg P ∥ N$
11	4 9 10	syl2an2r	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to \neg P ∥ N$
12		eqid	$⊢ N^{P - 2} \mod P = N^{P - 2} \mod P$
13	12	modprminv	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to (N^{P - 2} \mod P \in (1 \dots P - 1) \land N (N^{P - 2} \mod P) \mod P = 1)$
14	13	simpld	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to N^{P - 2} \mod P \in (1 \dots P - 1)$
15	13	simprd	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to N (N^{P - 2} \mod P) \mod P = 1$
16		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
17		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots P - 1) \subseteq (0 \dots P - 1)$
18	16 17	mp1i	$⊢ P \in ℙ \to (1 \dots P - 1) \subseteq (0 \dots P - 1)$
19	18	sseld	$⊢ P \in ℙ \to (s \in (1 \dots P - 1) \to s \in (0 \dots P - 1))$
20	19	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to (s \in (1 \dots P - 1) \to s \in (0 \dots P - 1))$
21	20	imdistani	$⊢ ((P \in ℙ \land N \in ℤ \land \neg P ∥ N) \land s \in (1 \dots P - 1)) \to ((P \in ℙ \land N \in ℤ \land \neg P ∥ N) \land s \in (0 \dots P - 1))$
22	12	modprminveq	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to ((s \in (0 \dots P - 1) \land N s \mod P = 1) \leftrightarrow s = N^{P - 2} \mod P)$
23	22	biimpa	$⊢ ((P \in ℙ \land N \in ℤ \land \neg P ∥ N) \land (s \in (0 \dots P - 1) \land N s \mod P = 1)) \to s = N^{P - 2} \mod P$
24	23	eqcomd	$⊢ ((P \in ℙ \land N \in ℤ \land \neg P ∥ N) \land (s \in (0 \dots P - 1) \land N s \mod P = 1)) \to N^{P - 2} \mod P = s$
25	24	expr	$⊢ ((P \in ℙ \land N \in ℤ \land \neg P ∥ N) \land s \in (0 \dots P - 1)) \to (N s \mod P = 1 \to N^{P - 2} \mod P = s)$
26	21 25	syl	$⊢ ((P \in ℙ \land N \in ℤ \land \neg P ∥ N) \land s \in (1 \dots P - 1)) \to (N s \mod P = 1 \to N^{P - 2} \mod P = s)$
27	26	ralrimiva	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to N^{P - 2} \mod P = s)$
28	14 15 27	jca32	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to (N^{P - 2} \mod P \in (1 \dots P - 1) \land (N (N^{P - 2} \mod P) \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to N^{P - 2} \mod P = s)))$
29	1 3 11 28	syl3anc	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to (N^{P - 2} \mod P \in (1 \dots P - 1) \land (N (N^{P - 2} \mod P) \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to N^{P - 2} \mod P = s)))$
30		oveq2	$⊢ i = N^{P - 2} \mod P \to N i = N (N^{P - 2} \mod P)$
31	30	oveq1d	$⊢ i = N^{P - 2} \mod P \to N i \mod P = N (N^{P - 2} \mod P) \mod P$
32	31	eqeq1d	$⊢ i = N^{P - 2} \mod P \to (N i \mod P = 1 \leftrightarrow N (N^{P - 2} \mod P) \mod P = 1)$
33		eqeq1	$⊢ i = N^{P - 2} \mod P \to (i = s \leftrightarrow N^{P - 2} \mod P = s)$
34	33	imbi2d	$⊢ i = N^{P - 2} \mod P \to ((N s \mod P = 1 \to i = s) \leftrightarrow (N s \mod P = 1 \to N^{P - 2} \mod P = s))$
35	34	ralbidv	$⊢ i = N^{P - 2} \mod P \to (\forall s \in (1 \dots P - 1) (N s \mod P = 1 \to i = s) \leftrightarrow \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to N^{P - 2} \mod P = s))$
36	32 35	anbi12d	$⊢ i = N^{P - 2} \mod P \to ((N i \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to i = s)) \leftrightarrow (N (N^{P - 2} \mod P) \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to N^{P - 2} \mod P = s)))$
37	36	rspcev	$⊢ (N^{P - 2} \mod P \in (1 \dots P - 1) \land (N (N^{P - 2} \mod P) \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to N^{P - 2} \mod P = s))) \to \exists i \in (1 \dots P - 1) (N i \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to i = s))$
38	29 37	syl	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to \exists i \in (1 \dots P - 1) (N i \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to i = s))$
39		oveq2	$⊢ i = s \to N i = N s$
40	39	oveq1d	$⊢ i = s \to N i \mod P = N s \mod P$
41	40	eqeq1d	$⊢ i = s \to (N i \mod P = 1 \leftrightarrow N s \mod P = 1)$
42	41	reu8	$⊢ \exists! i \in (1 \dots P - 1) N i \mod P = 1 \leftrightarrow \exists i \in (1 \dots P - 1) (N i \mod P = 1 \land \forall s \in (1 \dots P - 1) (N s \mod P = 1 \to i = s))$
43	38 42	sylibr	$⊢ (P \in ℙ \land N \in (1 ..^P)) \to \exists! i \in (1 \dots P - 1) N i \mod P = 1$

Metamath Proof Explorer

Theorem reumodprminv

Proof