# Metamath Proof Explorer

## Theorem 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}\mathrm{mod}{P}$
Assertion prmdiveq ${⊢}\left({P}\in ℙ\wedge {A}\in ℤ\wedge ¬{P}\parallel {A}\right)\to \left(\left({S}\in \left(0\dots {P}-1\right)\wedge {P}\parallel \left({A}{S}-1\right)\right)↔{S}={R}\right)$

### Proof

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