P. 163 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pcbcctr 16201*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
Theorem	bcmono 16202	The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
Theorem	bcmax 16203	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁))
Theorem	bcp1ctr 16204	Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → ((2 · (𝑁 + 1))C(𝑁 + 1)) = (((2 · 𝑁)C𝑁) · (2 · (((2 · 𝑁) + 1) / (𝑁 + 1)))))
Theorem	bclbnd 16205	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Theorem	prmefexple 16206	Convert a bound on a power of a prime to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 21-Aug-2026.)
⊢ ((𝐴 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴)))))
Theorem	bpos1lem 16207*	Lemma for bpos1 . (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑)    &   ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑)    &   ⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 · 2) = 𝐵    &   ⊢ 𝐴 < 𝑃    &   ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑)
Theorem	bpos1 16208*	Bertrand's postulate, checked numerically for 𝑁 ≤ 64, using the prime sequence 2, 3, 5, 7, 13, 23, 43, 83. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≤ ;64) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
Theorem	bposlem1 16209	An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
Theorem	bposlem2 16210	There are no odd primes in the range (2𝑁 / 3, 𝑁] dividing the 𝑁-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 2 < 𝑃)    &   ⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = 0)
Theorem	bposlem3 16211*	Lemma for bpos . Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 16210 and prmfac1 12947, respectively, and it does not have any in the range (𝑁, 2𝑁] by hypothesis, the product of the primes up through 2𝑁 / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
Theorem	bposlem4 16212*	Lemma for bpos . (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (3...𝐾))
Theorem	bposlem5 16213*	Lemma for bpos . Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
11.4.5  Quadratic residues and the Legendre symbol If the congruence ((𝑥↑2) mod 𝑝) = (𝑛 mod 𝑝) has a solution we say that 𝑛 is a quadratic residue mod 𝑝. If the congruence has no solution we say that 𝑛 is a quadratic nonresidue mod 𝑝, see definition in [ApostolNT] p. 178. The Legendre symbol (𝑛 /L 𝑝) is defined in a way that its value is 1 if 𝑛 is a quadratic residue mod 𝑝 and -1 if 𝑛 is a quadratic nonresidue mod 𝑝 (and 0 if 𝑝 divides 𝑛). Originally, the Legendre symbol (𝑁 /L 𝑃) was defined for odd primes 𝑃 only (and arbitrary integers 𝑁) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 16215 for the "Legendre symbol" /L is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol".
Syntax	clgs 16214	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 16215*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ /L = (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))))
Theorem	zabsle1 16216	{-1, 0, 1} is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ {-1, 0, 1} ↔ (abs‘𝑍) ≤ 1))
Theorem	lgslem1 16217	When 𝑎 is coprime to the prime 𝑝, 𝑎↑((𝑝 − 1) / 2) is equivalent mod 𝑝 to 1 or -1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2})
Theorem	lgslem2 16218	The set 𝑍 of all integers with absolute value at most 1 contains {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ (-1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍)
Theorem	lgslem3 16219*	The set 𝑍 of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍) → (𝐴 · 𝐵) ∈ 𝑍)
Theorem	lgslem4 16220*	Lemma for lgsfcl2 16223. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
Theorem	lgsval 16221*	Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
Theorem	lgsfvalg 16222*	Value of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝐹‘𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1))
Theorem	lgsfcl2 16223*	The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 16216). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    &   ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶𝑍)
Theorem	lgscllem 16224*	The Legendre symbol is an element of 𝑍. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    &   ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍)
Theorem	lgsfcl 16225*	Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ)
Theorem	lgsfle1 16226*	The function 𝐹 has magnitude less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑀 ∈ ℕ) → (abs‘(𝐹‘𝑀)) ≤ 1)
Theorem	lgsval2lem 16227*	Lemma for lgsval2 16233. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ) → (𝐴 /L 𝑁) = if(𝑁 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑁 − 1) / 2)) + 1) mod 𝑁) − 1)))
Theorem	lgsval4lem 16228*	Lemma for lgsval4 16237. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))
Theorem	lgscl2 16229*	The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍)
Theorem	lgs0 16230	The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
Theorem	lgscl 16231	The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
Theorem	lgsle1 16232	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 16231 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴 /L 𝑁)) ≤ 1)
Theorem	lgsval2 16233	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 16234	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 16235	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 16236	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. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃))
Theorem	lgsval4 16237*	Restate lgsval 16221 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 16238*	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 16239*	Same as lgsval4 16237 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁))
Theorem	lgscl1 16240	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 16241	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 16242	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 16243	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 16244	Lemma for lgsdi 16254 and lgsdir 16252: 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 16245	Lemma for lgsdir2 16250. (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 16246	Lemma for lgsdir2 16250. (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 16247	Lemma for lgsdir2 16250. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))
Theorem	lgsdir2lem4 16248	Lemma for lgsdir2 16250. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7}))
Theorem	lgsdir2lem5 16249	Lemma for lgsdir2 16250. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})
Theorem	lgsdir2 16250	The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2)))
Theorem	lgsdirprm 16251	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 16252	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). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
Theorem	lgsdilem2 16253*	Lemma for lgsdi 16254. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))
Theorem	lgsdi 16254	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 16255	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 16256	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 16257	The Legendre symbol at a square is equal to 1. Together with lgsmod 16243 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 16258	The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1)
Theorem	lgsprme0 16259	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 16260	The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ (𝑁 ∈ ℤ → (1 /L 𝑁) = 1)
Theorem	lgs1 16261	The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 1) = 1)
Theorem	lgsmodeq 16262	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 16263	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 16264	Variation on lgsdir 16252 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 16265	Variation on lgsdi 16254 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 𝑁)))
11.4.6  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 16286. The general case is still to prove.
Theorem	gausslemma2dlem0a 16266	Auxiliary lemma 1 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ℕ)
Theorem	gausslemma2dlem0b 16267	Auxiliary lemma 2 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → 𝐻 ∈ ℕ)
Theorem	gausslemma2dlem0c 16268	Auxiliary lemma 3 for gausslemma2d 16286. (Contributed by AV, 13-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1)
Theorem	gausslemma2dlem0d 16269	Auxiliary lemma 4 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → 𝑀 ∈ ℕ0)
Theorem	gausslemma2dlem0e 16270	Auxiliary lemma 5 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2))
Theorem	gausslemma2dlem0f 16271	Auxiliary lemma 6 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻)
Theorem	gausslemma2dlem0g 16272	Auxiliary lemma 7 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → 𝑀 ≤ 𝐻)
Theorem	gausslemma2dlem0h 16273	Auxiliary lemma 8 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	gausslemma2dlem0i 16274	Auxiliary lemma 9 for gausslemma2d 16286. (Contributed by AV, 14-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁)))
Theorem	gausslemma2dlem1a 16275*	Lemma for gausslemma2dlem1 16278. (Contributed by AV, 1-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → ran 𝑅 = (1...𝐻))
Theorem	gausslemma2dlem1cl 16276	Lemma for gausslemma2dlem1 16278. Closure of the body of the definition of 𝑅. (Contributed by Jim Kingdon, 10-Aug-2025.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝐻))    ⇒   ⊢ (𝜑 → if((𝐴 · 2) < (𝑃 / 2), (𝐴 · 2), (𝑃 − (𝐴 · 2))) ∈ ℤ)
Theorem	gausslemma2dlem1f1o 16277*	Lemma for gausslemma2dlem1 16278. (Contributed by Jim Kingdon, 9-Aug-2025.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → 𝑅:(1...𝐻)–1-1-onto→(1...𝐻))
Theorem	gausslemma2dlem1 16278*	Lemma 1 for gausslemma2d 16286. (Contributed by AV, 5-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))
Theorem	gausslemma2dlem2 16279*	Lemma 2 for gausslemma2d 16286. (Contributed by AV, 4-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2))
Theorem	gausslemma2dlem3 16280*	Lemma 3 for gausslemma2d 16286. (Contributed by AV, 4-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))
Theorem	gausslemma2dlem4 16281*	Lemma 4 for gausslemma2d 16286. (Contributed by AV, 16-Jun-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))
Theorem	gausslemma2dlem5a 16282*	Lemma for gausslemma2dlem5 16283. (Contributed by AV, 8-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃))
Theorem	gausslemma2dlem5 16283*	Lemma 5 for gausslemma2d 16286. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃))
Theorem	gausslemma2dlem6 16284*	Lemma 6 for gausslemma2d 16286. (Contributed by AV, 16-Jun-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃))
Theorem	gausslemma2dlem7 16285*	Lemma 7 for gausslemma2d 16286. (Contributed by AV, 13-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)
Theorem	gausslemma2d 16286*	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↑𝑁))
11.4.7  Quadratic reciprocity
Theorem	lgseisenlem1 16287*	Lemma for lgseisen 16291. 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 16288*	Lemma for lgseisen 16291. 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 16289*	Lemma for lgseisen 16291. (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 16290*	Lemma for lgseisen 16291. (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 16291*	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	lgsquadlemsfi 16292*	Lemma for lgsquad 16297. 𝑆 is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → 𝑆 ∈ Fin)
Theorem	lgsquadlemofi 16293*	Lemma for lgsquad 16297. There are finitely many members of 𝑆 with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)} ∈ Fin)
Theorem	lgsquadlem1 16294*	Lemma for lgsquad 16297. 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 16295*	Lemma for lgsquad 16297. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 16294 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 16296*	Lemma for lgsquad 16297. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁)))
Theorem	lgsquad 16297	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 16298	Lemma for lgsquad2 16300. (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 16299*	Lemma for lgsquad2 16300. (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 16300	Extend lgsquad 16297 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))))