Theorem lgs0

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

	Ref	Expression
Assertion	lgs0	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		eqid	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 0 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 0 ) ) , 1 ) )
3	2	lgsval	⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝐴 /L 0 ) = if ( 0 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 0 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 0 ) ) , 1 ) ) ) ‘ ( abs ‘ 0 ) ) ) ) )
4	1 3	mpan2	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 0 ) = if ( 0 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 0 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 0 ) ) , 1 ) ) ) ‘ ( abs ‘ 0 ) ) ) ) )
5		eqid	⊢ 0 = 0
6	5	iftruei	⊢ if ( 0 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 0 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 0 ) ) , 1 ) ) ) ‘ ( abs ‘ 0 ) ) ) ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 )
7	4 6	eqtrdi	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )