prmdiv

Description: Show an explicit expression for the modular inverse of A mod P . (Contributed by Mario Carneiro, 24-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		prmdiv.1	$⊢ R = A^{P - 2} \mod P$
2		nprmdvds1	$⊢ P \in ℙ \to \neg P ∥ 1$
3	2	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to \neg P ∥ 1$
4		prmz	$⊢ P \in ℙ \to P \in ℤ$
5	4	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℤ$
6		simp2	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \in ℤ$
7		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
8	7	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ϕ (P) = P - 1$
9		prmnn	$⊢ P \in ℙ \to P \in ℕ$
10	9	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℕ$
11		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
12	10 11	syl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - 1 \in ℕ_{0}$
13	8 12	eqeltrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ϕ (P) \in ℕ_{0}$
14		zexpcl	$⊢ (A \in ℤ \land ϕ (P) \in ℕ_{0}) \to A^{ϕ (P)} \in ℤ$
15	6 13 14	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} \in ℤ$
16		1z	$⊢ 1 \in ℤ$
17		zsubcl	$⊢ (A^{ϕ (P)} \in ℤ \land 1 \in ℤ) \to A^{ϕ (P)} - 1 \in ℤ$
18	15 16 17	sylancl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} - 1 \in ℤ$
19		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
20	19	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℤ_{\geq 2}$
21		uznn0sub	$⊢ P \in ℤ_{\geq 2} \to P - 2 \in ℕ_{0}$
22	20 21	syl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - 2 \in ℕ_{0}$
23		zexpcl	$⊢ (A \in ℤ \land P - 2 \in ℕ_{0}) \to A^{P - 2} \in ℤ$
24	6 22 23	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} \in ℤ$
25	24	zred	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} \in ℝ$
26	25 10	nndivred	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to \frac{A^{P - 2}}{P} \in ℝ$
27	26	flcld	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ⌊\frac{A^{P - 2}}{P}⌋ \in ℤ$
28	6 27	zmulcld	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A ⌊\frac{A^{P - 2}}{P}⌋ \in ℤ$
29	5 28	zmulcld	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P A ⌊\frac{A^{P - 2}}{P}⌋ \in ℤ$
30	6 5	gcdcomd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \gcd P = P \gcd A$
31		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
32	31	biimp3a	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \gcd A = 1$
33	30 32	eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \gcd P = 1$
34		eulerth	$⊢ (P \in ℕ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \mod P = 1 \mod P$
35	10 6 33 34	syl3anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} \mod P = 1 \mod P$
36		1zzd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to 1 \in ℤ$
37		moddvds	$⊢ (P \in ℕ \land A^{ϕ (P)} \in ℤ \land 1 \in ℤ) \to (A^{ϕ (P)} \mod P = 1 \mod P \leftrightarrow P ∥ (A^{ϕ (P)} - 1))$
38	10 15 36 37	syl3anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (A^{ϕ (P)} \mod P = 1 \mod P \leftrightarrow P ∥ (A^{ϕ (P)} - 1))$
39	35 38	mpbid	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P ∥ (A^{ϕ (P)} - 1)$
40		dvdsmul1	$⊢ (P \in ℤ \land A ⌊\frac{A^{P - 2}}{P}⌋ \in ℤ) \to P ∥ P A ⌊\frac{A^{P - 2}}{P}⌋$
41	5 28 40	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P ∥ P A ⌊\frac{A^{P - 2}}{P}⌋$
42	5 18 29 39 41	dvds2subd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P ∥ (A^{ϕ (P)} - 1 - P A ⌊\frac{A^{P - 2}}{P}⌋)$
43	6	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \in ℂ$
44	24	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} \in ℂ$
45	5 27	zmulcld	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P ⌊\frac{A^{P - 2}}{P}⌋ \in ℤ$
46	45	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P ⌊\frac{A^{P - 2}}{P}⌋ \in ℂ$
47	43 44 46	subdid	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A (A^{P - 2} - P ⌊\frac{A^{P - 2}}{P}⌋) = A A^{P - 2} - A P ⌊\frac{A^{P - 2}}{P}⌋$
48	10	nnrpd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℝ^{+}$
49		modval	$⊢ (A^{P - 2} \in ℝ \land P \in ℝ^{+}) \to A^{P - 2} \mod P = A^{P - 2} - P ⌊\frac{A^{P - 2}}{P}⌋$
50	25 48 49	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} \mod P = A^{P - 2} - P ⌊\frac{A^{P - 2}}{P}⌋$
51	1 50	eqtrid	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to R = A^{P - 2} - P ⌊\frac{A^{P - 2}}{P}⌋$
52	51	oveq2d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A R = A (A^{P - 2} - P ⌊\frac{A^{P - 2}}{P}⌋)$
53		2m1e1	$⊢ 2 - 1 = 1$
54	53	oveq2i	$⊢ P - (2 - 1) = P - 1$
55	8 54	eqtr4di	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ϕ (P) = P - (2 - 1)$
56	10	nncnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℂ$
57		2cnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to 2 \in ℂ$
58		1cnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to 1 \in ℂ$
59	56 57 58	subsubd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - (2 - 1) = P - 2 + 1$
60	55 59	eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ϕ (P) = P - 2 + 1$
61	60	oveq2d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} = A^{P - 2 + 1}$
62	43 22	expp1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2 + 1} = A^{P - 2} A$
63	44 43	mulcomd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} A = A A^{P - 2}$
64	61 62 63	3eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} = A A^{P - 2}$
65	27	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to ⌊\frac{A^{P - 2}}{P}⌋ \in ℂ$
66	56 43 65	mul12d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P A ⌊\frac{A^{P - 2}}{P}⌋ = A P ⌊\frac{A^{P - 2}}{P}⌋$
67	64 66	oveq12d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} - P A ⌊\frac{A^{P - 2}}{P}⌋ = A A^{P - 2} - A P ⌊\frac{A^{P - 2}}{P}⌋$
68	47 52 67	3eqtr4d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A R = A^{ϕ (P)} - P A ⌊\frac{A^{P - 2}}{P}⌋$
69	68	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A R - 1 = A^{ϕ (P)} - P A ⌊\frac{A^{P - 2}}{P}⌋ - 1$
70	15	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} \in ℂ$
71	29	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P A ⌊\frac{A^{P - 2}}{P}⌋ \in ℂ$
72	70 71 58	sub32d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} - P A ⌊\frac{A^{P - 2}}{P}⌋ - 1 = A^{ϕ (P)} - 1 - P A ⌊\frac{A^{P - 2}}{P}⌋$
73	69 72	eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A R - 1 = A^{ϕ (P)} - 1 - P A ⌊\frac{A^{P - 2}}{P}⌋$
74	42 73	breqtrrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P ∥ (A R - 1)$
75		oveq2	$⊢ R = 0 \to A R = A \cdot 0$
76	75	oveq1d	$⊢ R = 0 \to A R - 1 = A \cdot 0 - 1$
77	76	breq2d	$⊢ R = 0 \to (P ∥ (A R - 1) \leftrightarrow P ∥ (A \cdot 0 - 1))$
78	74 77	syl5ibcom	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R = 0 \to P ∥ (A \cdot 0 - 1))$
79	43	mul01d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \cdot 0 = 0$
80	79	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \cdot 0 - 1 = 0 - 1$
81		df-neg	$⊢ - 1 = 0 - 1$
82	80 81	eqtr4di	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \cdot 0 - 1 = - 1$
83	82	breq2d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (P ∥ (A \cdot 0 - 1) \leftrightarrow P ∥ -1)$
84		dvdsnegb	$⊢ (P \in ℤ \land 1 \in ℤ) \to (P ∥ 1 \leftrightarrow P ∥ -1)$
85	5 16 84	sylancl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (P ∥ 1 \leftrightarrow P ∥ -1)$
86	83 85	bitr4d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (P ∥ (A \cdot 0 - 1) \leftrightarrow P ∥ 1)$
87	78 86	sylibd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R = 0 \to P ∥ 1)$
88	3 87	mtod	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to \neg R = 0$
89		zmodfz	$⊢ (A^{P - 2} \in ℤ \land P \in ℕ) \to A^{P - 2} \mod P \in (0 \dots P - 1)$
90	24 10 89	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} \mod P \in (0 \dots P - 1)$
91	1 90	eqeltrid	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to R \in (0 \dots P - 1)$
92		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
93	12 92	eleqtrdi	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - 1 \in ℤ_{\geq 0}$
94		elfzp12	$⊢ P - 1 \in ℤ_{\geq 0} \to (R \in (0 \dots P - 1) \leftrightarrow (R = 0 \lor R \in (0 + 1 \dots P - 1)))$
95	93 94	syl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (0 \dots P - 1) \leftrightarrow (R = 0 \lor R \in (0 + 1 \dots P - 1)))$
96	91 95	mpbid	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R = 0 \lor R \in (0 + 1 \dots P - 1))$
97	96	ord	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (\neg R = 0 \to R \in (0 + 1 \dots P - 1))$
98	88 97	mpd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to R \in (0 + 1 \dots P - 1)$
99		1e0p1	$⊢ 1 = 0 + 1$
100	99	oveq1i	$⊢ (1 \dots P - 1) = (0 + 1 \dots P - 1)$
101	98 100	eleqtrrdi	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to R \in (1 \dots P - 1)$
102	101 74	jca	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (R \in (1 \dots P - 1) \land P ∥ (A R - 1))$

Metamath Proof Explorer

Theorem prmdiv

Proof