Metamath Proof Explorer

Theorem lgsprme0

Description: The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in ApostolNT p. 179. (Contributed by AV, 20-Jul-2021)

Ref Expression
Assertion lgsprme0 ⊢ A ∈ ℤ ∧ P ∈ ℙ → A / L P = 0 ↔ A mod P = 0

Proof

Step Hyp Ref Expression
1 prmz ⊢ P ∈ ℙ → P ∈ ℤ
2 lgsne0 ⊢ A ∈ ℤ ∧ P ∈ ℤ → A / L P ≠ 0 ↔ A gcd P = 1
3 1 2 sylan2 ⊢ A ∈ ℤ ∧ P ∈ ℙ → A / L P ≠ 0 ↔ A gcd P = 1
4 coprm ⊢ P ∈ ℙ ∧ A ∈ ℤ → ¬ P ∥ A ↔ P gcd A = 1
5 4 ancoms ⊢ A ∈ ℤ ∧ P ∈ ℙ → ¬ P ∥ A ↔ P gcd A = 1
6 1 anim1i ⊢ P ∈ ℙ ∧ A ∈ ℤ → P ∈ ℤ ∧ A ∈ ℤ
7 6 ancoms ⊢ A ∈ ℤ ∧ P ∈ ℙ → P ∈ ℤ ∧ A ∈ ℤ
8 gcdcom ⊢ P ∈ ℤ ∧ A ∈ ℤ → P gcd A = A gcd P
9 7 8 syl ⊢ A ∈ ℤ ∧ P ∈ ℙ → P gcd A = A gcd P
10 9 eqeq1d ⊢ A ∈ ℤ ∧ P ∈ ℙ → P gcd A = 1 ↔ A gcd P = 1
11 5 10 bitr2d ⊢ A ∈ ℤ ∧ P ∈ ℙ → A gcd P = 1 ↔ ¬ P ∥ A
12 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
13 dvdsval3 ⊢ P ∈ ℕ ∧ A ∈ ℤ → P ∥ A ↔ A mod P = 0
14 12 13 sylan ⊢ P ∈ ℙ ∧ A ∈ ℤ → P ∥ A ↔ A mod P = 0
15 14 ancoms ⊢ A ∈ ℤ ∧ P ∈ ℙ → P ∥ A ↔ A mod P = 0
16 15 notbid ⊢ A ∈ ℤ ∧ P ∈ ℙ → ¬ P ∥ A ↔ ¬ A mod P = 0
17 3 11 16 3bitrd ⊢ A ∈ ℤ ∧ P ∈ ℙ → A / L P ≠ 0 ↔ ¬ A mod P = 0
18 17 necon4abid ⊢ A ∈ ℤ ∧ P ∈ ℙ → A / L P = 0 ↔ A mod P = 0