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 ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
lgsfcl2.z ⊢ Z = x ∈ ℤ | x ≤ 1
Assertion lgscllem ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ Z

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
2 lgsfcl2.z ⊢ Z = x ∈ ℤ | x ≤ 1
3 1 lgsval ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N = if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × 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 ⊢ if A 2 = 1 1 0 ∈ Z
8 7 a1i ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N = 0 → if A 2 = 1 1 0 ∈ Z
9 4 simp1i ⊢ − 1 ∈ Z
10 9 5 ifcli ⊢ if N < 0 ∧ A < 0 − 1 1 ∈ 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 → seq 1 × F ⁡ N ∈ Z
28 2 lgslem3 ⊢ if N < 0 ∧ A < 0 − 1 1 ∈ Z ∧ seq 1 × F ⁡ N ∈ Z → if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N ∈ Z
29 10 27 28 sylancr ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ ¬ N = 0 → if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N ∈ Z
30 8 29 ifclda ⊢ A ∈ ℤ ∧ N ∈ ℤ → if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N ∈ Z
31 3 30 eqeltrd ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ Z