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/L0=ifA2=110

Proof

Step Hyp Ref Expression
1 0z ⊢0∈ℤ
2 eqid ⊢n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCnt01=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCnt01
3 2 lgsval ⊢A∈ℤ∧0∈ℤ→A/L0=if0=0ifA2=110if0<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCnt01⁡0
4 1 3 mpan2 ⊢A∈ℤ→A/L0=if0=0ifA2=110if0<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCnt01⁡0
5 eqid ⊢0=0
6 5 iftruei ⊢if0=0ifA2=110if0<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCnt01⁡0=ifA2=110
7 4 6 eqtrdi ⊢A∈ℤ→A/L0=ifA2=110