![]() |
Metamath
Proof Explorer Theorem List (p. 275 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lgsmulsqcoprm 27401 | 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 27402 | Variation on lgsdir 27390 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 27403 | Variation on lgsdi 27392 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 27404 | Lemma for lgsqr 27409. (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 27405* | Lemma for lgsqr 27409. (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 27406* | Lemma for lgsqr 27409. (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 27407* | Lemma for lgsqr 27409. (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 27408* | Lemma for lgsqr 27409. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ (𝐴 /L 𝑃) = 1) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) | ||
Theorem | lgsqr 27409* | 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 27393) and the number is a quadratic residue mod 𝑃 (it is -1 for nonresidues by the process of elimination from lgsabs1 27394). 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 27410* | 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 27411* | 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 27412* | 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 27413* | 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 27432. The general case is still to prove. | ||
Theorem | gausslemma2dlem0a 27414 | Auxiliary lemma 1 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) ⇒ ⊢ (𝜑 → 𝑃 ∈ ℕ) | ||
Theorem | gausslemma2dlem0b 27415 | Auxiliary lemma 2 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝐻 ∈ ℕ) | ||
Theorem | gausslemma2dlem0c 27416 | Auxiliary lemma 3 for gausslemma2d 27432. (Contributed by AV, 13-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1) | ||
Theorem | gausslemma2dlem0d 27417 | Auxiliary lemma 4 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → 𝑀 ∈ ℕ0) | ||
Theorem | gausslemma2dlem0e 27418 | Auxiliary lemma 5 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) | ||
Theorem | gausslemma2dlem0f 27419 | Auxiliary lemma 6 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻) | ||
Theorem | gausslemma2dlem0g 27420 | Auxiliary lemma 7 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) ⇒ ⊢ (𝜑 → 𝑀 ≤ 𝐻) | ||
Theorem | gausslemma2dlem0h 27421 | Auxiliary lemma 8 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ0) | ||
Theorem | gausslemma2dlem0i 27422 | Auxiliary lemma 9 for gausslemma2d 27432. (Contributed by AV, 14-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) | ||
Theorem | gausslemma2dlem1a 27423* | Lemma for gausslemma2dlem1 27424. (Contributed by AV, 1-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → ran 𝑅 = (1...𝐻)) | ||
Theorem | gausslemma2dlem1 27424* | Lemma 1 for gausslemma2d 27432. (Contributed by AV, 5-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) ⇒ ⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) | ||
Theorem | gausslemma2dlem2 27425* | Lemma 2 for gausslemma2d 27432. (Contributed by AV, 4-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) | ||
Theorem | gausslemma2dlem3 27426* | Lemma 3 for gausslemma2d 27432. (Contributed by AV, 4-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | ||
Theorem | gausslemma2dlem4 27427* | Lemma 4 for gausslemma2d 27432. (Contributed by AV, 16-Jun-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) | ||
Theorem | gausslemma2dlem5a 27428* | Lemma for gausslemma2dlem5 27429. (Contributed by AV, 8-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) ⇒ ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) | ||
Theorem | gausslemma2dlem5 27429* | Lemma 5 for gausslemma2d 27432. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) | ||
Theorem | gausslemma2dlem6 27430* | Lemma 6 for gausslemma2d 27432. (Contributed by AV, 16-Jun-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) | ||
Theorem | gausslemma2dlem7 27431* | Lemma 7 for gausslemma2d 27432. (Contributed by AV, 13-Jul-2021.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ 𝐻 = ((𝑃 − 1) / 2) & ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) & ⊢ 𝑀 = (⌊‘(𝑃 / 4)) & ⊢ 𝑁 = (𝐻 − 𝑀) ⇒ ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1) | ||
Theorem | gausslemma2d 27432* | 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 27433* | Lemma for lgseisen 27437. 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 27434* | Lemma for lgseisen 27437. 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 27435* | Lemma for lgseisen 27437. (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 27436* | Lemma for lgseisen 27437. (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 27437* | 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 27438* | Lemma for lgsquad 27441. 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 27439* | Lemma for lgsquad 27441. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 27438 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 27440* | Lemma for lgsquad 27441. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2})) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ 𝑀 = ((𝑃 − 1) / 2) & ⊢ 𝑁 = ((𝑄 − 1) / 2) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⇒ ⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁))) | ||
Theorem | lgsquad 27441 | 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 27442 | Lemma for lgsquad2 27444. (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 27443* | Lemma for lgsquad2 27444. (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 27444 | Extend lgsquad 27441 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 27445 | Extend lgsquad2 27444 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀))) | ||
Theorem | m1lgs 27446 | 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 27447* | Lemma 1 for 2lgslem1a 27449. (Contributed by AV, 16-Jun-2021.) |
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ∀𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑖 · 2) = ((𝑖 · 2) mod 𝑃)) | ||
Theorem | 2lgslem1a2 27448 | Lemma 2 for 2lgslem1a 27449. (Contributed by AV, 18-Jun-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → ((⌊‘(𝑁 / 4)) < 𝐼 ↔ (𝑁 / 2) < (𝐼 · 2))) | ||
Theorem | 2lgslem1a 27449* | Lemma 1 for 2lgslem1 27452. (Contributed by AV, 18-Jun-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)}) | ||
Theorem | 2lgslem1b 27450* | Lemma 2 for 2lgslem1 27452. (Contributed by AV, 18-Jun-2021.) |
⊢ 𝐼 = (𝐴...𝐵) & ⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2)) ⇒ ⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} | ||
Theorem | 2lgslem1c 27451 | Lemma 3 for 2lgslem1 27452. (Contributed by AV, 19-Jun-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) | ||
Theorem | 2lgslem1 27452* | Lemma 1 for 2lgs 27465. (Contributed by AV, 19-Jun-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))) | ||
Theorem | 2lgslem2 27453 | Lemma 2 for 2lgs 27465. (Contributed by AV, 20-Jun-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → 𝑁 ∈ ℤ) | ||
Theorem | 2lgslem3a 27454 | Lemma for 2lgslem3a1 27458. (Contributed by AV, 14-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 1)) → 𝑁 = (2 · 𝐾)) | ||
Theorem | 2lgslem3b 27455 | Lemma for 2lgslem3b1 27459. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 3)) → 𝑁 = ((2 · 𝐾) + 1)) | ||
Theorem | 2lgslem3c 27456 | Lemma for 2lgslem3c1 27460. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 5)) → 𝑁 = ((2 · 𝐾) + 1)) | ||
Theorem | 2lgslem3d 27457 | Lemma for 2lgslem3d1 27461. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 7)) → 𝑁 = ((2 · 𝐾) + 2)) | ||
Theorem | 2lgslem3a1 27458 | Lemma 1 for 2lgslem3 27462. (Contributed by AV, 15-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 1) → (𝑁 mod 2) = 0) | ||
Theorem | 2lgslem3b1 27459 | Lemma 2 for 2lgslem3 27462. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 3) → (𝑁 mod 2) = 1) | ||
Theorem | 2lgslem3c1 27460 | Lemma 3 for 2lgslem3 27462. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 5) → (𝑁 mod 2) = 1) | ||
Theorem | 2lgslem3d1 27461 | Lemma 4 for 2lgslem3 27462. (Contributed by AV, 15-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 7) → (𝑁 mod 2) = 0) | ||
Theorem | 2lgslem3 27462 | Lemma 3 for 2lgs 27465. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑁 mod 2) = if((𝑃 mod 8) ∈ {1, 7}, 0, 1)) | ||
Theorem | 2lgs2 27463 | The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.) |
⊢ (2 /L 2) = 0 | ||
Theorem | 2lgslem4 27464 | Lemma 4 for 2lgs 27465: special case of 2lgs 27465 for 𝑃 = 2. (Contributed by AV, 20-Jun-2021.) |
⊢ ((2 /L 2) = 1 ↔ (2 mod 8) ∈ {1, 7}) | ||
Theorem | 2lgs 27465 | 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 27372) 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 27466 | Lemma 1 for 2lgsoddprm 27474. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ((8 · 𝐴) + 𝐵)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 1) / 8))) | ||
Theorem | 2lgsoddprmlem2 27467 | Lemma 2 for 2lgsoddprm 27474. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8))) | ||
Theorem | 2lgsoddprmlem3a 27468 | Lemma 1 for 2lgsoddprmlem3 27472. (Contributed by AV, 20-Jul-2021.) |
⊢ (((1↑2) − 1) / 8) = 0 | ||
Theorem | 2lgsoddprmlem3b 27469 | Lemma 2 for 2lgsoddprmlem3 27472. (Contributed by AV, 20-Jul-2021.) |
⊢ (((3↑2) − 1) / 8) = 1 | ||
Theorem | 2lgsoddprmlem3c 27470 | Lemma 3 for 2lgsoddprmlem3 27472. (Contributed by AV, 20-Jul-2021.) |
⊢ (((5↑2) − 1) / 8) = 3 | ||
Theorem | 2lgsoddprmlem3d 27471 | Lemma 4 for 2lgsoddprmlem3 27472. (Contributed by AV, 20-Jul-2021.) |
⊢ (((7↑2) − 1) / 8) = (2 · 3) | ||
Theorem | 2lgsoddprmlem3 27472 | Lemma 3 for 2lgsoddprm 27474. (Contributed by AV, 20-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 𝑅 ∈ {1, 7})) | ||
Theorem | 2lgsoddprmlem4 27473 | Lemma 4 for 2lgsoddprm 27474. (Contributed by AV, 20-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ (𝑁 mod 8) ∈ {1, 7})) | ||
Theorem | 2lgsoddprm 27474 | 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 27475* | Lemma for 2sq 27488. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝐴 = ((abs‘𝑥)↑2)) | ||
Theorem | 2sqlem2 27476* | Lemma for 2sq 27488. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2))) | ||
Theorem | mul2sq 27477 | 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 27478 | Lemma for 2sqlem5 27480. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) & ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) & ⊢ (𝜑 → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
Theorem | 2sqlem4 27479 | Lemma for 2sqlem5 27480. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) & ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
Theorem | 2sqlem5 27480 | Lemma for 2sq 27488. 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 27481* | Lemma for 2sq 27488. 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 27482* | Lemma for 2sq 27488. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) | ||
Theorem | 2sqlem8a 27483* | Lemma for 2sqlem8 27484. (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 27484* | Lemma for 2sq 27488. (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 27485* | Lemma for 2sq 27488. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ 𝑌) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑆) | ||
Theorem | 2sqlem10 27486* | Lemma for 2sq 27488. 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 27487* | Lemma for 2sq 27488. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) | ||
Theorem | 2sq 27488* | 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 27489 | Lemma for 2sqb 27490. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2)) & ⊢ (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) & ⊢ (𝜑 → 𝑃 = ((𝑋↑2) + (𝑌↑2))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵))) ⇒ ⊢ (𝜑 → (𝑃 mod 4) = 1) | ||
Theorem | 2sqb 27490* | The converse to 2sq 27488. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1))) | ||
Theorem | 2sq2 27491 | 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 27492 | 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 27493 | 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 27494 | 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 27495* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 27490 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqnn0 27496* | 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 27497* | 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 27498* |
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 27501, 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 27501. (Contributed by AV, 21-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ∃!𝑎 ∈ ℂ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqn2reu 27499* |
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 27498, 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 27500* |
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 27498, 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 27498). For more details see comment for addsqnreup 27501. (Contributed by AV, 20-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ∃𝑎 ∈ ℂ ¬ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |