Metamath Proof Explorer

Theorem lgsfval

Description: Value of the function F which defines the Legendre symbol at the primes. (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 lgsfval ⊢ M ∈ ℕ → F ⁡ M = if M ∈ ℙ if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1 M pCnt N 1

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 eleq1 ⊢ n = M → n ∈ ℙ ↔ M ∈ ℙ
3 eqeq1 ⊢ n = M → n = 2 ↔ M = 2
4 oveq1 ⊢ n = M → n − 1 = M − 1
5 4 oveq1d ⊢ n = M → n − 1 2 = M − 1 2
6 5 oveq2d ⊢ n = M → A n − 1 2 = A M − 1 2
7 6 oveq1d ⊢ n = M → A n − 1 2 + 1 = A M − 1 2 + 1
8 id ⊢ n = M → n = M
9 7 8 oveq12d ⊢ n = M → A n − 1 2 + 1 mod n = A M − 1 2 + 1 mod M
10 9 oveq1d ⊢ n = M → A n − 1 2 + 1 mod n − 1 = A M − 1 2 + 1 mod M − 1
11 3 10 ifbieq2d ⊢ n = M → if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 = if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1
12 oveq1 ⊢ n = M → n pCnt N = M pCnt N
13 11 12 oveq12d ⊢ n = 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 = if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1 M pCnt N
14 2 13 ifbieq1d ⊢ n = M → 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 = if M ∈ ℙ if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1 M pCnt N 1
15 ovex ⊢ if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1 M pCnt N ∈ V
16 1ex ⊢ 1 ∈ V
17 15 16 ifex ⊢ if M ∈ ℙ if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1 M pCnt N 1 ∈ V
18 14 1 17 fvmpt ⊢ M ∈ ℕ → F ⁡ M = if M ∈ ℙ if M = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A M − 1 2 + 1 mod M − 1 M pCnt N 1