Theorem lgs2

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

	Ref	Expression
Assertion	lgs2	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 2 ) = if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2prm	⊢ 2 ∈ ℙ
2		lgsval2	⊢ ( ( 𝐴 ∈ ℤ ∧ 2 ∈ ℙ ) → ( 𝐴 /L 2 ) = if ( 2 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 2 − 1 ) / 2 ) ) + 1 ) mod 2 ) − 1 ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 2 ) = if ( 2 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 2 − 1 ) / 2 ) ) + 1 ) mod 2 ) − 1 ) ) )
4		eqid	⊢ 2 = 2
5	4	iftruei	⊢ if ( 2 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 2 − 1 ) / 2 ) ) + 1 ) mod 2 ) − 1 ) ) = if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) )
6	3 5	eqtrdi	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 2 ) = if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) )