Metamath Proof Explorer

Theorem lgs0

Description: The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgs0 ⊢ A ∈ ℤ → A / L 0 = if A 2 = 1 1 0

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 eqid ⊢ n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt 0 1 = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt 0 1
3 2 lgsval ⊢ A ∈ ℤ ∧ 0 ∈ ℤ → A / L 0 = if 0 = 0 if A 2 = 1 1 0 if 0 < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt 0 1 ⁡ 0
4 1 3 mpan2 ⊢ A ∈ ℤ → A / L 0 = if 0 = 0 if A 2 = 1 1 0 if 0 < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt 0 1 ⁡ 0
5 eqid ⊢ 0 = 0
6 5 iftruei ⊢ if 0 = 0 if A 2 = 1 1 0 if 0 < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt 0 1 ⁡ 0 = if A 2 = 1 1 0
7 4 6 eqtrdi ⊢ A ∈ ℤ → A / L 0 = if A 2 = 1 1 0