Metamath Proof Explorer

Theorem prmdivdiv

Description: The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Hypothesis prmdiv.1 ⊢ 𝑅 = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
Assertion prmdivdiv ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 = ( ( 𝑅 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )

Proof

Step Hyp Ref Expression
1 prmdiv.1 ⊢ 𝑅 = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
2 fz1ssfz0 ⊢ ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 0 ... ( 𝑃 − 1 ) )
3 simpr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
4 2 3 sselid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 ∈ ( 0 ... ( 𝑃 − 1 ) ) )
5 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℙ )
6 elfznn ⊢ ( 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝐴 ∈ ℕ )
7 6 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 ∈ ℕ )
8 7 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 ∈ ℤ )
9 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
10 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝐴 )
11 9 10 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝐴 )
12 1 prmdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) ) )
13 5 8 11 12 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) ) )
14 13 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ( 𝐴 · 𝑅 ) − 1 ) )
15 7 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 ∈ ℂ )
16 13 simpld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
17 elfznn ⊢ ( 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑅 ∈ ℕ )
18 16 17 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑅 ∈ ℕ )
19 18 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑅 ∈ ℂ )
20 15 19 mulcomd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝐴 · 𝑅 ) = ( 𝑅 · 𝐴 ) )
21 20 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( 𝐴 · 𝑅 ) − 1 ) = ( ( 𝑅 · 𝐴 ) − 1 ) )
22 14 21 breqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ( 𝑅 · 𝐴 ) − 1 ) )
23 16 elfzelzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑅 ∈ ℤ )
24 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑅 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑅 )
25 9 16 24 syl2an2r ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑅 )
26 eqid ⊢ ( ( 𝑅 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑅 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
27 26 prmdiveq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑅 ) → ( ( 𝐴 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑅 · 𝐴 ) − 1 ) ) ↔ 𝐴 = ( ( 𝑅 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
28 5 23 25 27 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( 𝐴 ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑅 · 𝐴 ) − 1 ) ) ↔ 𝐴 = ( ( 𝑅 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
29 4 22 28 mpbi2and ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝐴 = ( ( 𝑅 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )