Metamath Proof Explorer

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

Proof

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