Metamath Proof Explorer

Theorem lgs2

Description: The Legendre symbol at 2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgs2 ⊢ A ∈ ℤ → A / L 2 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1

Proof

Step Hyp Ref Expression
1 2prm ⊢ 2 ∈ ℙ
2 lgsval2 ⊢ A ∈ ℤ ∧ 2 ∈ ℙ → A / L 2 = if 2 = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A 2 − 1 2 + 1 mod 2 − 1
3 1 2 mpan2 ⊢ A ∈ ℤ → A / L 2 = if 2 = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A 2 − 1 2 + 1 mod 2 − 1
4 eqid ⊢ 2 = 2
5 4 iftruei ⊢ if 2 = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A 2 − 1 2 + 1 mod 2 − 1 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1
6 3 5 eqtrdi ⊢ A ∈ ℤ → A / L 2 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1