This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑅 = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
Assertion prmdiveq ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ↔ 𝑆 = 𝑅 ) )

Proof

Step Hyp Ref Expression
1 prmdiv.1 ⊢ 𝑅 = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
2 simpl1 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∈ ℙ )
3 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
4 2 3 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∈ ℤ )
5 simpl2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝐴 ∈ ℤ )
6 elfzelz ⊢ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) → 𝑆 ∈ ℤ )
7 6 ad2antrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 ∈ ℤ )
8 5 7 zmulcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 · 𝑆 ) ∈ ℤ )
9 1z ⊢ 1 ∈ ℤ
10 zsubcl ⊢ ( ( ( 𝐴 · 𝑆 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝐴 · 𝑆 ) − 1 ) ∈ ℤ )
11 8 9 10 sylancl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( 𝐴 · 𝑆 ) − 1 ) ∈ ℤ )
12 1 prmdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) ) )
13 12 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) ) )
14 13 simpld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
15 elfzelz ⊢ ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑅 ∈ ℤ )
16 14 15 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑅 ∈ ℤ )
17 5 16 zmulcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 · 𝑅 ) ∈ ℤ )
18 zsubcl ⊢ ( ( ( 𝐴 · 𝑅 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝐴 · 𝑅 ) − 1 ) ∈ ℤ )
19 17 9 18 sylancl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( 𝐴 · 𝑅 ) − 1 ) ∈ ℤ )
20 simprr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) )
21 13 simprd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) )
22 4 11 19 20 21 dvds2subd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∥ ( ( ( 𝐴 · 𝑆 ) − 1 ) − ( ( 𝐴 · 𝑅 ) − 1 ) ) )
23 8 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 · 𝑆 ) ∈ ℂ )
24 17 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 · 𝑅 ) ∈ ℂ )
25 1cnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 1 ∈ ℂ )
26 23 24 25 nnncan2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( ( 𝐴 · 𝑆 ) − 1 ) − ( ( 𝐴 · 𝑅 ) − 1 ) ) = ( ( 𝐴 · 𝑆 ) − ( 𝐴 · 𝑅 ) ) )
27 5 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝐴 ∈ ℂ )
28 elfznn0 ⊢ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) → 𝑆 ∈ ℕ0 )
29 28 ad2antrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 ∈ ℕ0 )
30 29 nn0red ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 ∈ ℝ )
31 30 recnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 ∈ ℂ )
32 16 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑅 ∈ ℂ )
33 27 31 32 subdid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 · ( 𝑆 − 𝑅 ) ) = ( ( 𝐴 · 𝑆 ) − ( 𝐴 · 𝑅 ) ) )
34 26 33 eqtr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( ( 𝐴 · 𝑆 ) − 1 ) − ( ( 𝐴 · 𝑅 ) − 1 ) ) = ( 𝐴 · ( 𝑆 − 𝑅 ) ) )
35 22 34 breqtrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∥ ( 𝐴 · ( 𝑆 − 𝑅 ) ) )
36 simpl3 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ¬ 𝑃 ∥ 𝐴 )
37 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
38 2 5 37 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
39 36 38 mpbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑃 gcd 𝐴 ) = 1 )
40 7 16 zsubcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑆 − 𝑅 ) ∈ ℤ )
41 coprmdvds ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝑆 − 𝑅 ) ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝐴 · ( 𝑆 − 𝑅 ) ) ∧ ( 𝑃 gcd 𝐴 ) = 1 ) → 𝑃 ∥ ( 𝑆 − 𝑅 ) ) )
42 4 5 40 41 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( 𝑃 ∥ ( 𝐴 · ( 𝑆 − 𝑅 ) ) ∧ ( 𝑃 gcd 𝐴 ) = 1 ) → 𝑃 ∥ ( 𝑆 − 𝑅 ) ) )
43 35 39 42 mp2and ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∥ ( 𝑆 − 𝑅 ) )
44 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
45 2 44 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∈ ℕ )
46 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑆 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( ( 𝑆 mod 𝑃 ) = ( 𝑅 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝑆 − 𝑅 ) ) )
47 45 7 16 46 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( 𝑆 mod 𝑃 ) = ( 𝑅 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝑆 − 𝑅 ) ) )
48 43 47 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑆 mod 𝑃 ) = ( 𝑅 mod 𝑃 ) )
49 45 nnrpd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑃 ∈ ℝ+ )
50 elfzle1 ⊢ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) → 0 ≤ 𝑆 )
51 50 ad2antrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 0 ≤ 𝑆 )
52 elfzle2 ⊢ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) → 𝑆 ≤ ( 𝑃 − 1 ) )
53 52 ad2antrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 ≤ ( 𝑃 − 1 ) )
54 zltlem1 ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑆 < 𝑃 ↔ 𝑆 ≤ ( 𝑃 − 1 ) ) )
55 7 4 54 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑆 < 𝑃 ↔ 𝑆 ≤ ( 𝑃 − 1 ) ) )
56 53 55 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 < 𝑃 )
57 modid ⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑆 ∧ 𝑆 < 𝑃 ) ) → ( 𝑆 mod 𝑃 ) = 𝑆 )
58 30 49 51 56 57 syl22anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑆 mod 𝑃 ) = 𝑆 )
59 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
60 uznn0sub ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 2 ) ∈ ℕ0 )
61 2 59 60 3syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑃 − 2 ) ∈ ℕ0 )
62 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
63 5 61 62 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
64 63 zred ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ )
65 modabs2 ⊢ ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
66 64 49 65 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
67 1 oveq1i ⊢ ( 𝑅 mod 𝑃 ) = ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 )
68 66 67 1 3eqtr4g ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → ( 𝑅 mod 𝑃 ) = 𝑅 )
69 48 58 68 3eqtr3d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) ∧ ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) → 𝑆 = 𝑅 )
70 69 ex ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) → 𝑆 = 𝑅 ) )
71 fz1ssfz0 ⊢ ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 0 ... ( 𝑃 − 1 ) )
72 71 sseli ⊢ ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑅 ∈ ( 0 ... ( 𝑃 − 1 ) ) )
73 eleq1 ⊢ ( 𝑆 = 𝑅 → ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ↔ 𝑅 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
74 72 73 imbitrrid ⊢ ( 𝑆 = 𝑅 → ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
75 oveq2 ⊢ ( 𝑆 = 𝑅 → ( 𝐴 · 𝑆 ) = ( 𝐴 · 𝑅 ) )
76 75 oveq1d ⊢ ( 𝑆 = 𝑅 → ( ( 𝐴 · 𝑆 ) − 1 ) = ( ( 𝐴 · 𝑅 ) − 1 ) )
77 76 breq2d ⊢ ( 𝑆 = 𝑅 → ( 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ↔ 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) ) )
78 77 biimprd ⊢ ( 𝑆 = 𝑅 → ( 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) → 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) )
79 74 78 anim12d ⊢ ( 𝑆 = 𝑅 → ( ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) ) → ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) )
80 12 79 syl5com ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑆 = 𝑅 → ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ) )
81 70 80 impbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝑆 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑆 ) − 1 ) ) ↔ 𝑆 = 𝑅 ) )