Home | Metamath
Proof Explorer Theorem List (p. 259 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lgslem1 25801 | 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 25802 | 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 25803* | 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 25804* | Lemma for lgsfcl2 25807. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.) |
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍) | ||
Theorem | lgsval 25805* | 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 25806* | 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 25807* | The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 25800). (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 25808* | 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 25809* | 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 25810* | 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 25811* | Lemma for lgsval2 25817. (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 25812* | Lemma for lgsval4 25821. (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 25813* | The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍) | ||
Theorem | lgs0 25814 | 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 25815 | The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ) | ||
Theorem | lgsle1 25816 | The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 25815 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴 /L 𝑁)) ≤ 1) | ||
Theorem | lgsval2 25817 | 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 25818 | 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 25819 | 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 25820 | 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 25855. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) | ||
Theorem | lgsval4 25821* | Restate lgsval 25805 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 25822* | 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 25823* | Same as lgsval4 25821 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁)) | ||
Theorem | lgscl1 25824 | 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 25825 | 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 25826 | 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 25827 | 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 25828 | Lemma for lgsdi 25838 and lgsdir 25836: 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 25829 | Lemma for lgsdir2 25834. (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 25830 | Lemma for lgsdir2 25834. (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 25831 | Lemma for lgsdir2 25834. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5})) | ||
Theorem | lgsdir2lem4 25832 | Lemma for lgsdir2 25834. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7})) | ||
Theorem | lgsdir2lem5 25833 | Lemma for lgsdir2 25834. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7}) | ||
Theorem | lgsdir2 25834 | The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2))) | ||
Theorem | lgsdirprm 25835 | The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) | ||
Theorem | lgsdir 25836 | 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 25855 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 25837* | Lemma for lgsdi 25838. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) ⇒ ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁)))) | ||
Theorem | lgsdi 25838 | 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 25839 | 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 25840 | 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 25841 | The Legendre symbol at a square is equal to 1. Together with lgsmod 25827 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 25842 | The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1) | ||
Theorem | lgsprme0 25843 | 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 25844 | The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ (𝑁 ∈ ℤ → (1 /L 𝑁) = 1) | ||
Theorem | lgs1 25845 | The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ (𝐴 ∈ ℤ → (𝐴 /L 1) = 1) | ||
Theorem | lgsmodeq 25846 | 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 25847 | 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 25848 | Variation on lgsdir 25836 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 25849 | Variation on lgsdi 25838 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 25850 | Lemma for lgsqr 25855. (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 25851* | Lemma for lgsqr 25855. (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 25852* | Lemma for lgsqr 25855. (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 25853* | Lemma for lgsqr 25855. (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 25854* | Lemma for lgsqr 25855. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) | ||
Theorem | lgsqr 25855* | 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 25839) and the number is a quadratic residue mod 𝑃 (it is -1 for nonresidues by the process of elimination from lgsabs1 25840). 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 25856* | 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 25857* | If the Legendre symbol of an integer 𝐴 for an odd prime is 1, then the number is a quadratic residue mod 𝑃 with a solution 𝑥 of the congruence (𝑥↑2)≡𝐴 (mod 𝑃) which is not divisible by the prime. (Contributed by AV, 20-Aug-2021.) (Proof shortened by AV, 18-Mar-2022.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) = 1 → ∃𝑥 ∈ ℤ (((𝑥↑2) mod 𝑃) = (𝐴 mod 𝑃) ∧ ¬ 𝑃 ∥ 𝑥))) | ||
Theorem | lgsdchrval 25858* | 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 25859* | 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 25878. The general case is still to prove. | ||
Theorem | gausslemma2dlem0a 25860 | Auxiliary lemma 1 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) ⇒ ⊢ (𝜑 → 𝑃 ∈ ℕ) | ||
Theorem | gausslemma2dlem0b 25861 | Auxiliary lemma 2 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝐻 ∈ ℕ) | ||
Theorem | gausslemma2dlem0c 25862 | Auxiliary lemma 3 for gausslemma2d 25878. (Contributed by AV, 13-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1) | ||
Theorem | gausslemma2dlem0d 25863 | Auxiliary lemma 4 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → 𝑀 ∈ ℕ0) | ||
Theorem | gausslemma2dlem0e 25864 | Auxiliary lemma 5 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) | ||
Theorem | gausslemma2dlem0f 25865 | Auxiliary lemma 6 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻) | ||
Theorem | gausslemma2dlem0g 25866 | Auxiliary lemma 7 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝑀 ≤ 𝐻) | ||
Theorem | gausslemma2dlem0h 25867 | Auxiliary lemma 8 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ0) | ||
Theorem | gausslemma2dlem0i 25868 | Auxiliary lemma 9 for gausslemma2d 25878. (Contributed by AV, 14-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) | ||
Theorem | gausslemma2dlem1a 25869* | Lemma for gausslemma2dlem1 25870. (Contributed by AV, 1-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → ran 𝑅 = (1...𝐻)) | ||
Theorem | gausslemma2dlem1 25870* | Lemma 1 for gausslemma2d 25878. (Contributed by AV, 5-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) | ||
Theorem | gausslemma2dlem2 25871* | Lemma 2 for gausslemma2d 25878. (Contributed by AV, 4-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) | ||
Theorem | gausslemma2dlem3 25872* | Lemma 3 for gausslemma2d 25878. (Contributed by AV, 4-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | ||
Theorem | gausslemma2dlem4 25873* | Lemma 4 for gausslemma2d 25878. (Contributed by AV, 16-Jun-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) | ||
Theorem | gausslemma2dlem5a 25874* | Lemma for gausslemma2dlem5 25875. (Contributed by AV, 8-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) | ||
Theorem | gausslemma2dlem5 25875* | Lemma 5 for gausslemma2d 25878. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) | ||
Theorem | gausslemma2dlem6 25876* | Lemma 6 for gausslemma2d 25878. (Contributed by AV, 16-Jun-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) | ||
Theorem | gausslemma2dlem7 25877* | Lemma 7 for gausslemma2d 25878. (Contributed by AV, 13-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1) | ||
Theorem | gausslemma2d 25878* | 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 25879* | Lemma for lgseisen 25883. If 𝑅(𝑢) = (𝑄 · 𝑢) mod 𝑃 and 𝑀(𝑢) = (-1↑𝑅(𝑢)) · 𝑅(𝑢), then for any even 1 ≤ 𝑢 ≤ 𝑃 − 1, 𝑀(𝑢) is also an even integer 1 ≤ 𝑀(𝑢) ≤ 𝑃 − 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that 𝑀(𝑥 / 2) = (-1↑𝑅(𝑥 / 2)) · 𝑅(𝑥 / 2) / 2 is an integer between 1 and (𝑃 − 1) / 2. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) & ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) ⇒ ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2))) | ||
Theorem | lgseisenlem2 25880* | Lemma for lgseisen 25883. The function 𝑀 is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) & ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) & ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) ⇒ ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2))) | ||
Theorem | lgseisenlem3 25881* | Lemma for lgseisen 25883. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) & ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) & ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) & ⊢ 𝑌 = (ℤ/nℤ‘𝑃) & ⊢ 𝐺 = (mulGrp‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌)) | ||
Theorem | lgseisenlem4 25882* | Lemma for lgseisen 25883. The function 𝑀 is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) & ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) & ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) & ⊢ 𝑌 = (ℤ/nℤ‘𝑃) & ⊢ 𝐺 = (mulGrp‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃)) | ||
Theorem | lgseisen 25883* | Eisenstein's lemma, an expression for (𝑃 /L 𝑄) when 𝑃, 𝑄 are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | ||
Theorem | lgsquadlem1 25884* | Lemma for lgsquad 25887. Count the members of 𝑆 with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑀 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = ((𝑄 − 1) / 2) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⇒ ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}))) | ||
Theorem | lgsquadlem2 25885* | Lemma for lgsquad 25887. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 25884 to get the total count of lattice points in 𝑆 (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑀 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = ((𝑄 − 1) / 2) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⇒ ⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆))) | ||
Theorem | lgsquadlem3 25886* | Lemma for lgsquad 25887. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑀 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = ((𝑄 − 1) / 2) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⇒ ⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁))) | ||
Theorem | lgsquad 25887 | The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] p. 185. If 𝑃 and 𝑄 are distinct odd primes, then the product of the Legendre symbols (𝑃 /L 𝑄) and (𝑄 /L 𝑃) is the parity of ((𝑃 − 1) / 2) · ((𝑄 − 1) / 2). This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity. This is Metamath 100 proof #7. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑄 ∈ (ℙ ∖ {2}) ∧ 𝑃 ≠ 𝑄) → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(((𝑃 − 1) / 2) · ((𝑄 − 1) / 2)))) | ||
Theorem | lgsquad2lem1 25888 | Lemma for lgsquad2 25890. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑀) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑁) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → (𝐴 · 𝐵) = 𝑀) & ⊢ (𝜑 → ((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) = (-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)))) & ⊢ (𝜑 → ((𝐵 /L 𝑁) · (𝑁 /L 𝐵)) = (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))) ⇒ ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)))) | ||
Theorem | lgsquad2lem2 25889* | Lemma for lgsquad2 25890. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑀) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑁) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2)))) & ⊢ (𝜓 ↔ ∀𝑥 ∈ (1...𝑘)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2))))) ⇒ ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)))) | ||
Theorem | lgsquad2 25890 | Extend lgsquad 25887 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑀) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑁) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)))) | ||
Theorem | lgsquad3 25891 | Extend lgsquad2 25890 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀))) | ||
Theorem | m1lgs 25892 | The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime 𝑃 iff 𝑃≡1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1)) | ||
Theorem | 2lgslem1a1 25893* | Lemma 1 for 2lgslem1a 25895. (Contributed by AV, 16-Jun-2021.) |
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ∀𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑖 · 2) = ((𝑖 · 2) mod 𝑃)) | ||
Theorem | 2lgslem1a2 25894 | Lemma 2 for 2lgslem1a 25895. (Contributed by AV, 18-Jun-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → ((⌊‘(𝑁 / 4)) < 𝐼 ↔ (𝑁 / 2) < (𝐼 · 2))) | ||
Theorem | 2lgslem1a 25895* | Lemma 1 for 2lgslem1 25898. (Contributed by AV, 18-Jun-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)}) | ||
Theorem | 2lgslem1b 25896* | Lemma 2 for 2lgslem1 25898. (Contributed by AV, 18-Jun-2021.) |
⊢ 𝐼 = (𝐴...𝐵) & ⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2)) ⇒ ⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} | ||
Theorem | 2lgslem1c 25897 | Lemma 3 for 2lgslem1 25898. (Contributed by AV, 19-Jun-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) | ||
Theorem | 2lgslem1 25898* | Lemma 1 for 2lgs 25911. (Contributed by AV, 19-Jun-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))) | ||
Theorem | 2lgslem2 25899 | Lemma 2 for 2lgs 25911. (Contributed by AV, 20-Jun-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → 𝑁 ∈ ℤ) | ||
Theorem | 2lgslem3a 25900 | Lemma for 2lgslem3a1 25904. (Contributed by AV, 14-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 1)) → 𝑁 = (2 · 𝐾)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |