| Metamath
Proof Explorer Theorem List (p. 275 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | gausslemma2dlem0b 27401 | Auxiliary lemma 2 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝐻 ∈ ℕ) | ||
| Theorem | gausslemma2dlem0c 27402 | Auxiliary lemma 3 for gausslemma2d 27418. (Contributed by AV, 13-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1) | ||
| Theorem | gausslemma2dlem0d 27403 | Auxiliary lemma 4 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → 𝑀 ∈ ℕ0) | ||
| Theorem | gausslemma2dlem0e 27404 | Auxiliary lemma 5 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) | ||
| Theorem | gausslemma2dlem0f 27405 | Auxiliary lemma 6 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻) | ||
| Theorem | gausslemma2dlem0g 27406 | Auxiliary lemma 7 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝑀 ≤ 𝐻) | ||
| Theorem | gausslemma2dlem0h 27407 | Auxiliary lemma 8 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ0) | ||
| Theorem | gausslemma2dlem0i 27408 | Auxiliary lemma 9 for gausslemma2d 27418. (Contributed by AV, 14-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) | ||
| Theorem | gausslemma2dlem1a 27409* | Lemma for gausslemma2dlem1 27410. (Contributed by AV, 1-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → ran 𝑅 = (1...𝐻)) | ||
| Theorem | gausslemma2dlem1 27410* | Lemma 1 for gausslemma2d 27418. (Contributed by AV, 5-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) | ||
| Theorem | gausslemma2dlem2 27411* | Lemma 2 for gausslemma2d 27418. (Contributed by AV, 4-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) | ||
| Theorem | gausslemma2dlem3 27412* | Lemma 3 for gausslemma2d 27418. (Contributed by AV, 4-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | ||
| Theorem | gausslemma2dlem4 27413* | Lemma 4 for gausslemma2d 27418. (Contributed by AV, 16-Jun-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) | ||
| Theorem | gausslemma2dlem5a 27414* | Lemma for gausslemma2dlem5 27415. (Contributed by AV, 8-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) | ||
| Theorem | gausslemma2dlem5 27415* | Lemma 5 for gausslemma2d 27418. (Contributed by AV, 9-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) | ||
| Theorem | gausslemma2dlem6 27416* | Lemma 6 for gausslemma2d 27418. (Contributed by AV, 16-Jun-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) | ||
| Theorem | gausslemma2dlem7 27417* | Lemma 7 for gausslemma2d 27418. (Contributed by AV, 13-Jul-2021.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1) | ||
| Theorem | gausslemma2d 27418* | 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 27419* | Lemma for lgseisen 27423. 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 27420* | Lemma for lgseisen 27423. 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 27421* | Lemma for lgseisen 27423. (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 27422* | Lemma for lgseisen 27423. (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 27423* | 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 27424* | Lemma for lgsquad 27427. 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 27425* | Lemma for lgsquad 27427. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 27424 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 27426* | Lemma for lgsquad 27427. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑀 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = ((𝑄 − 1) / 2) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⇒ ⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁))) | ||
| Theorem | lgsquad 27427 | 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 27428 | Lemma for lgsquad2 27430. (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 27429* | Lemma for lgsquad2 27430. (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 27430 | Extend lgsquad 27427 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 27431 | Extend lgsquad2 27430 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀))) | ||
| Theorem | m1lgs 27432 | 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 27433* | Lemma 1 for 2lgslem1a 27435. (Contributed by AV, 16-Jun-2021.) |
| ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ∀𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑖 · 2) = ((𝑖 · 2) mod 𝑃)) | ||
| Theorem | 2lgslem1a2 27434 | Lemma 2 for 2lgslem1a 27435. (Contributed by AV, 18-Jun-2021.) |
| ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → ((⌊‘(𝑁 / 4)) < 𝐼 ↔ (𝑁 / 2) < (𝐼 · 2))) | ||
| Theorem | 2lgslem1a 27435* | Lemma 1 for 2lgslem1 27438. (Contributed by AV, 18-Jun-2021.) |
| ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)}) | ||
| Theorem | 2lgslem1b 27436* | Lemma 2 for 2lgslem1 27438. (Contributed by AV, 18-Jun-2021.) |
| ⊢ 𝐼 = (𝐴...𝐵) & ⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2)) ⇒ ⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} | ||
| Theorem | 2lgslem1c 27437 | Lemma 3 for 2lgslem1 27438. (Contributed by AV, 19-Jun-2021.) |
| ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) | ||
| Theorem | 2lgslem1 27438* | Lemma 1 for 2lgs 27451. (Contributed by AV, 19-Jun-2021.) |
| ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))) | ||
| Theorem | 2lgslem2 27439 | Lemma 2 for 2lgs 27451. (Contributed by AV, 20-Jun-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → 𝑁 ∈ ℤ) | ||
| Theorem | 2lgslem3a 27440 | Lemma for 2lgslem3a1 27444. (Contributed by AV, 14-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 1)) → 𝑁 = (2 · 𝐾)) | ||
| Theorem | 2lgslem3b 27441 | Lemma for 2lgslem3b1 27445. (Contributed by AV, 16-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 3)) → 𝑁 = ((2 · 𝐾) + 1)) | ||
| Theorem | 2lgslem3c 27442 | Lemma for 2lgslem3c1 27446. (Contributed by AV, 16-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 5)) → 𝑁 = ((2 · 𝐾) + 1)) | ||
| Theorem | 2lgslem3d 27443 | Lemma for 2lgslem3d1 27447. (Contributed by AV, 16-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 7)) → 𝑁 = ((2 · 𝐾) + 2)) | ||
| Theorem | 2lgslem3a1 27444 | Lemma 1 for 2lgslem3 27448. (Contributed by AV, 15-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 1) → (𝑁 mod 2) = 0) | ||
| Theorem | 2lgslem3b1 27445 | Lemma 2 for 2lgslem3 27448. (Contributed by AV, 16-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 3) → (𝑁 mod 2) = 1) | ||
| Theorem | 2lgslem3c1 27446 | Lemma 3 for 2lgslem3 27448. (Contributed by AV, 16-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 5) → (𝑁 mod 2) = 1) | ||
| Theorem | 2lgslem3d1 27447 | Lemma 4 for 2lgslem3 27448. (Contributed by AV, 15-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 7) → (𝑁 mod 2) = 0) | ||
| Theorem | 2lgslem3 27448 | Lemma 3 for 2lgs 27451. (Contributed by AV, 16-Jul-2021.) |
| ⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑁 mod 2) = if((𝑃 mod 8) ∈ {1, 7}, 0, 1)) | ||
| Theorem | 2lgs2 27449 | The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.) |
| ⊢ (2 /L 2) = 0 | ||
| Theorem | 2lgslem4 27450 | Lemma 4 for 2lgs 27451: special case of 2lgs 27451 for 𝑃 = 2. (Contributed by AV, 20-Jun-2021.) |
| ⊢ ((2 /L 2) = 1 ↔ (2 mod 8) ∈ {1, 7}) | ||
| Theorem | 2lgs 27451 | The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime 𝑃 iff 𝑃≡±1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of (𝑁 /L 2) (lgs2 27358) to some degree, by demanding that reciprocity extend to the case 𝑄 = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.) |
| ⊢ (𝑃 ∈ ℙ → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7})) | ||
| Theorem | 2lgsoddprmlem1 27452 | Lemma 1 for 2lgsoddprm 27460. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ((8 · 𝐴) + 𝐵)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 1) / 8))) | ||
| Theorem | 2lgsoddprmlem2 27453 | Lemma 2 for 2lgsoddprm 27460. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8))) | ||
| Theorem | 2lgsoddprmlem3a 27454 | Lemma 1 for 2lgsoddprmlem3 27458. (Contributed by AV, 20-Jul-2021.) |
| ⊢ (((1↑2) − 1) / 8) = 0 | ||
| Theorem | 2lgsoddprmlem3b 27455 | Lemma 2 for 2lgsoddprmlem3 27458. (Contributed by AV, 20-Jul-2021.) |
| ⊢ (((3↑2) − 1) / 8) = 1 | ||
| Theorem | 2lgsoddprmlem3c 27456 | Lemma 3 for 2lgsoddprmlem3 27458. (Contributed by AV, 20-Jul-2021.) |
| ⊢ (((5↑2) − 1) / 8) = 3 | ||
| Theorem | 2lgsoddprmlem3d 27457 | Lemma 4 for 2lgsoddprmlem3 27458. (Contributed by AV, 20-Jul-2021.) |
| ⊢ (((7↑2) − 1) / 8) = (2 · 3) | ||
| Theorem | 2lgsoddprmlem3 27458 | Lemma 3 for 2lgsoddprm 27460. (Contributed by AV, 20-Jul-2021.) |
| ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 𝑅 ∈ {1, 7})) | ||
| Theorem | 2lgsoddprmlem4 27459 | Lemma 4 for 2lgsoddprm 27460. (Contributed by AV, 20-Jul-2021.) |
| ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ (𝑁 mod 8) ∈ {1, 7})) | ||
| Theorem | 2lgsoddprm 27460 | The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in [ApostolNT] p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ((2 /L 𝑃) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.) |
| ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 /L 𝑃) = (-1↑(((𝑃↑2) − 1) / 8))) | ||
| Theorem | 2sqlem1 27461* | Lemma for 2sq 27474. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝐴 = ((abs‘𝑥)↑2)) | ||
| Theorem | 2sqlem2 27462* | Lemma for 2sq 27474. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2))) | ||
| Theorem | mul2sq 27463 | Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆) | ||
| Theorem | 2sqlem3 27464 | Lemma for 2sqlem5 27466. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) & ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) & ⊢ (𝜑 → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
| Theorem | 2sqlem4 27465 | Lemma for 2sqlem5 27466. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) & ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
| Theorem | 2sqlem5 27466 | Lemma for 2sq 27474. If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (𝑁 · 𝑃) ∈ 𝑆) & ⊢ (𝜑 → 𝑃 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
| Theorem | 2sqlem6 27467* | Lemma for 2sq 27474. If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)) & ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑆) | ||
| Theorem | 2sqlem7 27468* | Lemma for 2sq 27474. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) | ||
| Theorem | 2sqlem8a 27469* | Lemma for 2sqlem8 27470. (Contributed by Mario Carneiro, 4-Jun-2016.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) & ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2))) & ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ) | ||
| Theorem | 2sqlem8 27470* | Lemma for 2sq 27474. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) & ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2))) & ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷)) & ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷)) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑆) | ||
| Theorem | 2sqlem9 27471* | Lemma for 2sq 27474. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ 𝑌) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑆) | ||
| Theorem | 2sqlem10 27472* | Lemma for 2sq 27474. Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → 𝐵 ∈ 𝑆) | ||
| Theorem | 2sqlem11 27473* | Lemma for 2sq 27474. (Contributed by Mario Carneiro, 19-Jun-2015.) |
| ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) | ||
| Theorem | 2sq 27474* | All primes of the form 4𝑘 + 1 are sums of two squares. This is Metamath 100 proof #20. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2))) | ||
| Theorem | 2sqblem 27475 | Lemma for 2sqb 27476. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2)) & ⊢ (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) & ⊢ (𝜑 → 𝑃 = ((𝑋↑2) + (𝑌↑2))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵))) ⇒ ⊢ (𝜑 → (𝑃 mod 4) = 1) | ||
| Theorem | 2sqb 27476* | The converse to 2sq 27474. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1))) | ||
| Theorem | 2sq2 27477 | 2 is the sum of squares of two nonnegative integers iff the two integers are 1. (Contributed by AV, 19-Jun-2023.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = 2 ↔ (𝐴 = 1 ∧ 𝐵 = 1))) | ||
| Theorem | 2sqn0 27478 | If the sum of two squares is prime, none of the original number is zero. (Contributed by Thierry Arnoux, 4-Feb-2020.) |
| ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
| Theorem | 2sqcoprm 27479 | If the sum of two squares is prime, the two original numbers are coprime. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
| ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | ||
| Theorem | 2sqmod 27480 | Given two decompositions of a prime as a sum of two squares, show that they are equal. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
| ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) & ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | 2sqmo 27481* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 27476 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
| ⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
| Theorem | 2sqnn0 27482* | All primes of the form 4𝑘 + 1 are sums of squares of two nonnegative integers. (Contributed by AV, 3-Jun-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝑃 = ((𝑥↑2) + (𝑦↑2))) | ||
| Theorem | 2sqnn 27483* | All primes of the form 4𝑘 + 1 are sums of squares of two positive integers. (Contributed by AV, 11-Jun-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑃 = ((𝑥↑2) + (𝑦↑2))) | ||
| Theorem | addsq2reu 27484* |
For each complex number 𝐶, there exists a unique complex
number
𝑎 added to the square of a unique
another complex number 𝑏
resulting in the given complex number 𝐶. The unique complex number
𝑎 is 𝐶, and the unique another complex
number 𝑏 is 0.
Remark: This, together with addsqnreup 27487, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑). See also comments for df-eu 2569 and 2eu4 2655. For more details see comment for addsqnreup 27487. (Contributed by AV, 21-Jun-2023.) |
| ⊢ (𝐶 ∈ ℂ → ∃!𝑎 ∈ ℂ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
| Theorem | addsqn2reu 27485* |
For each complex number 𝐶, there does not exist a unique
complex
number 𝑏, squared and added to a unique
another complex number
𝑎 resulting in the given complex number
𝐶.
Actually, for each
complex number 𝑏, 𝑎 = (𝐶 − (𝑏↑2)) is unique.
Remark: This, together with addsq2reu 27484, shows that commutation of two unique quantifications need not be equivalent, and provides an evident justification of the fact that considering the pair of variables is necessary to obtain what we intuitively understand as "double unique existence". (Proposed by GL, 23-Jun-2023.). (Contributed by AV, 23-Jun-2023.) |
| ⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑏 ∈ ℂ ∃!𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
| Theorem | addsqrexnreu 27486* |
For each complex number, there exists a complex number to which the
square of more than one (or no) other complex numbers can be added to
result in the given complex number.
Remark: This theorem, together with addsq2reu 27484, shows that there are cases in which there is a set together with a not unique other set fulfilling a wff, although there is a unique set fulfilling the wff together with another unique set (see addsq2reu 27484). For more details see comment for addsqnreup 27487. (Contributed by AV, 20-Jun-2023.) |
| ⊢ (𝐶 ∈ ℂ → ∃𝑎 ∈ ℂ ¬ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
| Theorem | addsqnreup 27487* |
There is no unique decomposition of a complex number as a sum of a
complex number and a square of a complex number.
Remark: This theorem, together with addsq2reu 27484, is a real life example (about a numerical property) showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑"). See also comments for df-eu 2569 and 2eu4 2655. In the case of decompositions of complex numbers as a sum of a complex number and a square of a complex number, the only/unique complex number to which the square of a unique complex number is added yields in the given complex number is the given number itself, and the unique complex number to be squared is 0 (see comment for addsq2reu 27484). There are, however, complex numbers to which the square of more than one other complex numbers can be added to yield the given complex number (see addsqrexnreu 27486). For example, 〈1, (√‘(𝐶 − 1))〉 and 〈1, -(√‘(𝐶 − 1))〉 are two different decompositions of 𝐶 (if 𝐶 ≠ 1). Therefore, there is no unique decomposition of any complex number as a sum of a complex number and a square of a complex number, as generally proved by this theorem. As a consequence, a theorem must claim the existence of a unique pair of sets to express "There are unique 𝑎 and 𝑏 so that .." (more formally ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 with 𝑝 = 〈𝑎, 𝑏〉), or by showing (∃!𝑥 ∈ 𝐴∃𝑦 ∈ 𝐵𝜑 ∧ ∃!𝑦 ∈ 𝐵∃𝑥 ∈ 𝐴𝜑) (see 2reu4 4523 resp. 2eu4 2655). These two representations are equivalent (see opreu2reurex 6314). An analogon of this theorem using the latter variant is given in addsqn2reurex2 27489. In some cases, however, the variant with (ordered!) pairs may be possible only for ordered sets (like ℝ or ℙ) and claiming that the first component is less than or equal to the second component (see, for example, 2sqreunnltb 27505 and 2sqreuopb 27512). Alternatively, (proper) unordered pairs can be used: ∃!𝑝𝑒𝒫 𝐴((♯‘𝑝) = 2 ∧ 𝜑), or, using the definition of proper pairs: ∃!𝑝 ∈ (Pairsproper‘𝐴)𝜑 (see, for example, inlinecirc02preu 48709). (Contributed by AV, 21-Jun-2023.) |
| ⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶) | ||
| Theorem | addsq2nreurex 27488* | For each complex number 𝐶, there is no unique complex number 𝑎 added to the square of another complex number 𝑏 resulting in the given complex number 𝐶. (Contributed by AV, 2-Jul-2023.) |
| ⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
| Theorem | addsqn2reurex2 27489* |
For each complex number 𝐶, there does not uniquely exist two
complex numbers 𝑎 and 𝑏, with 𝑏 squared
and added to 𝑎
resulting in the given complex number 𝐶.
Remark: This, together with addsq2reu 27484, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑), as it is the case with the pattern (∃!𝑎 ∈ 𝐴∃𝑏 ∈ 𝐵𝜑 ∧ ∃!𝑏 ∈ 𝐵∃𝑎 ∈ 𝐴𝜑. See also comments for df-eu 2569 and 2eu4 2655. (Contributed by AV, 2-Jul-2023.) |
| ⊢ (𝐶 ∈ ℂ → ¬ (∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ∧ ∃!𝑏 ∈ ℂ ∃𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)) | ||
| Theorem | 2sqreulem1 27490* | Lemma 1 for 2sqreu 27500. (Contributed by AV, 4-Jun-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
| Theorem | 2sqreultlem 27491* | Lemma for 2sqreult 27502. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
| Theorem | 2sqreultblem 27492* | Lemma for 2sqreultb 27503. (Contributed by AV, 10-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023.) |
| ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) | ||
| Theorem | 2sqreunnlem1 27493* | Lemma 1 for 2sqreunn 27501. (Contributed by AV, 11-Jun-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
| Theorem | 2sqreunnltlem 27494* | Lemma for 2sqreunnlt 27504. (Contributed by AV, 4-Jun-2023.) Specialization to different integers, proposed by GL. (Revised by AV, 11-Jun-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
| Theorem | 2sqreunnltblem 27495* | Lemma for 2sqreunnltb 27505. (Contributed by AV, 11-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023.) |
| ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) | ||
| Theorem | 2sqreulem2 27496 | Lemma 2 for 2sqreu 27500 etc. (Contributed by AV, 25-Jun-2023.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = ((𝐴↑2) + (𝐶↑2)) → 𝐵 = 𝐶)) | ||
| Theorem | 2sqreulem3 27497 | Lemma 3 for 2sqreu 27500 etc. (Contributed by AV, 25-Jun-2023.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0)) → (((𝜑 ∧ ((𝐴↑2) + (𝐵↑2)) = 𝑃) ∧ (𝜓 ∧ ((𝐴↑2) + (𝐶↑2)) = 𝑃)) → 𝐵 = 𝐶)) | ||
| Theorem | 2sqreulem4 27498* | Lemma 4 for 2sqreu 27500 et. (Contributed by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ∀𝑎 ∈ ℕ0 ∃*𝑏 ∈ ℕ0 𝜑 | ||
| Theorem | 2sqreunnlem2 27499* | Lemma 2 for 2sqreunn 27501. (Contributed by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ∀𝑎 ∈ ℕ ∃*𝑏 ∈ ℕ 𝜑 | ||
| Theorem | 2sqreu 27500* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 27482 for the existence of such a decomposition. (Contributed by AV, 4-Jun-2023.) (Revised by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |