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 ) ∈ ℕ₀ )
12	10 11	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 1 ) ∈ ℕ₀ )
13	8 12	eqeltrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ϕ ‘ 𝑃 ) ∈ ℕ₀ )
14		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑃 ) ∈ ℕ₀ ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℤ )
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 ) ∈ ℕ₀ )
22	20 21	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 2 ) ∈ ℕ₀ )
23		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ₀ ) → ( 𝐴 ↑ ( 𝑃 − 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	eqtrid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑅 = ( ( 𝐴 ↑ ( 𝑃 − 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 )
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 ) ) )

Metamath Proof Explorer

Theorem prmdiv

Proof