Home | Metamath
Proof Explorer Theorem List (p. 260 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2lgslem3b 25901 | Lemma for 2lgslem3b1 25905. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 3)) → 𝑁 = ((2 · 𝐾) + 1)) | ||
Theorem | 2lgslem3c 25902 | Lemma for 2lgslem3c1 25906. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 5)) → 𝑁 = ((2 · 𝐾) + 1)) | ||
Theorem | 2lgslem3d 25903 | Lemma for 2lgslem3d1 25907. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 7)) → 𝑁 = ((2 · 𝐾) + 2)) | ||
Theorem | 2lgslem3a1 25904 | Lemma 1 for 2lgslem3 25908. (Contributed by AV, 15-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 1) → (𝑁 mod 2) = 0) | ||
Theorem | 2lgslem3b1 25905 | Lemma 2 for 2lgslem3 25908. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 3) → (𝑁 mod 2) = 1) | ||
Theorem | 2lgslem3c1 25906 | Lemma 3 for 2lgslem3 25908. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 5) → (𝑁 mod 2) = 1) | ||
Theorem | 2lgslem3d1 25907 | Lemma 4 for 2lgslem3 25908. (Contributed by AV, 15-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 7) → (𝑁 mod 2) = 0) | ||
Theorem | 2lgslem3 25908 | Lemma 3 for 2lgs 25911. (Contributed by AV, 16-Jul-2021.) |
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))) ⇒ ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑁 mod 2) = if((𝑃 mod 8) ∈ {1, 7}, 0, 1)) | ||
Theorem | 2lgs2 25909 | The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.) |
⊢ (2 /L 2) = 0 | ||
Theorem | 2lgslem4 25910 | Lemma 4 for 2lgs 25911: special case of 2lgs 25911 for 𝑃 = 2. (Contributed by AV, 20-Jun-2021.) |
⊢ ((2 /L 2) = 1 ↔ (2 mod 8) ∈ {1, 7}) | ||
Theorem | 2lgs 25911 | 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 25818) 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 25912 | Lemma 1 for 2lgsoddprm 25920. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ((8 · 𝐴) + 𝐵)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 1) / 8))) | ||
Theorem | 2lgsoddprmlem2 25913 | Lemma 2 for 2lgsoddprm 25920. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8))) | ||
Theorem | 2lgsoddprmlem3a 25914 | Lemma 1 for 2lgsoddprmlem3 25918. (Contributed by AV, 20-Jul-2021.) |
⊢ (((1↑2) − 1) / 8) = 0 | ||
Theorem | 2lgsoddprmlem3b 25915 | Lemma 2 for 2lgsoddprmlem3 25918. (Contributed by AV, 20-Jul-2021.) |
⊢ (((3↑2) − 1) / 8) = 1 | ||
Theorem | 2lgsoddprmlem3c 25916 | Lemma 3 for 2lgsoddprmlem3 25918. (Contributed by AV, 20-Jul-2021.) |
⊢ (((5↑2) − 1) / 8) = 3 | ||
Theorem | 2lgsoddprmlem3d 25917 | Lemma 4 for 2lgsoddprmlem3 25918. (Contributed by AV, 20-Jul-2021.) |
⊢ (((7↑2) − 1) / 8) = (2 · 3) | ||
Theorem | 2lgsoddprmlem3 25918 | Lemma 3 for 2lgsoddprm 25920. (Contributed by AV, 20-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 𝑅 ∈ {1, 7})) | ||
Theorem | 2lgsoddprmlem4 25919 | Lemma 4 for 2lgsoddprm 25920. (Contributed by AV, 20-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ (𝑁 mod 8) ∈ {1, 7})) | ||
Theorem | 2lgsoddprm 25920 | 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 25921* | Lemma for 2sq 25934. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝐴 = ((abs‘𝑥)↑2)) | ||
Theorem | 2sqlem2 25922* | Lemma for 2sq 25934. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2))) | ||
Theorem | mul2sq 25923 | 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 25924 | Lemma for 2sqlem5 25926. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) & ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) & ⊢ (𝜑 → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
Theorem | 2sqlem4 25925 | Lemma for 2sqlem5 25926. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2))) & ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2))) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑆) | ||
Theorem | 2sqlem5 25926 | Lemma for 2sq 25934. 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 25927* | Lemma for 2sq 25934. 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 25928* | Lemma for 2sq 25934. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) | ||
Theorem | 2sqlem8a 25929* | Lemma for 2sqlem8 25930. (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 25930* | Lemma for 2sq 25934. (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 25931* | Lemma for 2sq 25934. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ 𝑌) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑆) | ||
Theorem | 2sqlem10 25932* | Lemma for 2sq 25934. 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 25933* | Lemma for 2sq 25934. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) | ||
Theorem | 2sq 25934* | 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 25935 | Lemma for 2sqb 25936. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2)) & ⊢ (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) & ⊢ (𝜑 → 𝑃 = ((𝑋↑2) + (𝑌↑2))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵))) ⇒ ⊢ (𝜑 → (𝑃 mod 4) = 1) | ||
Theorem | 2sqb 25936* | The converse to 2sq 25934. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1))) | ||
Theorem | 2sq2 25937 | 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 25938 | 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 25939 | 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 25940 | 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 25941* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 25936 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqnn0 25942* | 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 25943* | 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 25944* |
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 25947, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑). See also comments for df-eu 2650 and 2eu4 2737. For more details see comment for addsqnreup 25947. (Contributed by AV, 21-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ∃!𝑎 ∈ ℂ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqn2reu 25945* |
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 25944, 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 25946* |
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 25944, 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 25944). For more details see comment for addsqnreup 25947. (Contributed by AV, 20-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ∃𝑎 ∈ ℂ ¬ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqnreup 25947* |
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 25944, 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 2650 and 2eu4 2737. 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 25944). 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 25946). 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 4464 resp. 2eu4 2737). These two representations are equivalent (see opreu2reurex 6139). An analogon of this theorem using the latter variant is given in addsqn2reurex2 25949. 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 25965 and 2sqreuopb 25972). Alternatively, (proper) unordered pairs can be used: ∃!𝑝𝑒𝒫 𝐴((♯‘𝑝) = 2 ∧ 𝜑), or, using the definition of proper pairs: ∃!𝑝 ∈ (Pairsproper‘𝐴)𝜑 (see, for example, inlinecirc02preu 44673). (Contributed by AV, 21-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶) | ||
Theorem | addsq2nreurex 25948* | 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 25949* |
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 25944, 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 2650 and 2eu4 2737. (Contributed by AV, 2-Jul-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ (∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ∧ ∃!𝑏 ∈ ℂ ∃𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)) | ||
Theorem | 2sqreulem1 25950* | Lemma 1 for 2sqreu 25960. (Contributed by AV, 4-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreultlem 25951* | Lemma for 2sqreult 25962. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreultblem 25952* | Lemma for 2sqreultb 25963. (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 25953* | Lemma 1 for 2sqreunn 25961. (Contributed by AV, 11-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreunnltlem 25954* | Lemma for 2sqreunnlt 25964. (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 25955* | Lemma for 2sqreunnltb 25965. (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 25956 | Lemma 2 for 2sqreu 25960 etc. (Contributed by AV, 25-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = ((𝐴↑2) + (𝐶↑2)) → 𝐵 = 𝐶)) | ||
Theorem | 2sqreulem3 25957 | Lemma 3 for 2sqreu 25960 etc. (Contributed by AV, 25-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0)) → (((𝜑 ∧ ((𝐴↑2) + (𝐵↑2)) = 𝑃) ∧ (𝜓 ∧ ((𝐴↑2) + (𝐶↑2)) = 𝑃)) → 𝐵 = 𝐶)) | ||
Theorem | 2sqreulem4 25958* | Lemma 4 for 2sqreu 25960 et. (Contributed by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ∀𝑎 ∈ ℕ0 ∃*𝑏 ∈ ℕ0 𝜑 | ||
Theorem | 2sqreunnlem2 25959* | Lemma 2 for 2sqreunn 25961. (Contributed by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ∀𝑎 ∈ ℕ ∃*𝑏 ∈ ℕ 𝜑 | ||
Theorem | 2sqreu 25960* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 25942 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 25961* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. See 2sqnn 25943 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 25962* | 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 25963* | 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 25964* | 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 25965* | 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 ↔ (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑))) | ||
Theorem | 2sqreuop 25966* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. Ordered pair variant of 2sqreu 25960. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuopnn 25967* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. Ordered pair variant of 2sqreunn 25961. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuoplt 25968* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 25962. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuopltb 25969* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). Ordered pair variant of 2sqreultb 25963. (Contributed by AV, 3-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))) | ||
Theorem | 2sqreuopnnlt 25970* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. Ordered pair variant of 2sqreunnlt 25964. (Contributed by AV, 3-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuopnnltb 25971* | 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. Ordered pair variant of 2sqreunnltb 25965. (Contributed by AV, 3-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))) | ||
Theorem | 2sqreuopb 25972* | 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. Alternate ordered pair variant of 2sqreunnltb 25965. (Contributed by AV, 3-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))) | ||
Theorem | chebbnd1lem1 25973 | Lemma for chebbnd1 25976: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 25797. (Note that the expression 𝐾 is actually equal to 2 · 𝑁, but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 25788, which shows that each term in the expansion ((2 · 𝑁)C𝑁) = ∏𝑝 ∈ ℙ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) is at most 2 · 𝑁, so that the sum really only has nonzero elements up to 2 · 𝑁, and since each term is at most 2 · 𝑁, after taking logs we get the inequality π(2 · 𝑁) · log(2 · 𝑁) ≤ log((2 · 𝑁)C𝑁), and bclbnd 25784 finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2016.) |
⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁)))) | ||
Theorem | chebbnd1lem2 25974 | Lemma for chebbnd1 25976: Show that log(𝑁) / 𝑁 does not change too much between 𝑁 and 𝑀 = ⌊(𝑁 / 2). (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ 𝑀 = (⌊‘(𝑁 / 2)) ⇒ ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → ((log‘(2 · 𝑀)) / (2 · 𝑀)) < (2 · ((log‘𝑁) / 𝑁))) | ||
Theorem | chebbnd1lem3 25975 | Lemma for chebbnd1 25976: get a lower bound on π(𝑁) / (𝑁 / log(𝑁)) that is independent of 𝑁. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 = (⌊‘(𝑁 / 2)) ⇒ ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → (((log‘2) − (1 / (2 · e))) / 2) < ((π‘𝑁) · ((log‘𝑁) / 𝑁))) | ||
Theorem | chebbnd1 25976 | The Chebyshev bound: The function π(𝑥) is eventually lower bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function (𝑥 / log(𝑥)) / π(𝑥) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) | ||
Theorem | chtppilimlem1 25977 | Lemma for chtppilim 25979. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝑁 ∈ (2[,)+∞)) & ⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴)) ⇒ ⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁)) | ||
Theorem | chtppilimlem2 25978* | Lemma for chtppilim 25979. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) | ||
Theorem | chtppilim 25979 | The θ function is asymptotic to π(𝑥)log(𝑥), so it is sufficient to prove θ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1 | ||
Theorem | chto1ub 25980 | The θ function is upper bounded by a linear term. Corollary of chtub 25716. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1) | ||
Theorem | chebbnd2 25981 | The Chebyshev bound, part 2: The function π(𝑥) is eventually upper bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function π(𝑥) / (𝑥 / log(𝑥)) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((π‘𝑥) / (𝑥 / (log‘𝑥)))) ∈ 𝑂(1) | ||
Theorem | chto1lb 25982 | The θ function is lower bounded by a linear term. Corollary of chebbnd1 25976. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) ∈ 𝑂(1) | ||
Theorem | chpchtlim 25983 | The ψ and θ functions are asymptotic to each other, so is sufficient to prove either θ(𝑥) / 𝑥 ⇝𝑟 1 or ψ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟 1 | ||
Theorem | chpo1ub 25984 | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) | ||
Theorem | chpo1ubb 25985* | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.) |
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥) | ||
Theorem | vmadivsum 25986* | The sum of the von Mangoldt function over 𝑛 is asymptotic to log𝑥 + 𝑂(1). Equation 9.2.13 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) | ||
Theorem | vmadivsumb 25987* | Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐 | ||
Theorem | rplogsumlem1 25988* | Lemma for rplogsum 26031. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2) | ||
Theorem | rplogsumlem2 25989* | Lemma for rplogsum 26031. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2) | ||
Theorem | dchrisum0lem1a 25990 | Lemma for dchrisum0lem1 26020. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ (((𝜑 ∧ 𝑋 ∈ ℝ+) ∧ 𝐷 ∈ (1...(⌊‘𝑋))) → (𝑋 ≤ ((𝑋↑2) / 𝐷) ∧ (⌊‘((𝑋↑2) / 𝐷)) ∈ (ℤ≥‘(⌊‘𝑋)))) | ||
Theorem | rpvmasumlem 25991* | Lemma for rpvmasum 26030. Calculate the "trivial case" estimate Σ𝑛 ≤ 𝑥( 1 (𝑛)Λ(𝑛) / 𝑛) = log𝑥 + 𝑂(1), where 1 (𝑥) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) | ||
Theorem | dchrisumlema 25992* | Lemma for dchrisum 25996. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ ℝ+ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴))) | ||
Theorem | dchrisumlem1 25993* | Lemma for dchrisum 25996. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) | ||
Theorem | dchrisumlem2 25994* | Lemma for dchrisum 25996. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) & ⊢ (𝜑 → 𝑈 ∈ ℝ+) & ⊢ (𝜑 → 𝑀 ≤ 𝑈) & ⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1)) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝐼)) ⇒ ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴)) | ||
Theorem | dchrisumlem3 25995* | Lemma for dchrisum 25996. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) | ||
Theorem | dchrisum 25996* | If 𝑛 ∈ [𝑀, +∞) ↦ 𝐴(𝑛) is a positive decreasing function approaching zero, then the infinite sum Σ𝑛, 𝑋(𝑛)𝐴(𝑛) is convergent, with the partial sum Σ𝑛 ≤ 𝑥, 𝑋(𝑛)𝐴(𝑛) within 𝑂(𝐴(𝑀)) of the limit 𝑇. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) | ||
Theorem | dchrmusumlema 25997* | Lemma for dchrmusum 26028 and dchrisumn0 26025. Apply dchrisum 25996 for the function 1 / 𝑦. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) | ||
Theorem | dchrmusum2 25998* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded, provided that 𝑇 ≠ 0. Lemma 9.4.2 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · 𝑇)) ∈ 𝑂(1)) | ||
Theorem | dchrvmasumlem1 25999* | An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘𝑚) / 𝑚)))) | ||
Theorem | dchrvmasum2lem 26000* | Give an expression for log𝑥 remarkably similar to Σ𝑛 ≤ 𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 25999. Part of Lemma 9.4.3 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |