Metamath Proof Explorer

Theorem lgscllem

Description: The Legendre symbol is an element of Z . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypotheses lgsval.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
lgsfcl2.z ⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
Assertion lgscllem ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ 𝑍 )

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
2 lgsfcl2.z ⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
3 1 lgsval ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
4 2 lgslem2 ⊢ ( - 1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍 )
5 4 simp3i ⊢ 1 ∈ 𝑍
6 4 simp2i ⊢ 0 ∈ 𝑍
7 5 6 ifcli ⊢ if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) ∈ 𝑍
8 7 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) ∈ 𝑍 )
9 4 simp1i ⊢ - 1 ∈ 𝑍
10 9 5 ifcli ⊢ if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ 𝑍
11 simplr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → 𝑁 ∈ ℤ )
12 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → ¬ 𝑁 = 0 )
13 12 neqned ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → 𝑁 ≠ 0 )
14 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
15 11 13 14 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
16 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
17 15 16 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → ( abs ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
18 df-ne ⊢ ( 𝑁 ≠ 0 ↔ ¬ 𝑁 = 0 )
19 1 2 lgsfcl2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝐹 : ℕ ⟶ 𝑍 )
20 19 3expa ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → 𝐹 : ℕ ⟶ 𝑍 )
21 18 20 sylan2br ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → 𝐹 : ℕ ⟶ 𝑍 )
22 elfznn ⊢ ( 𝑦 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) → 𝑦 ∈ ℕ )
23 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ 𝑍 ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑍 )
24 21 22 23 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑍 )
25 2 lgslem3 ⊢ ( ( 𝑦 ∈ 𝑍 ∧ 𝑧 ∈ 𝑍 ) → ( 𝑦 · 𝑧 ) ∈ 𝑍 )
26 25 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) ∧ ( 𝑦 ∈ 𝑍 ∧ 𝑧 ∈ 𝑍 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝑍 )
27 17 24 26 seqcl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ∈ 𝑍 )
28 2 lgslem3 ⊢ ( ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ 𝑍 ∧ ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ∈ 𝑍 ) → ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ∈ 𝑍 )
29 10 27 28 sylancr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ 𝑁 = 0 ) → ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ∈ 𝑍 )
30 8 29 ifclda ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) ∈ 𝑍 )
31 3 30 eqeltrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ 𝑍 )