prmdiveq

Description: The modular inverse of A mod P is unique. (Contributed by Mario Carneiro, 24-Jan-2015)

		Ref	Expression
	Hypothesis	prmdiv.1	$⊢ R = A^{P - 2} \mod P$
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		prmdiv.1	$⊢ R = A^{P - 2} \mod P$
2		simpl1	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P \in ℙ$
3		prmz	$⊢ P \in ℙ \to P \in ℤ$
4	2 3	syl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P \in ℤ$
5		simpl2	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A \in ℤ$
6		elfzelz	$⊢ S \in (0 \dots P - 1) \to S \in ℤ$
7	6	ad2antrl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \in ℤ$
8	5 7	zmulcld	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A S \in ℤ$
9		1z	$⊢ 1 \in ℤ$
10		zsubcl	$⊢ (A S \in ℤ \land 1 \in ℤ) \to A S - 1 \in ℤ$
11	8 9 10	sylancl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A S - 1 \in ℤ$
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	12	adantr	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to (R \in (1 \dots P - 1) \land P ∥ (A R - 1))$
14	13	simpld	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to R \in (1 \dots P - 1)$
15		elfzelz	$⊢ R \in (1 \dots P - 1) \to R \in ℤ$
16	14 15	syl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to R \in ℤ$
17	5 16	zmulcld	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A R \in ℤ$
18		zsubcl	$⊢ (A R \in ℤ \land 1 \in ℤ) \to A R - 1 \in ℤ$
19	17 9 18	sylancl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A R - 1 \in ℤ$
20		simprr	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P ∥ (A S - 1)$
21	13	simprd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P ∥ (A R - 1)$
22	4 11 19 20 21	dvds2subd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P ∥ (A S - 1 - (A R - 1))$
23	8	zcnd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A S \in ℂ$
24	17	zcnd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A R \in ℂ$
25		1cnd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to 1 \in ℂ$
26	23 24 25	nnncan2d	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A S - 1 - (A R - 1) = A S - A R$
27	5	zcnd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A \in ℂ$
28		elfznn0	$⊢ S \in (0 \dots P - 1) \to S \in ℕ_{0}$
29	28	ad2antrl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \in ℕ_{0}$
30	29	nn0red	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \in ℝ$
31	30	recnd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \in ℂ$
32	16	zcnd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to R \in ℂ$
33	27 31 32	subdid	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A (S - R) = A S - A R$
34	26 33	eqtr4d	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A S - 1 - (A R - 1) = A (S - R)$
35	22 34	breqtrd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P ∥ A (S - R)$
36		simpl3	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to \neg P ∥ A$
37		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
38	2 5 37	syl2anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
39	36 38	mpbid	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P \gcd A = 1$
40	7 16	zsubcld	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S - R \in ℤ$
41		coprmdvds	$⊢ (P \in ℤ \land A \in ℤ \land S - R \in ℤ) \to ((P ∥ A (S - R) \land P \gcd A = 1) \to P ∥ (S - R))$
42	4 5 40 41	syl3anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to ((P ∥ A (S - R) \land P \gcd A = 1) \to P ∥ (S - R))$
43	35 39 42	mp2and	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P ∥ (S - R)$
44		prmnn	$⊢ P \in ℙ \to P \in ℕ$
45	2 44	syl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P \in ℕ$
46		moddvds	$⊢ (P \in ℕ \land S \in ℤ \land R \in ℤ) \to (S \mod P = R \mod P \leftrightarrow P ∥ (S - R))$
47	45 7 16 46	syl3anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to (S \mod P = R \mod P \leftrightarrow P ∥ (S - R))$
48	43 47	mpbird	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \mod P = R \mod P$
49	45	nnrpd	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P \in ℝ^{+}$
50		elfzle1	$⊢ S \in (0 \dots P - 1) \to 0 \leq S$
51	50	ad2antrl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to 0 \leq S$
52		elfzle2	$⊢ S \in (0 \dots P - 1) \to S \leq P - 1$
53	52	ad2antrl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \leq P - 1$
54		zltlem1	$⊢ (S \in ℤ \land P \in ℤ) \to (S < P \leftrightarrow S \leq P - 1)$
55	7 4 54	syl2anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to (S < P \leftrightarrow S \leq P - 1)$
56	53 55	mpbird	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S < P$
57		modid	$⊢ ((S \in ℝ \land P \in ℝ^{+}) \land (0 \leq S \land S < P)) \to S \mod P = S$
58	30 49 51 56 57	syl22anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S \mod P = S$
59		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
60		uznn0sub	$⊢ P \in ℤ_{\geq 2} \to P - 2 \in ℕ_{0}$
61	2 59 60	3syl	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to P - 2 \in ℕ_{0}$
62		zexpcl	$⊢ (A \in ℤ \land P - 2 \in ℕ_{0}) \to A^{P - 2} \in ℤ$
63	5 61 62	syl2anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A^{P - 2} \in ℤ$
64	63	zred	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to A^{P - 2} \in ℝ$
65		modabs2	$⊢ (A^{P - 2} \in ℝ \land P \in ℝ^{+}) \to (A^{P - 2} \mod P) \mod P = A^{P - 2} \mod P$
66	64 49 65	syl2anc	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to (A^{P - 2} \mod P) \mod P = A^{P - 2} \mod P$
67	1	oveq1i	$⊢ R \mod P = (A^{P - 2} \mod P) \mod P$
68	66 67 1	3eqtr4g	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to R \mod P = R$
69	48 58 68	3eqtr3d	$⊢ ((P \in ℙ \land A \in ℤ \land \neg P ∥ A) \land (S \in (0 \dots P - 1) \land P ∥ (A S - 1))) \to S = R$
70	69	ex	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ((S \in (0 \dots P - 1) \land P ∥ (A S - 1)) \to S = R)$
71		fz1ssfz0	$⊢ (1 \dots P - 1) \subseteq (0 \dots P - 1)$
72	71	sseli	$⊢ R \in (1 \dots P - 1) \to R \in (0 \dots P - 1)$
73		eleq1	$⊢ S = R \to (S \in (0 \dots P - 1) \leftrightarrow R \in (0 \dots P - 1))$
74	72 73	syl5ibr	$⊢ S = R \to (R \in (1 \dots P - 1) \to S \in (0 \dots P - 1))$
75		oveq2	$⊢ S = R \to A S = A R$
76	75	oveq1d	$⊢ S = R \to A S - 1 = A R - 1$
77	76	breq2d	$⊢ S = R \to (P ∥ (A S - 1) \leftrightarrow P ∥ (A R - 1))$
78	77	biimprd	$⊢ S = R \to (P ∥ (A R - 1) \to P ∥ (A S - 1))$
79	74 78	anim12d	$⊢ S = R \to ((R \in (1 \dots P - 1) \land P ∥ (A R - 1)) \to (S \in (0 \dots P - 1) \land P ∥ (A S - 1)))$
80	12 79	syl5com	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (S = R \to (S \in (0 \dots P - 1) \land P ∥ (A S - 1)))$
81	70 80	impbid	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ((S \in (0 \dots P - 1) \land P ∥ (A S - 1)) \leftrightarrow S = R)$

Metamath Proof Explorer

Theorem prmdiveq

Proof