Home | Metamath
Proof Explorer Theorem 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) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pcbcctr 24801* | Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))))) | ||
Theorem | bcmono 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𝐵)) | ||
Theorem | bcmax 24803 | The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) | ||
Theorem | bcp1ctr 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))))) | ||
Theorem | bclbnd 24805 | A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) | ||
Theorem | efexple 24806 | Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴))))) | ||
Theorem | bpos1lem 24807* | Lemma for bpos1 24808. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑) & ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑) & ⊢ 𝑃 ∈ ℙ & ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 · 2) = 𝐵 & ⊢ 𝐴 < 𝑃 & ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑) | ||
Theorem | bpos1 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 · 𝑁))) | ||
Theorem | bposlem1 24809 | 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 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) | ||
Theorem | bposlem3 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𝑁)) | ||
Theorem | bposlem4 24812* | Lemma for bpos 24818. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5)) & ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) & ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3)) & ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁))) ⇒ ⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) | ||
Theorem | bposlem5 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))) | ||
Theorem | bposlem6 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)))) | ||
Theorem | bposlem7 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) ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 → (𝐹‘𝐵) < (𝐹‘𝐴))) | ||
Theorem | bposlem8 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)) | ||
Theorem | bposlem9 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 · 𝑁))) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bpos 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 · 𝑁))) | ||
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". | ||
Syntax | clgs 24819 | Extend class notation with the Legendre symbol function. |
class /L | ||
Definition | df-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‘𝑛))))) | ||
Theorem | zabsle1 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)) | ||
Theorem | lgslem1 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}) | ||
Theorem | lgslem2 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 ∈ 𝑍) | ||
Theorem | lgslem3 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} ⇒ ⊢ ((𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍) → (𝐴 · 𝐵) ∈ 𝑍) | ||
Theorem | lgslem4 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) ∈ 𝑍) | ||
Theorem | lgsval 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‘𝑁))))) | ||
Theorem | lgsfval 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)) | ||
Theorem | lgsfcl2 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) → 𝐹:ℕ⟶𝑍) | ||
Theorem | lgscllem 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 𝑁) ∈ 𝑍) | ||
Theorem | lgsfcl 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) → 𝐹:ℕ⟶ℤ) | ||
Theorem | lgsfle1 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) | ||
Theorem | lgsval2lem 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))) | ||
Theorem | lgsval4lem 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))) | ||
Theorem | lgscl2 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 𝑁) ∈ 𝑍) | ||
Theorem | lgs0 24835 | 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 24836 | The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ) | ||
Theorem | lgsle1 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) | ||
Theorem | lgsval2 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))) | ||
Theorem | lgs2 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))) | ||
Theorem | lgsval3 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)) | ||
Theorem | lgsvalmod 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 𝑃)) | ||
Theorem | lgsval4 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‘𝑁)))) | ||
Theorem | lgsfcl3 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) → 𝐹:ℕ⟶ℤ) | ||
Theorem | lgsval4a 24844* | Same as lgsval4 24842 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁)) | ||
Theorem | lgscl1 24845 | 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 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 𝑁))) | ||
Theorem | lgsneg1 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 𝑁)) | ||
Theorem | lgsmod 24848 | 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 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))) | ||
Theorem | lgsdir2lem1 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)) | ||
Theorem | lgsdir2lem2 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) ∈ 𝑆))) | ||
Theorem | lgsdir2lem3 24852 | Lemma for lgsdir2 24855. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5})) | ||
Theorem | lgsdir2lem4 24853 | Lemma for lgsdir2 24855. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7})) | ||
Theorem | lgsdir2lem5 24854 | Lemma for lgsdir2 24855. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7}) | ||
Theorem | lgsdir2 24855 | The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2))) | ||
Theorem | lgsdirprm 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 𝑃))) | ||
Theorem | lgsdir 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 𝑁))) | ||
Theorem | lgsdilem2 24858* | Lemma for lgsdi 24859. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) ⇒ ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁)))) | ||
Theorem | lgsdi 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 𝑁))) | ||
Theorem | lgsne0 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)) | ||
Theorem | lgsabs1 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)) | ||
Theorem | lgssq 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) | ||
Theorem | lgssq2 24863 | The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1) | ||
Theorem | lgsprme0 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)) | ||
Theorem | 1lgs 24865 | The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ (𝑁 ∈ ℤ → (1 /L 𝑁) = 1) | ||
Theorem | lgs1 24866 | The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ (𝐴 ∈ ℤ → (𝐴 /L 1) = 1) | ||
Theorem | lgsmodeq 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 𝑁))) | ||
Theorem | lgsmulsqcoprm 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 𝑁)) | ||
Theorem | lgsdirnn0 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 𝑁))) | ||
Theorem | lgsdinn0 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 𝑁))) | ||
Theorem | lgsqrlem1 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‘𝑌)) | ||
Theorem | lgsqrlem2 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‘𝑌)})) | ||
Theorem | lgsqrlem3 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‘𝑌)})) | ||
Theorem | lgsqrlem4 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) − 𝐴)) | ||
Theorem | lgsqrlem5 24875* | Lemma for lgsqr 24876. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) | ||
Theorem | lgsqr 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) − 𝐴)))) | ||
Theorem | lgsqrmod 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 𝑃))) | ||
Theorem | lgsqrmodndvds 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 𝑃) ∧ ¬ 𝑃 ∥ 𝑥))) | ||
Theorem | lgsdchrval 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 𝑁)) | ||
Theorem | lgsdchr 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 ∥ 𝑁) → (𝑋 ∈ 𝐷 ∧ 𝑋:𝐵⟶ℝ)) | ||
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. | ||
Theorem | gausslemma2dlem0a 24881 | Auxiliary lemma 1 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) ⇒ ⊢ (𝜑 → 𝑃 ∈ ℕ) | ||
Theorem | gausslemma2dlem0b 24882 | Auxiliary lemma 2 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝐻 ∈ ℕ) | ||
Theorem | gausslemma2dlem0c 24883 | Auxiliary lemma 3 for gausslemma2d 24899. (Contributed by AV, 13-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1) | ||
Theorem | gausslemma2dlem0d 24884 | Auxiliary lemma 4 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → 𝑀 ∈ ℕ0) | ||
Theorem | gausslemma2dlem0e 24885 | Auxiliary lemma 5 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) | ||
Theorem | gausslemma2dlem0f 24886 | Auxiliary lemma 6 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻) | ||
Theorem | gausslemma2dlem0g 24887 | Auxiliary lemma 7 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝑀 ≤ 𝐻) | ||
Theorem | gausslemma2dlem0h 24888 | Auxiliary lemma 8 for gausslemma2d 24899. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ0) | ||
Theorem | gausslemma2dlem0i 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↑𝑁))) | ||
Theorem | gausslemma2dlem1a 24890* | Lemma for gausslemma2dlem1 24891. (Contributed by AV, 1-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → ran 𝑅 = (1...𝐻)) | ||
Theorem | gausslemma2dlem1 24891* | Lemma 1 for gausslemma2d 24899. (Contributed by AV, 5-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) | ||
Theorem | gausslemma2dlem2 24892* | Lemma 2 for gausslemma2d 24899. (Contributed by AV, 4-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) | ||
Theorem | gausslemma2dlem3 24893* | Lemma 3 for gausslemma2d 24899. (Contributed by AV, 4-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | ||
Theorem | gausslemma2dlem4 24894* | Lemma 4 for gausslemma2d 24899. (Contributed by AV, 16-Jun-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) | ||
Theorem | gausslemma2dlem5a 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 𝑃)) | ||
Theorem | gausslemma2dlem5 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 𝑃)) | ||
Theorem | gausslemma2dlem6 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 𝑃)) | ||
Theorem | gausslemma2dlem7 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) | ||
Theorem | gausslemma2d 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↑𝑁)) | ||
Theorem | lgseisenlem1 24900* | Lemma for lgseisen 24904. 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))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |