P. 257 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25601-25700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lgscl 25601	The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
Theorem	lgsle1 25602	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 25601 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴 /L 𝑁)) ≤ 1)
Theorem	lgsval2 25603	The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝐴 /L 𝑃) = if(𝑃 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)))
Theorem	lgs2 25604	The Legendre symbol at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
Theorem	lgsval3 25605	The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝐴 /L 𝑃) = ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
Theorem	lgsvalmod 25606	The Legendre symbol is equivalent to 𝑎↑((𝑝 − 1) / 2), mod 𝑝. This theorem is also called "Euler's criterion", see theorem 9.2 in [ApostolNT] p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr 25641. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃))
Theorem	lgsval4 25607*	Restate lgsval 25591 for nonzero 𝑁, where the function 𝐹 has been abbreviated into a self-referential expression taking the value of /L on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
Theorem	lgsfcl3 25608*	Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ)
Theorem	lgsval4a 25609*	Same as lgsval4 25607 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁))
Theorem	lgscl1 25610	The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ {-1, 0, 1})
Theorem	lgsneg 25611	The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L -𝑁) = (if(𝐴 < 0, -1, 1) · (𝐴 /L 𝑁)))
Theorem	lgsneg1 25612	The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (𝐴 /L -𝑁) = (𝐴 /L 𝑁))
Theorem	lgsmod 25613	The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁))
Theorem	lgsdilem 25614	Lemma for lgsdi 25624 and lgsdir 25622: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
Theorem	lgsdir2lem1 25615	Lemma for lgsdir2 25620. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((1 mod 8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) = 5))
Theorem	lgsdir2lem2 25616	Lemma for lgsdir2 25620. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝐾 ∈ ℤ ∧ 2 ∥ (𝐾 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...𝐾) → (𝐴 mod 8) ∈ 𝑆)))    &   ⊢ 𝑀 = (𝐾 + 1)    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ 𝑁 ∈ 𝑆    ⇒   ⊢ (𝑁 ∈ ℤ ∧ 2 ∥ (𝑁 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...𝑁) → (𝐴 mod 8) ∈ 𝑆)))
Theorem	lgsdir2lem3 25617	Lemma for lgsdir2 25620. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))
Theorem	lgsdir2lem4 25618	Lemma for lgsdir2 25620. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7}))
Theorem	lgsdir2lem5 25619	Lemma for lgsdir2 25620. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})
Theorem	lgsdir2 25620	The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2)))
Theorem	lgsdirprm 25621	The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))
Theorem	lgsdir 25622	The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that 𝐴 and 𝐵 are odd positive integers). Together with lgsqr 25641 this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
Theorem	lgsdilem2 25623*	Lemma for lgsdi 25624. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))
Theorem	lgsdi 25624	The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that 𝑀 and 𝑁 are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)))
Theorem	lgsne0 25625	The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	lgsabs1 25626	The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘(𝐴 /L 𝑁)) = 1 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	lgssq 25627	The Legendre symbol at a square is equal to 1. Together with lgsmod 25613 this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.) (Revised by AV, 20-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((𝐴↑2) /L 𝑁) = 1)
Theorem	lgssq2 25628	The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1)
Theorem	lgsprme0 25629	The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in [ApostolNT] p. 179. (Contributed by AV, 20-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 /L 𝑃) = 0 ↔ (𝐴 mod 𝑃) = 0))
Theorem	1lgs 25630	The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ (𝑁 ∈ ℤ → (1 /L 𝑁) = 1)
Theorem	lgs1 25631	The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 1) = 1)
Theorem	lgsmodeq 25632	The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. Theorem 9.9(c) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → (𝐴 /L 𝑁) = (𝐵 /L 𝑁)))
Theorem	lgsmulsqcoprm 25633	The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) → (((𝐴↑2) · 𝐵) /L 𝑁) = (𝐵 /L 𝑁))
Theorem	lgsdirnn0 25634	Variation on lgsdir 25622 valid for all 𝐴, 𝐵 but only for positive 𝑁. (The exact location of the failure of this law is for 𝐴 = 0, 𝐵 < 0, 𝑁 = -1 in which case (0 /L -1) = 1 but (𝐵 /L -1) = -1.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
Theorem	lgsdinn0 25635	Variation on lgsdi 25624 valid for all 𝑀, 𝑁 but only for positive 𝐴. (The exact location of the failure of this law is for 𝐴 = -1, 𝑀 = 0, and some 𝑁 in which case (-1 /L 0) = 1 but (-1 /L 𝑁) = -1 when -1 is not a quadratic residue mod 𝑁.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)))
Theorem	lgsqrlem1 25636	Lemma for lgsqr 25641. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑆 = (Poly1‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = ( deg1 ‘𝑌)    &   ⊢ 𝑂 = (eval1‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ 𝑋 = (var1‘𝑌)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃) = (1 mod 𝑃))    ⇒   ⊢ (𝜑 → ((𝑂‘𝑇)‘(𝐿‘𝐴)) = (0g‘𝑌))
Theorem	lgsqrlem2 25637*	Lemma for lgsqr 25641. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑆 = (Poly1‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = ( deg1 ‘𝑌)    &   ⊢ 𝑂 = (eval1‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ 𝑋 = (var1‘𝑌)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2)))    ⇒   ⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}))
Theorem	lgsqrlem3 25638*	Lemma for lgsqr 25641. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑆 = (Poly1‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = ( deg1 ‘𝑌)    &   ⊢ 𝑂 = (eval1‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ 𝑋 = (var1‘𝑌)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → (𝐴 /L 𝑃) = 1)    ⇒   ⊢ (𝜑 → (𝐿‘𝐴) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}))
Theorem	lgsqrlem4 25639*	Lemma for lgsqr 25641. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑆 = (Poly1‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐷 = ( deg1 ‘𝑌)    &   ⊢ 𝑂 = (eval1‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ 𝑋 = (var1‘𝑌)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    &   ⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → (𝐴 /L 𝑃) = 1)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))
Theorem	lgsqrlem5 25640*	Lemma for lgsqr 25641. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))
Theorem	lgsqr 25641*	The Legendre symbol for odd primes is 1 iff the number is not a multiple of the prime (in which case it is 0, see lgsne0 25625) and the number is a quadratic residue mod 𝑃 (it is -1 for nonresidues by the process of elimination from lgsabs1 25626). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ 𝐴 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))))
Theorem	lgsqrmod 25642*	If the Legendre symbol of an integer for an odd prime is 1, then the number is a quadratic residue mod 𝑃. (Contributed by AV, 20-Aug-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → ∃𝑥 ∈ ℤ ((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃)))
Theorem	lgsqrmodndvds 25643*	If the Legendre symbol of an integer 𝐴 for an odd prime is 1, then the number is a quadratic residue mod 𝑃 with a solution 𝑥 of the congruence (𝑥↑2)≡𝐴 (mod 𝑃) which is not divisible by the prime. (Contributed by AV, 20-Aug-2021.) (Proof shortened by AV, 18-Mar-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → ∃𝑥 ∈ ℤ (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃 ∥ 𝑥)))
Theorem	lgsdchrval 25644*	The Legendre symbol function 𝑋(𝑚) = (𝑚 /L 𝑁), where 𝑁 is an odd positive number, is a Dirichlet character modulo 𝑁. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ 𝑋 = (𝑦 ∈ 𝐵 ↦ (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))))    ⇒   ⊢ (((𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝑋‘(𝐿‘𝐴)) = (𝐴 /L 𝑁))
Theorem	lgsdchr 25645*	The Legendre symbol function 𝑋(𝑚) = (𝑚 /L 𝑁), where 𝑁 is an odd positive number, is a real Dirichlet character modulo 𝑁. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ 𝑋 = (𝑦 ∈ 𝐵 ↦ (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (𝑋 ∈ 𝐷 ∧ 𝑋:𝐵⟶ℝ))
14.4.9  Gauss' Lemma Gauss' Lemma is valid for any integer not dividing the given prime number. In the following, only the special case for 2 (not dividing any odd prime) is proven, see gausslemma2d 25664. The general case is still to prove.
Theorem	gausslemma2dlem0a 25646	Auxiliary lemma 1 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ℕ)
Theorem	gausslemma2dlem0b 25647	Auxiliary lemma 2 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → 𝐻 ∈ ℕ)
Theorem	gausslemma2dlem0c 25648	Auxiliary lemma 3 for gausslemma2d 25664. (Contributed by AV, 13-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1)
Theorem	gausslemma2dlem0d 25649	Auxiliary lemma 4 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → 𝑀 ∈ ℕ0)
Theorem	gausslemma2dlem0e 25650	Auxiliary lemma 5 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2))
Theorem	gausslemma2dlem0f 25651	Auxiliary lemma 6 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻)
Theorem	gausslemma2dlem0g 25652	Auxiliary lemma 7 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → 𝑀 ≤ 𝐻)
Theorem	gausslemma2dlem0h 25653	Auxiliary lemma 8 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	gausslemma2dlem0i 25654	Auxiliary lemma 9 for gausslemma2d 25664. (Contributed by AV, 14-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁)))
Theorem	gausslemma2dlem1a 25655*	Lemma for gausslemma2dlem1 25656. (Contributed by AV, 1-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → ran 𝑅 = (1...𝐻))
Theorem	gausslemma2dlem1 25656*	Lemma 1 for gausslemma2d 25664. (Contributed by AV, 5-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))
Theorem	gausslemma2dlem2 25657*	Lemma 2 for gausslemma2d 25664. (Contributed by AV, 4-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2))
Theorem	gausslemma2dlem3 25658*	Lemma 3 for gausslemma2d 25664. (Contributed by AV, 4-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))
Theorem	gausslemma2dlem4 25659*	Lemma 4 for gausslemma2d 25664. (Contributed by AV, 16-Jun-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))
Theorem	gausslemma2dlem5a 25660*	Lemma for gausslemma2dlem5 25661. (Contributed by AV, 8-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃))
Theorem	gausslemma2dlem5 25661*	Lemma 5 for gausslemma2d 25664. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃))
Theorem	gausslemma2dlem6 25662*	Lemma 6 for gausslemma2d 25664. (Contributed by AV, 16-Jun-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃))
Theorem	gausslemma2dlem7 25663*	Lemma 7 for gausslemma2d 25664. (Contributed by AV, 13-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)
Theorem	gausslemma2d 25664*	Gauss' Lemma (see also theorem 9.6 in [ApostolNT] p. 182) for integer 2: Let p be an odd prime. Let S={2,4,6,...,(p-1)}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (2 /L 𝑃) = (-1↑𝑁))
14.4.10  Quadratic reciprocity
Theorem	lgseisenlem1 25665*	Lemma for lgseisen 25669. If 𝑅(𝑢) = (𝑄 · 𝑢) mod 𝑃 and 𝑀(𝑢) = (-1↑𝑅(𝑢)) · 𝑅(𝑢), then for any even 1 ≤ 𝑢 ≤ 𝑃 − 1, 𝑀(𝑢) is also an even integer 1 ≤ 𝑀(𝑢) ≤ 𝑃 − 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that 𝑀(𝑥 / 2) = (-1↑𝑅(𝑥 / 2)) · 𝑅(𝑥 / 2) / 2 is an integer between 1 and (𝑃 − 1) / 2. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)    &   ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))    ⇒   ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
Theorem	lgseisenlem2 25666*	Lemma for lgseisen 25669. The function 𝑀 is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)    &   ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))    &   ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)    ⇒   ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
Theorem	lgseisenlem3 25667*	Lemma for lgseisen 25669. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)    &   ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))    &   ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝐺 = (mulGrp‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌))
Theorem	lgseisenlem4 25668*	Lemma for lgseisen 25669. The function 𝑀 is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)    &   ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))    &   ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝐺 = (mulGrp‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃))
Theorem	lgseisen 25669*	Eisenstein's lemma, an expression for (𝑃 /L 𝑄) when 𝑃, 𝑄 are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
Theorem	lgsquadlem1 25670*	Lemma for lgsquad 25673. Count the members of 𝑆 with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})))
Theorem	lgsquadlem2 25671*	Lemma for lgsquad 25673. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 25670 to get the total count of lattice points in 𝑆 (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))
Theorem	lgsquadlem3 25672*	Lemma for lgsquad 25673. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁)))
Theorem	lgsquad 25673	The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] p. 185. If 𝑃 and 𝑄 are distinct odd primes, then the product of the Legendre symbols (𝑃 /L 𝑄) and (𝑄 /L 𝑃) is the parity of ((𝑃 − 1) / 2) · ((𝑄 − 1) / 2). This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity. This is Metamath 100 proof #7. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑄 ∈ (ℙ ∖ {2}) ∧ 𝑃 ≠ 𝑄) → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(((𝑃 − 1) / 2) · ((𝑄 − 1) / 2))))
Theorem	lgsquad2lem1 25674	Lemma for lgsquad2 25676. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 𝑀)    &   ⊢ (𝜑 → ((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) = (-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))))    &   ⊢ (𝜑 → ((𝐵 /L 𝑁) · (𝑁 /L 𝐵)) = (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))    ⇒   ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Theorem	lgsquad2lem2 25675*	Lemma for lgsquad2 25676. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))    &   ⊢ (𝜓 ↔ ∀𝑥 ∈ (1...𝑘)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))))    ⇒   ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Theorem	lgsquad2 25676	Extend lgsquad 25673 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Theorem	lgsquad3 25677	Extend lgsquad2 25676 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))
Theorem	m1lgs 25678	The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime 𝑃 iff 𝑃≡1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))
Theorem	2lgslem1a1 25679*	Lemma 1 for 2lgslem1a 25681. (Contributed by AV, 16-Jun-2021.)
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ∀𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑖 · 2) = ((𝑖 · 2) mod 𝑃))
Theorem	2lgslem1a2 25680	Lemma 2 for 2lgslem1a 25681. (Contributed by AV, 18-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → ((⌊‘(𝑁 / 4)) < 𝐼 ↔ (𝑁 / 2) < (𝐼 · 2)))
Theorem	2lgslem1a 25681*	Lemma 1 for 2lgslem1 25684. (Contributed by AV, 18-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)})
Theorem	2lgslem1b 25682*	Lemma 2 for 2lgslem1 25684. (Contributed by AV, 18-Jun-2021.)
⊢ 𝐼 = (𝐴...𝐵)    &   ⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2))    ⇒   ⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)}
Theorem	2lgslem1c 25683	Lemma 3 for 2lgslem1 25684. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2))
Theorem	2lgslem1 25684*	Lemma 1 for 2lgs 25697. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))))
Theorem	2lgslem2 25685	Lemma 2 for 2lgs 25697. (Contributed by AV, 20-Jun-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → 𝑁 ∈ ℤ)
Theorem	2lgslem3a 25686	Lemma for 2lgslem3a1 25690. (Contributed by AV, 14-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 1)) → 𝑁 = (2 · 𝐾))
Theorem	2lgslem3b 25687	Lemma for 2lgslem3b1 25691. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 3)) → 𝑁 = ((2 · 𝐾) + 1))
Theorem	2lgslem3c 25688	Lemma for 2lgslem3c1 25692. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 5)) → 𝑁 = ((2 · 𝐾) + 1))
Theorem	2lgslem3d 25689	Lemma for 2lgslem3d1 25693. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 7)) → 𝑁 = ((2 · 𝐾) + 2))
Theorem	2lgslem3a1 25690	Lemma 1 for 2lgslem3 25694. (Contributed by AV, 15-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 1) → (𝑁 mod 2) = 0)
Theorem	2lgslem3b1 25691	Lemma 2 for 2lgslem3 25694. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 3) → (𝑁 mod 2) = 1)
Theorem	2lgslem3c1 25692	Lemma 3 for 2lgslem3 25694. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 5) → (𝑁 mod 2) = 1)
Theorem	2lgslem3d1 25693	Lemma 4 for 2lgslem3 25694. (Contributed by AV, 15-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 7) → (𝑁 mod 2) = 0)
Theorem	2lgslem3 25694	Lemma 3 for 2lgs 25697. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑁 mod 2) = if((𝑃 mod 8) ∈ {1, 7}, 0, 1))
Theorem	2lgs2 25695	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
⊢ (2 /L 2) = 0
Theorem	2lgslem4 25696	Lemma 4 for 2lgs 25697: special case of 2lgs 25697 for 𝑃 = 2. (Contributed by AV, 20-Jun-2021.)
⊢ ((2 /L 2) = 1 ↔ (2 mod 8) ∈ {1, 7})
Theorem	2lgs 25697	The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime 𝑃 iff 𝑃≡±1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of (𝑁 /L 2) (lgs2 25604) to some degree, by demanding that reciprocity extend to the case 𝑄 = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.)
⊢ (𝑃 ∈ ℙ → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7}))
Theorem	2lgsoddprmlem1 25698	Lemma 1 for 2lgsoddprm 25706. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ((8 · 𝐴) + 𝐵)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 1) / 8)))
Theorem	2lgsoddprmlem2 25699	Lemma 2 for 2lgsoddprm 25706. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8)))
Theorem	2lgsoddprmlem3a 25700	Lemma 1 for 2lgsoddprmlem3 25704. (Contributed by AV, 20-Jul-2021.)
⊢ (((1↑2) − 1) / 8) = 0