Metamath Proof Explorer

Theorem lgsval

Description: Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis 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
Assertion 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

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 simpr ⊢ a = A ∧ m = N → m = N
3 2 eqeq1d ⊢ a = A ∧ m = N → m = 0 ↔ N = 0
4 simpl ⊢ a = A ∧ m = N → a = A
5 4 oveq1d ⊢ a = A ∧ m = N → a 2 = A 2
6 5 eqeq1d ⊢ a = A ∧ m = N → a 2 = 1 ↔ A 2 = 1
7 6 ifbid ⊢ a = A ∧ m = N → if a 2 = 1 1 0 = if A 2 = 1 1 0
8 2 breq1d ⊢ a = A ∧ m = N → m < 0 ↔ N < 0
9 4 breq1d ⊢ a = A ∧ m = N → a < 0 ↔ A < 0
10 8 9 anbi12d ⊢ a = A ∧ m = N → m < 0 ∧ a < 0 ↔ N < 0 ∧ A < 0
11 10 ifbid ⊢ a = A ∧ m = N → if m < 0 ∧ a < 0 − 1 1 = if N < 0 ∧ A < 0 − 1 1
12 4 breq2d ⊢ a = A ∧ m = N → 2 ∥ a ↔ 2 ∥ A
13 4 oveq1d ⊢ a = A ∧ m = N → a mod 8 = A mod 8
14 13 eleq1d ⊢ a = A ∧ m = N → a mod 8 ∈ 1 7 ↔ A mod 8 ∈ 1 7
15 14 ifbid ⊢ a = A ∧ m = N → if a mod 8 ∈ 1 7 1 − 1 = if A mod 8 ∈ 1 7 1 − 1
16 12 15 ifbieq2d ⊢ a = A ∧ m = N → if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1
17 4 oveq1d ⊢ a = A ∧ m = N → a n − 1 2 = A n − 1 2
18 17 oveq1d ⊢ a = A ∧ m = N → a n − 1 2 + 1 = A n − 1 2 + 1
19 18 oveq1d ⊢ a = A ∧ m = N → a n − 1 2 + 1 mod n = A n − 1 2 + 1 mod n
20 19 oveq1d ⊢ a = A ∧ m = N → a n − 1 2 + 1 mod n − 1 = A n − 1 2 + 1 mod n − 1
21 16 20 ifeq12d ⊢ a = A ∧ m = N → if n = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a n − 1 2 + 1 mod n − 1 = if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1
22 2 oveq2d ⊢ a = A ∧ m = N → n pCnt m = n pCnt N
23 21 22 oveq12d ⊢ a = A ∧ m = 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 m = 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
24 23 ifeq1d ⊢ a = A ∧ m = 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 m 1 = 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
25 24 mpteq2dv ⊢ a = A ∧ m = N → 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 m 1 = 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
26 25 1 eqtr4di ⊢ a = A ∧ m = N → 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 m 1 = F
27 26 seqeq3d ⊢ a = A ∧ m = N → seq 1 × 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 m 1 = seq 1 × F
28 2 fveq2d ⊢ a = A ∧ m = N → m = N
29 27 28 fveq12d ⊢ a = A ∧ m = N → seq 1 × 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 m 1 ⁡ m = seq 1 × F ⁡ N
30 11 29 oveq12d ⊢ a = A ∧ m = N → if m < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × 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 m 1 ⁡ m = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N
31 3 7 30 ifbieq12d ⊢ a = A ∧ m = N → if m = 0 if a 2 = 1 1 0 if m < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × 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 m 1 ⁡ m = if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N
32 df-lgs ⊢ / L = a ∈ ℤ , m ∈ ℤ ⟼ if m = 0 if a 2 = 1 1 0 if m < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × 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 m 1 ⁡ m
33 1nn0 ⊢ 1 ∈ ℕ 0
34 0nn0 ⊢ 0 ∈ ℕ 0
35 33 34 ifcli ⊢ if A 2 = 1 1 0 ∈ ℕ 0
36 35 elexi ⊢ if A 2 = 1 1 0 ∈ V
37 ovex ⊢ if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N ∈ V
38 36 37 ifex ⊢ if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N ∈ V
39 31 32 38 ovmpoa ⊢ 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