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 𝑃 ) )