This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )