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 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
lgsfcl2.z ⊢Z=x∈ℤ|x≤1
Assertion lgscllem ⊢A∈ℤ∧N∈ℤ→A/LN∈Z

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
2 lgsfcl2.z ⊢Z=x∈ℤ|x≤1
3 1 lgsval ⊢A∈ℤ∧N∈ℤ→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N
4 2 lgslem2 ⊢−1∈Z∧0∈Z∧1∈Z
5 4 simp3i ⊢1∈Z
6 4 simp2i ⊢0∈Z
7 5 6 ifcli ⊢ifA2=110∈Z
8 7 a1i ⊢A∈ℤ∧N∈ℤ∧N=0→ifA2=110∈Z
9 4 simp1i ⊢−1∈Z
10 9 5 ifcli ⊢ifN<0∧A<0−11∈Z
11 simplr ⊢A∈ℤ∧N∈ℤ∧¬N=0→N∈ℤ
12 simpr ⊢A∈ℤ∧N∈ℤ∧¬N=0→¬N=0
13 12 neqned ⊢A∈ℤ∧N∈ℤ∧¬N=0→N≠0
14 nnabscl ⊢N∈ℤ∧N≠0→N∈ℕ
15 11 13 14 syl2anc ⊢A∈ℤ∧N∈ℤ∧¬N=0→N∈ℕ
16 nnuz ⊢ℕ=ℤ≥1
17 15 16 eleqtrdi ⊢A∈ℤ∧N∈ℤ∧¬N=0→N∈ℤ≥1
18 df-ne ⊢N≠0↔¬N=0
19 1 2 lgsfcl2 ⊢A∈ℤ∧N∈ℤ∧N≠0→F:ℕ⟶Z
20 19 3expa ⊢A∈ℤ∧N∈ℤ∧N≠0→F:ℕ⟶Z
21 18 20 sylan2br ⊢A∈ℤ∧N∈ℤ∧¬N=0→F:ℕ⟶Z
22 elfznn ⊢y∈1…N→y∈ℕ
23 ffvelcdm ⊢F:ℕ⟶Z∧y∈ℕ→F⁡y∈Z
24 21 22 23 syl2an ⊢A∈ℤ∧N∈ℤ∧¬N=0∧y∈1…N→F⁡y∈Z
25 2 lgslem3 ⊢y∈Z∧z∈Z→y⁢z∈Z
26 25 adantl ⊢A∈ℤ∧N∈ℤ∧¬N=0∧y∈Z∧z∈Z→y⁢z∈Z
27 17 24 26 seqcl ⊢A∈ℤ∧N∈ℤ∧¬N=0→seq1×F⁡N∈Z
28 2 lgslem3 ⊢ifN<0∧A<0−11∈Z∧seq1×F⁡N∈Z→ifN<0∧A<0−11⁢seq1×F⁡N∈Z
29 10 27 28 sylancr ⊢A∈ℤ∧N∈ℤ∧¬N=0→ifN<0∧A<0−11⁢seq1×F⁡N∈Z
30 8 29 ifclda ⊢A∈ℤ∧N∈ℤ→ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N∈Z
31 3 30 eqeltrd ⊢A∈ℤ∧N∈ℤ→A/LN∈Z