Theorem vfermltl

Description: Variant of Fermat's little theorem if A is not a multiple of P , see theorem 5.18 in ApostolNT p. 113. (Contributed by AV, 21-Aug-2020) (Proof shortened by AV, 5-Sep-2020)

	Ref	Expression
Assertion	vfermltl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		phiprm	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
2	1	eqcomd	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) = ( ϕ ‘ 𝑃 ) )
3	2	3ad2ant1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 1 ) = ( ϕ ‘ 𝑃 ) )
4	3	oveq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( 𝑃 − 1 ) ) = ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) )
5	4	oveq1d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) )
6		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
7	6	3ad2ant1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℕ )
8		simp2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝐴 ∈ ℤ )
9		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
10	9	anim1ci	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) )
11	10	3adant3	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) )
12		gcdcom	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝐴 gcd 𝑃 ) = ( 𝑃 gcd 𝐴 ) )
13	11 12	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 gcd 𝑃 ) = ( 𝑃 gcd 𝐴 ) )
14		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
15	14	biimp3a	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 gcd 𝐴 ) = 1 )
16	13 15	eqtrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 gcd 𝑃 ) = 1 )
17		eulerth	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
18	7 8 16 17	syl3anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
19	6	nnred	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
20		prmgt1	⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
21	19 20	jca	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
22	21	3ad2ant1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
23		1mod	⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
24	22 23	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 1 mod 𝑃 ) = 1 )
25	5 18 24	3eqtrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 )