 Home Metamath Proof ExplorerTheorem List (p. 249 of 424) < 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-27159) Hilbert Space Explorer (27160-28684) Users' Mathboxes (28685-42360)

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

Theorempcbcctr 24801* Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))))

Theorembcmono 24802 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𝐵))

Theorembcmax 24803 The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁))

Theorembcp1ctr 24804 Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)
(𝑁 ∈ ℕ0 → ((2 · (𝑁 + 1))C(𝑁 + 1)) = (((2 · 𝑁)C𝑁) · (2 · (((2 · 𝑁) + 1) / (𝑁 + 1)))))

Theorembclbnd 24805 A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
(𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))

Theoremefexple 24806 Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
(((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴𝑁) ≤ 𝐵𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴)))))

Theorembpos1lem 24807* Lemma for bpos1 24808. (Contributed by Mario Carneiro, 12-Mar-2014.)
(∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) → 𝜑)    &   (𝑁 ∈ (ℤ𝑃) → 𝜑)    &   𝑃 ∈ ℙ    &   𝐴 ∈ ℕ0    &   (𝐴 · 2) = 𝐵    &   𝐴 < 𝑃    &   (𝑃 < 𝐵𝑃 = 𝐵)       (𝑁 ∈ (ℤ𝐴) → 𝜑)

Theorembpos1 24808* 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 · 𝑁)))

Theorembposlem1 24809 An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))

Theorembposlem2 24810 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)

Theorembposlem3 24811* Lemma for bpos 24818. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 24810 and prmfac1 15269, 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𝑁))

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

Theorembposlem5 24813* Lemma for bpos 24818. 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 24814* Lemma for bpos 24818. 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 24815* Lemma for bpos 24818. The function 𝐹 is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)
𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   (𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑 → (e↑2) ≤ 𝐴)    &   (𝜑 → (e↑2) ≤ 𝐵)       (𝜑 → (𝐴 < 𝐵 → (𝐹𝐵) < (𝐹𝐴)))

Theorembposlem8 24816 Lemma for bpos 24818. 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 24817* Lemma for bpos 24818. 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 24818* 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 24876.

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 24820 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 24819 Extend class notation with the Legendre symbol function.
class /L

Definitiondf-lgs 24820* 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 24821 {-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 24822 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 24823 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 24824* 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 24825* The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 24821). (Contributed by Mario Carneiro, 4-Feb-2015.)
𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}       ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)

Theoremlgsval 24826* 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 24827* 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 24828* The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 24821). (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 24829* 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 24830* 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 24831* 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 24832* Lemma for lgsval2 24838. (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 24833* Lemma for lgsval4 24842. (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 24834* 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 24835 The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)
(𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))

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

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

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

Theoremlgsval4 24842* Restate lgsval 24826 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 24843* 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 24844* Same as lgsval4 24842 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.)
𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))       ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁))

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

Theoremlgsneg 24846 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 24847 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 24848 The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁))

Theoremlgsdilem 24849 Lemma for lgsdi 24859 and lgsdir 24857: 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 24850 Lemma for lgsdir2 24855. (Contributed by Mario Carneiro, 4-Feb-2015.)
(((1 mod 8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) = 5))

Theoremlgsdir2lem2 24851 Lemma for lgsdir2 24855. (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 24852 Lemma for lgsdir2 24855. (Contributed by Mario Carneiro, 4-Feb-2015.)
((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))

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

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

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

Theoremlgsdirprm 24856 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 24857 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 24876 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 24858* Lemma for lgsdi 24859. (Contributed by Mario Carneiro, 4-Feb-2015.)
(𝜑𝐴 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑀 ≠ 0)    &   (𝜑𝑁 ≠ 0)    &   𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))       (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))

Theoremlgsdi 24859 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 24860 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 24861 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 24862 The Legendre symbol at a square is equal to 1. Together with lgsmod 24848 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 24863 The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.)
((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1)

Theoremlgsprme0 24864 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 24865 The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)
(𝑁 ∈ ℤ → (1 /L 𝑁) = 1)

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

Theoremlgsmodeq 24867 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 24868 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 24869 Variation on lgsdir 24857 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 24870 Variation on lgsdi 24859 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 24871 Lemma for lgsqr 24876. (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 24872* Lemma for lgsqr 24876. (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 24873* Lemma for lgsqr 24876. (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 24874* Lemma for lgsqr 24876. (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 24875* Lemma for lgsqr 24876. (Contributed by Mario Carneiro, 15-Jun-2015.)
((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴))

Theoremlgsqr 24876* 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 24860) and the number is a quadratic residue mod 𝑃 (it is -1 for nonresidues by the process of elimination from lgsabs1 24861). 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 24877* 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 24878* 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 24879* 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 24880* 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 24899. The general case is still to prove.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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