 Home Metamath Proof ExplorerTheorem List (p. 248 of 425) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-26947) Hilbert Space Explorer (26948-28472) Users' Mathboxes (28473-42426)

Theorem List for Metamath Proof Explorer - 24701-24800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorembposlem4 24701* Lemma for bpos 24707. (Contributed by Mario Carneiro, 13-Mar-2014.)
(𝜑𝑁 ∈ (ℤ‘5))    &   (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))    &   𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   𝐾 = (⌊‘((2 · 𝑁) / 3))    &   𝑀 = (⌊‘(√‘(2 · 𝑁)))       (𝜑𝑀 ∈ (3...𝐾))

Theorembposlem5 24702* Lemma for bpos 24707. 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)))

Theorembposlem6 24703* Lemma for bpos 24707. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)
(𝜑𝑁 ∈ (ℤ‘5))    &   (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))    &   𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   𝐾 = (⌊‘((2 · 𝑁) / 3))    &   𝑀 = (⌊‘(√‘(2 · 𝑁)))       (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))

Theorembposlem7 24704* Lemma for bpos 24707. The function 𝐹 is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)
𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   (𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑 → (e↑2) ≤ 𝐴)    &   (𝜑 → (e↑2) ≤ 𝐵)       (𝜑 → (𝐴 < 𝐵 → (𝐹𝐵) < (𝐹𝐴)))

Theorembposlem8 24705 Lemma for bpos 24707. Evaluate 𝐹(64) and show it is less than log2. (Contributed by Mario Carneiro, 14-Mar-2014.)
𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))       ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))

Theorembposlem9 24706* Lemma for bpos 24707. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑64 < 𝑁)    &   (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))       (𝜑𝜓)

Theorembpos 24707* Bertrand's postulate: there is a prime between 𝑁 and 2𝑁 for every positive integer 𝑁. This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014.)
(𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))

14.4.8  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 𝑛), see lgsqr 24765.

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 24709 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".

Syntaxclgs 24708 Extend class notation with the Legendre symbol function.
class /L

Definitiondf-lgs 24709* 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‘𝑛)))))

Theoremzabsle1 24710 {-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))

Theoremlgslem1 24711 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})

Theoremlgslem2 24712 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 ∈ 𝑍)

Theoremlgslem3 24713* The set 𝑍 of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}       ((𝐴𝑍𝐵𝑍) → (𝐴 · 𝐵) ∈ 𝑍)

Theoremlgslem4 24714* The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 24710). (Contributed by Mario Carneiro, 4-Feb-2015.)
𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}       ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)

Theoremlgsval 24715* 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‘𝑁)))))

Theoremlgsfval 24716* Value 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))       (𝑀 ∈ ℕ → (𝐹𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1))

Theoremlgsfcl2 24717* The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 24710). (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) → 𝐹:ℕ⟶𝑍)

Theoremlgscllem 24718* 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 𝑁) ∈ 𝑍)

Theoremlgsfcl 24719* 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) → 𝐹:ℕ⟶ℤ)

Theoremlgsfle1 24720* 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)

Theoremlgsval2lem 24721* Lemma for lgsval2 24727. (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)))

Theoremlgsval4lem 24722* Lemma for lgsval4 24731. (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)))

Theoremlgscl2 24723* The Legendre symbol is an integer with absolute value less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}       ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍)

Theoremlgs0 24724 The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)
(𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))

Theoremlgscl 24725 The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)

Theoremlgsle1 24726 The Legendre symbol has absolute value less or equal to 1. Together with lgscl 24725 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴 /L 𝑁)) ≤ 1)

Theoremlgsval2 24727 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)))

Theoremlgs2 24728 The Legendre symbol at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
(𝐴 ∈ ℤ → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))

Theoremlgsval3 24729 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))

Theoremlgsvalmod 24730 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 24765. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃))

Theoremlgsval4 24731* Restate lgsval 24715 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‘𝑁))))

Theoremlgsfcl3 24732* Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))       ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ)

Theoremlgsval4a 24733* Same as lgsval4 24731 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.)
𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))       ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁))

Theoremlgscl1 24734 The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ {-1, 0, 1})

Theoremlgsneg 24735 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 𝑁)))

Theoremlgsneg1 24736 The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℕ0𝑁 ∈ ℤ) → (𝐴 /L -𝑁) = (𝐴 /L 𝑁))

Theoremlgsmod 24737 The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁))

Theoremlgsdilem 24738 Lemma for lgsdi 24748 and lgsdir 24746: 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)))

Theoremlgsdir2lem1 24739 Lemma for lgsdir2 24744. (Contributed by Mario Carneiro, 4-Feb-2015.)
(((1 mod 8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) = 5))

Theoremlgsdir2lem2 24740 Lemma for lgsdir2 24744. (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) ∈ 𝑆)))

Theoremlgsdir2lem3 24741 Lemma for lgsdir2 24744. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))

Theoremlgsdir2lem4 24742 Lemma for lgsdir2 24744. (Contributed by Mario Carneiro, 4-Feb-2015.)
(((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7}))

Theoremlgsdir2lem5 24743 Lemma for lgsdir2 24744. (Contributed by Mario Carneiro, 4-Feb-2015.)
(((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})

Theoremlgsdir2 24744 The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2)))

Theoremlgsdirprm 24745 The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))

Theoremlgsdir 24746 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 24765 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 𝑁)))

Theoremlgsdilem2 24747* Lemma for lgsdi 24748. (Contributed by Mario Carneiro, 4-Feb-2015.)
(𝜑𝐴 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑀 ≠ 0)    &   (𝜑𝑁 ≠ 0)    &   𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))       (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))

Theoremlgsdi 24748 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 𝑁)))

Theoremlgsne0 24749 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))

Theoremlgsabs1 24750 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))

Theoremlgssq 24751 The Legendre symbol at a square is equal to 1. Together with lgsmod 24737 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)

Theoremlgssq2 24752 The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1)

Theoremlgsprme0 24753 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))

Theorem1lgs 24754 The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)
(𝑁 ∈ ℤ → (1 /L 𝑁) = 1)

Theoremlgs1 24755 The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.)
(𝐴 ∈ ℤ → (𝐴 /L 1) = 1)

Theoremlgsmodeq 24756 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 𝑁)))

Theoremlgsmulsqcoprm 24757 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 𝑁))

Theoremlgsdirnn0 24758 Variation on lgsdir 24746 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 𝑁)))

Theoremlgsdinn0 24759 Variation on lgsdi 24748 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 𝑁)))

Theoremlgsqrlem1 24760 Lemma for lgsqr 24765. (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𝑌))

Theoremlgsqrlem2 24761* Lemma for lgsqr 24765. (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𝑌)}))

Theoremlgsqrlem3 24762* Lemma for lgsqr 24765. (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𝑌)}))

Theoremlgsqrlem4 24763* Lemma for lgsqr 24765. (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) − 𝐴))

Theoremlgsqrlem5 24764* Lemma for lgsqr 24765. (Contributed by Mario Carneiro, 15-Jun-2015.)
((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))

Theoremlgsqr 24765* 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 24749) and the number is a quadratic residue mod 𝑃 (it is -1 for nonresidues by the process of elimination from lgsabs1 24750). 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) − 𝐴))))

Theoremlgsqrmod 24766* 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 𝑃)))

Theoremlgsqrmodndvds 24767* 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.)
((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → ∃𝑥 ∈ ℤ (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃𝑥)))

Theoremlgsdchrval 24768* 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 𝑁))

Theoremlgsdchr 24769* 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 24788. The general case is still to prove.

Theoremgausslemma2dlem0a 24770 Auxiliary lemma 1 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))       (𝜑𝑃 ∈ ℕ)

Theoremgausslemma2dlem0b 24771 Auxiliary lemma 2 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)       (𝜑𝐻 ∈ ℕ)

Theoremgausslemma2dlem0c 24772 Auxiliary lemma 3 for gausslemma2d 24788. (Contributed by AV, 13-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)       (𝜑 → ((!‘𝐻) gcd 𝑃) = 1)

Theoremgausslemma2dlem0d 24773 Auxiliary lemma 4 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝑀 = (⌊‘(𝑃 / 4))       (𝜑𝑀 ∈ ℕ0)

Theoremgausslemma2dlem0e 24774 Auxiliary lemma 5 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝑀 = (⌊‘(𝑃 / 4))       (𝜑 → (𝑀 · 2) < (𝑃 / 2))

Theoremgausslemma2dlem0f 24775 Auxiliary lemma 6 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝐻 = ((𝑃 − 1) / 2)       (𝜑 → (𝑀 + 1) ≤ 𝐻)

Theoremgausslemma2dlem0g 24776 Auxiliary lemma 7 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝐻 = ((𝑃 − 1) / 2)       (𝜑𝑀𝐻)

Theoremgausslemma2dlem0h 24777 Auxiliary lemma 8 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑁 = (𝐻𝑀)       (𝜑𝑁 ∈ ℕ0)

Theoremgausslemma2dlem0i 24778 Auxiliary lemma 9 for gausslemma2d 24788. (Contributed by AV, 14-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑁 = (𝐻𝑀)       (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁)))

Theoremgausslemma2dlem1a 24779* Lemma for gausslemma2dlem1 24780. (Contributed by AV, 1-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))       (𝜑 → ran 𝑅 = (1...𝐻))

Theoremgausslemma2dlem1 24780* Lemma 1 for gausslemma2d 24788. (Contributed by AV, 5-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))       (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅𝑘))

Theoremgausslemma2dlem2 24781* Lemma 2 for gausslemma2d 24788. (Contributed by AV, 4-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))       (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅𝑘) = (𝑘 · 2))

Theoremgausslemma2dlem3 24782* Lemma 3 for gausslemma2d 24788. (Contributed by AV, 4-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))       (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅𝑘) = (𝑃 − (𝑘 · 2)))

Theoremgausslemma2dlem4 24783* Lemma 4 for gausslemma2d 24788. (Contributed by AV, 16-Jun-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))       (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅𝑘)))

Theoremgausslemma2dlem5a 24784* Lemma for gausslemma2dlem5 24785. (Contributed by AV, 8-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))       (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃))

Theoremgausslemma2dlem5 24785* Lemma 5 for gausslemma2d 24788. (Contributed by AV, 9-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝑁 = (𝐻𝑀)       (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃))

Theoremgausslemma2dlem6 24786* Lemma 6 for gausslemma2d 24788. (Contributed by AV, 16-Jun-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝑁 = (𝐻𝑀)       (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃))

Theoremgausslemma2dlem7 24787* Lemma 7 for gausslemma2d 24788. (Contributed by AV, 13-Jul-2021.)
(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   𝑀 = (⌊‘(𝑃 / 4))    &   𝑁 = (𝐻𝑀)       (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)

Theoremgausslemma2d 24788* 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↑𝑁))

Theoremlgseisenlem1 24789* Lemma for lgseisen 24793. 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)))

Theoremlgseisenlem2 24790* Lemma for lgseisen 24793. 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)))

Theoremlgseisenlem3 24791* Lemma for lgseisen 24793. (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𝑌))

Theoremlgseisenlem4 24792* Lemma for lgseisen 24793. 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 𝑃))

Theoremlgseisen 24793* 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 · 𝑥)))))

Theoremlgsquadlem1 24794* Lemma for lgsquad 24797. 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𝑧)})))

Theoremlgsquadlem2 24795* Lemma for lgsquad 24797. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 24794 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↑(#‘𝑆)))

(𝜑𝑃 ∈ (ℙ ∖ {2}))    &   (𝜑𝑄 ∈ (ℙ ∖ {2}))    &   (𝜑𝑃𝑄)    &   𝑀 = ((𝑃 − 1) / 2)    &   𝑁 = ((𝑄 − 1) / 2)    &   𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}       (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁)))

Theoremlgsquad 24797 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))))