P. 274 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27301-27400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gausslemma2dlem0g 27301	Auxiliary lemma 7 for gausslemma2d 27313. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    ⇒   ⊢ (𝜑 → 𝑀 ≤ 𝐻)
Theorem	gausslemma2dlem0h 27302	Auxiliary lemma 8 for gausslemma2d 27313. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	gausslemma2dlem0i 27303	Auxiliary lemma 9 for gausslemma2d 27313. (Contributed by AV, 14-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁)))
Theorem	gausslemma2dlem1a 27304*	Lemma for gausslemma2dlem1 27305. (Contributed by AV, 1-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → ran 𝑅 = (1...𝐻))
Theorem	gausslemma2dlem1 27305*	Lemma 1 for gausslemma2d 27313. (Contributed by AV, 5-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))
Theorem	gausslemma2dlem2 27306*	Lemma 2 for gausslemma2d 27313. (Contributed by AV, 4-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2))
Theorem	gausslemma2dlem3 27307*	Lemma 3 for gausslemma2d 27313. (Contributed by AV, 4-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))
Theorem	gausslemma2dlem4 27308*	Lemma 4 for gausslemma2d 27313. (Contributed by AV, 16-Jun-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))
Theorem	gausslemma2dlem5a 27309*	Lemma for gausslemma2dlem5 27310. (Contributed by AV, 8-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃))
Theorem	gausslemma2dlem5 27310*	Lemma 5 for gausslemma2d 27313. (Contributed by AV, 9-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃))
Theorem	gausslemma2dlem6 27311*	Lemma 6 for gausslemma2d 27313. (Contributed by AV, 16-Jun-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃))
Theorem	gausslemma2dlem7 27312*	Lemma 7 for gausslemma2d 27313. (Contributed by AV, 13-Jul-2021.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ 𝐻 = ((𝑃 − 1) / 2)    &   ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   ⊢ 𝑀 = (⌊‘(𝑃 / 4))    &   ⊢ 𝑁 = (𝐻 − 𝑀)    ⇒   ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)
Theorem	gausslemma2d 27313*	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↑𝑁))
14.4.10  Quadratic reciprocity
Theorem	lgseisenlem1 27314*	Lemma for lgseisen 27318. 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 27315*	Lemma for lgseisen 27318. 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 27316*	Lemma for lgseisen 27318. (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 27317*	Lemma for lgseisen 27318. (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 27318*	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 27319*	Lemma for lgsquad 27322. 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 27320*	Lemma for lgsquad 27322. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 27319 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 27321*	Lemma for lgsquad 27322. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ 𝑀 = ((𝑃 − 1) / 2)    &   ⊢ 𝑁 = ((𝑄 − 1) / 2)    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   ⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁)))
Theorem	lgsquad 27322	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 27323	Lemma for lgsquad2 27325. (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 27324*	Lemma for lgsquad2 27325. (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 27325	Extend lgsquad 27322 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 27326	Extend lgsquad2 27325 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))
Theorem	m1lgs 27327	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 27328*	Lemma 1 for 2lgslem1a 27330. (Contributed by AV, 16-Jun-2021.)
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ∀𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑖 · 2) = ((𝑖 · 2) mod 𝑃))
Theorem	2lgslem1a2 27329	Lemma 2 for 2lgslem1a 27330. (Contributed by AV, 18-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → ((⌊‘(𝑁 / 4)) < 𝐼 ↔ (𝑁 / 2) < (𝐼 · 2)))
Theorem	2lgslem1a 27330*	Lemma 1 for 2lgslem1 27333. (Contributed by AV, 18-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)})
Theorem	2lgslem1b 27331*	Lemma 2 for 2lgslem1 27333. (Contributed by AV, 18-Jun-2021.)
⊢ 𝐼 = (𝐴...𝐵)    &   ⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2))    ⇒   ⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)}
Theorem	2lgslem1c 27332	Lemma 3 for 2lgslem1 27333. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2))
Theorem	2lgslem1 27333*	Lemma 1 for 2lgs 27346. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))))
Theorem	2lgslem2 27334	Lemma 2 for 2lgs 27346. (Contributed by AV, 20-Jun-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → 𝑁 ∈ ℤ)
Theorem	2lgslem3a 27335	Lemma for 2lgslem3a1 27339. (Contributed by AV, 14-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 1)) → 𝑁 = (2 · 𝐾))
Theorem	2lgslem3b 27336	Lemma for 2lgslem3b1 27340. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 3)) → 𝑁 = ((2 · 𝐾) + 1))
Theorem	2lgslem3c 27337	Lemma for 2lgslem3c1 27341. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 5)) → 𝑁 = ((2 · 𝐾) + 1))
Theorem	2lgslem3d 27338	Lemma for 2lgslem3d1 27342. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 7)) → 𝑁 = ((2 · 𝐾) + 2))
Theorem	2lgslem3a1 27339	Lemma 1 for 2lgslem3 27343. (Contributed by AV, 15-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 1) → (𝑁 mod 2) = 0)
Theorem	2lgslem3b1 27340	Lemma 2 for 2lgslem3 27343. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 3) → (𝑁 mod 2) = 1)
Theorem	2lgslem3c1 27341	Lemma 3 for 2lgslem3 27343. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 5) → (𝑁 mod 2) = 1)
Theorem	2lgslem3d1 27342	Lemma 4 for 2lgslem3 27343. (Contributed by AV, 15-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 7) → (𝑁 mod 2) = 0)
Theorem	2lgslem3 27343	Lemma 3 for 2lgs 27346. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑁 mod 2) = if((𝑃 mod 8) ∈ {1, 7}, 0, 1))
Theorem	2lgs2 27344	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
⊢ (2 /L 2) = 0
Theorem	2lgslem4 27345	Lemma 4 for 2lgs 27346: special case of 2lgs 27346 for 𝑃 = 2. (Contributed by AV, 20-Jun-2021.)
⊢ ((2 /L 2) = 1 ↔ (2 mod 8) ∈ {1, 7})
Theorem	2lgs 27346	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 27253) 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 27347	Lemma 1 for 2lgsoddprm 27355. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ((8 · 𝐴) + 𝐵)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 1) / 8)))
Theorem	2lgsoddprmlem2 27348	Lemma 2 for 2lgsoddprm 27355. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8)))
Theorem	2lgsoddprmlem3a 27349	Lemma 1 for 2lgsoddprmlem3 27353. (Contributed by AV, 20-Jul-2021.)
⊢ (((1↑2) − 1) / 8) = 0
Theorem	2lgsoddprmlem3b 27350	Lemma 2 for 2lgsoddprmlem3 27353. (Contributed by AV, 20-Jul-2021.)
⊢ (((3↑2) − 1) / 8) = 1
Theorem	2lgsoddprmlem3c 27351	Lemma 3 for 2lgsoddprmlem3 27353. (Contributed by AV, 20-Jul-2021.)
⊢ (((5↑2) − 1) / 8) = 3
Theorem	2lgsoddprmlem3d 27352	Lemma 4 for 2lgsoddprmlem3 27353. (Contributed by AV, 20-Jul-2021.)
⊢ (((7↑2) − 1) / 8) = (2 · 3)
Theorem	2lgsoddprmlem3 27353	Lemma 3 for 2lgsoddprm 27355. (Contributed by AV, 20-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 𝑅 ∈ {1, 7}))
Theorem	2lgsoddprmlem4 27354	Lemma 4 for 2lgsoddprm 27355. (Contributed by AV, 20-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ (𝑁 mod 8) ∈ {1, 7}))
Theorem	2lgsoddprm 27355	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)))
14.4.11  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 27356*	Lemma for 2sq 27369. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝐴 = ((abs‘𝑥)↑2))
Theorem	2sqlem2 27357*	Lemma for 2sq 27369. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2)))
Theorem	mul2sq 27358	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 27359	Lemma for 2sqlem5 27361. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))    &   ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2)))    &   ⊢ (𝜑 → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑆)
Theorem	2sqlem4 27360	Lemma for 2sqlem5 27361. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))    &   ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑆)
Theorem	2sqlem5 27361	Lemma for 2sq 27369. 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 27362*	Lemma for 2sq 27369. 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 27363*	Lemma for 2sq 27369. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    ⇒   ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
Theorem	2sqlem8a 27364*	Lemma for 2sqlem8 27365. (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 27365*	Lemma for 2sq 27369. (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 27366*	Lemma for 2sq 27369. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑆)
Theorem	2sqlem10 27367*	Lemma for 2sq 27369. 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 27368*	Lemma for 2sq 27369. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆)
Theorem	2sq 27369*	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 27370	Lemma for 2sqb 27371. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))    &   ⊢ (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))    &   ⊢ (𝜑 → 𝑃 = ((𝑋↑2) + (𝑌↑2)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵)))    ⇒   ⊢ (𝜑 → (𝑃 mod 4) = 1)
Theorem	2sqb 27371*	The converse to 2sq 27369. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1)))
Theorem	2sq2 27372	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 27373	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 27374	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 27375	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 27376*	There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 27371 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqnn0 27377*	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 27378*	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 27379*	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 27382, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑). See also comments for df-eu 2566 and 2eu4 2652. For more details see comment for addsqnreup 27382. (Contributed by AV, 21-Jun-2023.)
⊢ (𝐶 ∈ ℂ → ∃!𝑎 ∈ ℂ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)
Theorem	addsqn2reu 27380*	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 27379, 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 27381*	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 27379, 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 27379). For more details see comment for addsqnreup 27382. (Contributed by AV, 20-Jun-2023.)
⊢ (𝐶 ∈ ℂ → ∃𝑎 ∈ ℂ ¬ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)
Theorem	addsqnreup 27382*	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 27379, 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 2566 and 2eu4 2652. 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 27379). 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 27381). 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 4472 resp. 2eu4 2652). These two representations are equivalent (see opreu2reurex 6246). An analogon of this theorem using the latter variant is given in addsqn2reurex2 27384. 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 27400 and 2sqreuopb 27407). Alternatively, (proper) unordered pairs can be used: ∃!𝑝𝑒𝒫 𝐴((♯‘𝑝) = 2 ∧ 𝜑), or, using the definition of proper pairs: ∃!𝑝 ∈ (Pairsproper‘𝐴)𝜑 (see, for example, inlinecirc02preu 48913). (Contributed by AV, 21-Jun-2023.)
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)
Theorem	addsq2nreurex 27383*	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 27384*	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 27379, 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 2566 and 2eu4 2652. (Contributed by AV, 2-Jul-2023.)
⊢ (𝐶 ∈ ℂ → ¬ (∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ∧ ∃!𝑏 ∈ ℂ ∃𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶))
Theorem	2sqreulem1 27385*	Lemma 1 for 2sqreu 27395. (Contributed by AV, 4-Jun-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqreultlem 27386*	Lemma for 2sqreult 27397. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqreultblem 27387*	Lemma for 2sqreultb 27398. (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 27388*	Lemma 1 for 2sqreunn 27396. (Contributed by AV, 11-Jun-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqreunnltlem 27389*	Lemma for 2sqreunnlt 27399. (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 27390*	Lemma for 2sqreunnltb 27400. (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 27391	Lemma 2 for 2sqreu 27395 etc. (Contributed by AV, 25-Jun-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = ((𝐴↑2) + (𝐶↑2)) → 𝐵 = 𝐶))
Theorem	2sqreulem3 27392	Lemma 3 for 2sqreu 27395 etc. (Contributed by AV, 25-Jun-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0)) → (((𝜑 ∧ ((𝐴↑2) + (𝐵↑2)) = 𝑃) ∧ (𝜓 ∧ ((𝐴↑2) + (𝐶↑2)) = 𝑃)) → 𝐵 = 𝐶))
Theorem	2sqreulem4 27393*	Lemma 4 for 2sqreu 27395 et. (Contributed by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ∀𝑎 ∈ ℕ0 ∃*𝑏 ∈ ℕ0 𝜑
Theorem	2sqreunnlem2 27394*	Lemma 2 for 2sqreunn 27396. (Contributed by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ∀𝑎 ∈ ℕ ∃*𝑏 ∈ ℕ 𝜑
Theorem	2sqreu 27395*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 27377 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 𝜑))
Theorem	2sqreunn 27396*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. See 2sqnn 27378 for the existence of such a decomposition. (Contributed by AV, 11-Jun-2023.) (Revised by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑))
Theorem	2sqreult 27397*	There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) (Revised by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑))
Theorem	2sqreultb 27398*	There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). (Contributed by AV, 10-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑)))
Theorem	2sqreunnlt 27399*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. (Contributed by AV, 4-Jun-2023.) Specialization to different integers, proposed by GL. (Revised by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑))
Theorem	2sqreunnltb 27400*	There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. (Contributed by AV, 11-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑)))