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