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

Metamath Proof Explorer

Theorem fermltl

Description: Fermat's little theorem. When P is prime, A ^ P == A (mod P ) for any A , see theorem 5.19 in ApostolNT p. 114. (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 19-Mar-2022)

Ref Expression
Assertion fermltl ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )

Proof

Step Hyp Ref Expression
1 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2 dvdsmodexp ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∈ ℕ ∧ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )
3 2 3exp ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 ∈ ℕ → ( 𝑃 ∥ 𝐴 → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) ) )
4 1 1 3 sylc ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ 𝐴 → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
5 4 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ 𝐴 → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
6 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
7 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
8 gcdcom ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 gcd 𝐴 ) = ( 𝐴 gcd 𝑃 ) )
9 7 8 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 gcd 𝐴 ) = ( 𝐴 gcd 𝑃 ) )
10 9 eqeq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝑃 gcd 𝐴 ) = 1 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
11 6 10 bitrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
12 simp2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → 𝐴 ∈ ℤ )
13 1 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → 𝑃 ∈ ℕ )
14 13 phicld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ϕ ‘ 𝑃 ) ∈ ℕ )
15 14 nnnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ϕ ‘ 𝑃 ) ∈ ℕ0 )
16 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℤ )
17 12 15 16 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℤ )
18 17 zred ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℝ )
19 1red ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → 1 ∈ ℝ )
20 13 nnrpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → 𝑃 ∈ ℝ+ )
21 eulerth ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
22 1 21 syl3an1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
23 modmul1 ⊢ ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) · 𝐴 ) mod 𝑃 ) = ( ( 1 · 𝐴 ) mod 𝑃 ) )
24 18 19 12 20 22 23 syl221anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) · 𝐴 ) mod 𝑃 ) = ( ( 1 · 𝐴 ) mod 𝑃 ) )
25 phiprm ⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
26 25 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
27 26 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) = ( 𝐴 ↑ ( 𝑃 − 1 ) ) )
28 27 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) · 𝐴 ) = ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) · 𝐴 ) )
29 12 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → 𝐴 ∈ ℂ )
30 expm1t ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℕ ) → ( 𝐴 ↑ 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) · 𝐴 ) )
31 29 13 30 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( 𝐴 ↑ 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) · 𝐴 ) )
32 28 31 eqtr4d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) · 𝐴 ) = ( 𝐴 ↑ 𝑃 ) )
33 32 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) · 𝐴 ) mod 𝑃 ) = ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) )
34 29 mullidd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( 1 · 𝐴 ) = 𝐴 )
35 34 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 1 · 𝐴 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )
36 24 33 35 3eqtr3d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )
37 36 3expia ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝑃 ) = 1 → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
38 11 37 sylbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
39 5 38 pm2.61d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑃 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )