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 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ ¬ P ∥ A → A P − 1 mod P = 1

Proof

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