![]() |
Metamath
Proof Explorer Theorem List (p. 270 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2lgslem3c 26901 | Lemma for 2lgslem3c1 26905. (Contributed by AV, 16-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐พ โ โ0 โง ๐ = ((8 ยท ๐พ) + 5)) โ ๐ = ((2 ยท ๐พ) + 1)) | ||
Theorem | 2lgslem3d 26902 | Lemma for 2lgslem3d1 26906. (Contributed by AV, 16-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐พ โ โ0 โง ๐ = ((8 ยท ๐พ) + 7)) โ ๐ = ((2 ยท ๐พ) + 2)) | ||
Theorem | 2lgslem3a1 26903 | Lemma 1 for 2lgslem3 26907. (Contributed by AV, 15-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐ โ โ โง (๐ mod 8) = 1) โ (๐ mod 2) = 0) | ||
Theorem | 2lgslem3b1 26904 | Lemma 2 for 2lgslem3 26907. (Contributed by AV, 16-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐ โ โ โง (๐ mod 8) = 3) โ (๐ mod 2) = 1) | ||
Theorem | 2lgslem3c1 26905 | Lemma 3 for 2lgslem3 26907. (Contributed by AV, 16-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐ โ โ โง (๐ mod 8) = 5) โ (๐ mod 2) = 1) | ||
Theorem | 2lgslem3d1 26906 | Lemma 4 for 2lgslem3 26907. (Contributed by AV, 15-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐ โ โ โง (๐ mod 8) = 7) โ (๐ mod 2) = 0) | ||
Theorem | 2lgslem3 26907 | Lemma 3 for 2lgs 26910. (Contributed by AV, 16-Jul-2021.) |
โข ๐ = (((๐ โ 1) / 2) โ (โโ(๐ / 4))) โ โข ((๐ โ โ โง ยฌ 2 โฅ ๐) โ (๐ mod 2) = if((๐ mod 8) โ {1, 7}, 0, 1)) | ||
Theorem | 2lgs2 26908 | The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.) |
โข (2 /L 2) = 0 | ||
Theorem | 2lgslem4 26909 | Lemma 4 for 2lgs 26910: special case of 2lgs 26910 for ๐ = 2. (Contributed by AV, 20-Jun-2021.) |
โข ((2 /L 2) = 1 โ (2 mod 8) โ {1, 7}) | ||
Theorem | 2lgs 26910 | 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 26817) 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 26911 | Lemma 1 for 2lgsoddprm 26919. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ = ((8 ยท ๐ด) + ๐ต)) โ (((๐โ2) โ 1) / 8) = (((8 ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) โ 1) / 8))) | ||
Theorem | 2lgsoddprmlem2 26912 | Lemma 2 for 2lgsoddprm 26919. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ = (๐ mod 8)) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ (((๐ โ2) โ 1) / 8))) | ||
Theorem | 2lgsoddprmlem3a 26913 | Lemma 1 for 2lgsoddprmlem3 26917. (Contributed by AV, 20-Jul-2021.) |
โข (((1โ2) โ 1) / 8) = 0 | ||
Theorem | 2lgsoddprmlem3b 26914 | Lemma 2 for 2lgsoddprmlem3 26917. (Contributed by AV, 20-Jul-2021.) |
โข (((3โ2) โ 1) / 8) = 1 | ||
Theorem | 2lgsoddprmlem3c 26915 | Lemma 3 for 2lgsoddprmlem3 26917. (Contributed by AV, 20-Jul-2021.) |
โข (((5โ2) โ 1) / 8) = 3 | ||
Theorem | 2lgsoddprmlem3d 26916 | Lemma 4 for 2lgsoddprmlem3 26917. (Contributed by AV, 20-Jul-2021.) |
โข (((7โ2) โ 1) / 8) = (2 ยท 3) | ||
Theorem | 2lgsoddprmlem3 26917 | Lemma 3 for 2lgsoddprm 26919. (Contributed by AV, 20-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ = (๐ mod 8)) โ (2 โฅ (((๐ โ2) โ 1) / 8) โ ๐ โ {1, 7})) | ||
Theorem | 2lgsoddprmlem4 26918 | Lemma 4 for 2lgsoddprm 26919. (Contributed by AV, 20-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ (2 โฅ (((๐โ2) โ 1) / 8) โ (๐ mod 8) โ {1, 7})) | ||
Theorem | 2lgsoddprm 26919 | 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 26920* | Lemma for 2sq 26933. (Contributed by Mario Carneiro, 19-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) โ โข (๐ด โ ๐ โ โ๐ฅ โ โค[i] ๐ด = ((absโ๐ฅ)โ2)) | ||
Theorem | 2sqlem2 26921* | Lemma for 2sq 26933. (Contributed by Mario Carneiro, 19-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) โ โข (๐ด โ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ด = ((๐ฅโ2) + (๐ฆโ2))) | ||
Theorem | mul2sq 26922 | 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 26923 | Lemma for 2sqlem5 26925. (Contributed by Mario Carneiro, 20-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ถ โ โค) & โข (๐ โ ๐ท โ โค) & โข (๐ โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) & โข (๐ โ ๐ = ((๐ถโ2) + (๐ทโ2))) & โข (๐ โ ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | 2sqlem4 26924 | Lemma for 2sqlem5 26925. (Contributed by Mario Carneiro, 20-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ถ โ โค) & โข (๐ โ ๐ท โ โค) & โข (๐ โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) & โข (๐ โ ๐ = ((๐ถโ2) + (๐ทโ2))) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | 2sqlem5 26925 | Lemma for 2sq 26933. 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 26926* | Lemma for 2sq 26933. 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 26927* | Lemma for 2sq 26933. (Contributed by Mario Carneiro, 19-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} โ โข ๐ โ (๐ โฉ โ) | ||
Theorem | 2sqlem8a 26928* | Lemma for 2sqlem8 26929. (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 26929* | Lemma for 2sq 26933. (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 26930* | Lemma for 2sq 26933. (Contributed by Mario Carneiro, 19-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} & โข (๐ โ โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐)) & โข (๐ โ ๐ โฅ ๐) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | 2sqlem10 26931* | Lemma for 2sq 26933. 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 26932* | Lemma for 2sq 26933. (Contributed by Mario Carneiro, 19-Jun-2015.) |
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} โ โข ((๐ โ โ โง (๐ mod 4) = 1) โ ๐ โ ๐) | ||
Theorem | 2sq 26933* | 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 26934 | Lemma for 2sqb 26935. (Contributed by Mario Carneiro, 20-Jun-2015.) |
โข (๐ โ (๐ โ โ โง ๐ โ 2)) & โข (๐ โ (๐ โ โค โง ๐ โ โค)) & โข (๐ โ ๐ = ((๐โ2) + (๐โ2))) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ (๐ gcd ๐) = ((๐ ยท ๐ด) + (๐ ยท ๐ต))) โ โข (๐ โ (๐ mod 4) = 1) | ||
Theorem | 2sqb 26935* | The converse to 2sq 26933. (Contributed by Mario Carneiro, 20-Jun-2015.) |
โข (๐ โ โ โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2)) โ (๐ = 2 โจ (๐ mod 4) = 1))) | ||
Theorem | 2sq2 26936 | 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 26937 | 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 26938 | 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 26939 | 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 26940* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 26935 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
โข (๐ โ โ โ โ*๐ โ โ0 โ๐ โ โ0 (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqnn0 26941* | 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 26942* | 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 26943* |
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 26946, is an example showing that the pattern โ!๐ โ ๐ดโ!๐ โ ๐ต๐ does not necessarily mean "There are unique sets ๐ and ๐ fulfilling ๐). See also comments for df-eu 2564 and 2eu4 2651. For more details see comment for addsqnreup 26946. (Contributed by AV, 21-Jun-2023.) |
โข (๐ถ โ โ โ โ!๐ โ โ โ!๐ โ โ (๐ + (๐โ2)) = ๐ถ) | ||
Theorem | addsqn2reu 26944* |
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 26943, 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 26945* |
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 26943, 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 26943). For more details see comment for addsqnreup 26946. (Contributed by AV, 20-Jun-2023.) |
โข (๐ถ โ โ โ โ๐ โ โ ยฌ โ!๐ โ โ (๐ + (๐โ2)) = ๐ถ) | ||
Theorem | addsqnreup 26946* |
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 26943, 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 2564 and 2eu4 2651. 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 26943). 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 26945). 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 4527 resp. 2eu4 2651). These two representations are equivalent (see opreu2reurex 6294). An analogon of this theorem using the latter variant is given in addsqn2reurex2 26948. 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 26964 and 2sqreuopb 26971). Alternatively, (proper) unordered pairs can be used: โ!๐๐๐ซ ๐ด((โฏโ๐) = 2 โง ๐), or, using the definition of proper pairs: โ!๐ โ (Pairsproperโ๐ด)๐ (see, for example, inlinecirc02preu 47474). (Contributed by AV, 21-Jun-2023.) |
โข (๐ถ โ โ โ ยฌ โ!๐ โ (โ ร โ)((1st โ๐) + ((2nd โ๐)โ2)) = ๐ถ) | ||
Theorem | addsq2nreurex 26947* | 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 26948* |
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 26943, 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 2564 and 2eu4 2651. (Contributed by AV, 2-Jul-2023.) |
โข (๐ถ โ โ โ ยฌ (โ!๐ โ โ โ๐ โ โ (๐ + (๐โ2)) = ๐ถ โง โ!๐ โ โ โ๐ โ โ (๐ + (๐โ2)) = ๐ถ)) | ||
Theorem | 2sqreulem1 26949* | Lemma 1 for 2sqreu 26959. (Contributed by AV, 4-Jun-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ โ0 โ!๐ โ โ0 (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqreultlem 26950* | Lemma for 2sqreult 26961. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ โ0 โ!๐ โ โ0 (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqreultblem 26951* | Lemma for 2sqreultb 26962. (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 26952* | Lemma 1 for 2sqreunn 26960. (Contributed by AV, 11-Jun-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ โ โ!๐ โ โ (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqreunnltlem 26953* | Lemma for 2sqreunnlt 26963. (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 26954* | Lemma for 2sqreunnltb 26964. (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 26955 | Lemma 2 for 2sqreu 26959 etc. (Contributed by AV, 25-Jun-2023.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0 โง ๐ถ โ โ0) โ (((๐ดโ2) + (๐ตโ2)) = ((๐ดโ2) + (๐ถโ2)) โ ๐ต = ๐ถ)) | ||
Theorem | 2sqreulem3 26956 | Lemma 3 for 2sqreu 26959 etc. (Contributed by AV, 25-Jun-2023.) |
โข ((๐ด โ โ0 โง (๐ต โ โ0 โง ๐ถ โ โ0)) โ (((๐ โง ((๐ดโ2) + (๐ตโ2)) = ๐) โง (๐ โง ((๐ดโ2) + (๐ถโ2)) = ๐)) โ ๐ต = ๐ถ)) | ||
Theorem | 2sqreulem4 26957* | Lemma 4 for 2sqreu 26959 et. (Contributed by AV, 25-Jun-2023.) |
โข (๐ โ (๐ โง ((๐โ2) + (๐โ2)) = ๐)) โ โข โ๐ โ โ0 โ*๐ โ โ0 ๐ | ||
Theorem | 2sqreunnlem2 26958* | Lemma 2 for 2sqreunn 26960. (Contributed by AV, 25-Jun-2023.) |
โข (๐ โ (๐ โง ((๐โ2) + (๐โ2)) = ๐)) โ โข โ๐ โ โ โ*๐ โ โ ๐ | ||
Theorem | 2sqreu 26959* | There exists a unique decomposition of a prime of the form 4๐ + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 26941 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 26960* | There exists a unique decomposition of a prime of the form 4๐ + 1 as a sum of squares of two positive integers. See 2sqnn 26942 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 26961* | 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 26962* | 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 26963* | 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 26964* | 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 26965* | 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 26959. (Contributed by AV, 2-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ0 ร โ0)((1st โ๐) โค (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuopnn 26966* | 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 26960. (Contributed by AV, 2-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ ร โ)((1st โ๐) โค (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuoplt 26967* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 26961. (Contributed by AV, 2-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ0 ร โ0)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuopltb 26968* | 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 26962. (Contributed by AV, 3-Jul-2023.) |
โข (๐ โ โ โ ((๐ mod 4) = 1 โ โ!๐ โ (โ0 ร โ0)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐))) | ||
Theorem | 2sqreuopnnlt 26969* | 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 26963. (Contributed by AV, 3-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ ร โ)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuopnnltb 26970* | 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 26964. (Contributed by AV, 3-Jul-2023.) |
โข (๐ โ โ โ ((๐ mod 4) = 1 โ โ!๐ โ (โ ร โ)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐))) | ||
Theorem | 2sqreuopb 26971* | 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 26964. (Contributed by AV, 3-Jul-2023.) |
โข (๐ โ โ โ ((๐ mod 4) = 1 โ โ!๐ โ (โ ร โ)โ๐โ๐(๐ = โจ๐, ๐โฉ โง (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐)))) | ||
Theorem | chebbnd1lem1 26972 | Lemma for chebbnd1 26975: show a lower bound on ฯ(๐ฅ) at even integers using similar techniques to those used to prove bpos 26796. (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 26787, 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 26783 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 26973 | Lemma for chebbnd1 26975: 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 26974 | Lemma for chebbnd1 26975: 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 26975 | 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 26976 | Lemma for chtppilim 26978. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ด < 1) & โข (๐ โ ๐ โ (2[,)+โ)) & โข (๐ โ ((๐โ๐๐ด) / (ฯโ๐)) < (1 โ ๐ด)) โ โข (๐ โ ((๐ดโ2) ยท ((ฯโ๐) ยท (logโ๐))) < (ฮธโ๐)) | ||
Theorem | chtppilimlem2 26977* | Lemma for chtppilim 26978. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ด < 1) โ โข (๐ โ โ๐ง โ โ โ๐ฅ โ (2[,)+โ)(๐ง โค ๐ฅ โ ((๐ดโ2) ยท ((ฯโ๐ฅ) ยท (logโ๐ฅ))) < (ฮธโ๐ฅ))) | ||
Theorem | chtppilim 26978 | 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 26979 | The ฮธ function is upper bounded by a linear term. Corollary of chtub 26715. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ฅ โ โ+ โฆ ((ฮธโ๐ฅ) / ๐ฅ)) โ ๐(1) | ||
Theorem | chebbnd2 26980 | 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 26981 | The ฮธ function is lower bounded by a linear term. Corollary of chebbnd1 26975. (Contributed by Mario Carneiro, 8-Apr-2016.) |
โข (๐ฅ โ (2[,)+โ) โฆ (๐ฅ / (ฮธโ๐ฅ))) โ ๐(1) | ||
Theorem | chpchtlim 26982 | 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 26983 | The ฯ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.) |
โข (๐ฅ โ โ+ โฆ ((ฯโ๐ฅ) / ๐ฅ)) โ ๐(1) | ||
Theorem | chpo1ubb 26984* | The ฯ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.) |
โข โ๐ โ โ+ โ๐ฅ โ โ+ (ฯโ๐ฅ) โค (๐ ยท ๐ฅ) | ||
Theorem | vmadivsum 26985* | 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 26986* | Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.) |
โข โ๐ โ โ+ โ๐ฅ โ (1[,)+โ)(absโ(ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โค ๐ | ||
Theorem | rplogsumlem1 26987* | Lemma for rplogsum 27030. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ด โ โ โ ฮฃ๐ โ (2...๐ด)((logโ๐) / (๐ ยท (๐ โ 1))) โค 2) | ||
Theorem | rplogsumlem2 26988* | Lemma for rplogsum 27030. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ด โ โค โ ฮฃ๐ โ (1...๐ด)(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) โค 2) | ||
Theorem | dchrisum0lem1a 26989 | Lemma for dchrisum0lem1 27019. (Contributed by Mario Carneiro, 7-Jun-2016.) |
โข (((๐ โง ๐ โ โ+) โง ๐ท โ (1...(โโ๐))) โ (๐ โค ((๐โ2) / ๐ท) โง (โโ((๐โ2) / ๐ท)) โ (โคโฅโ(โโ๐)))) | ||
Theorem | rpvmasumlem 26990* | Lemma for rpvmasum 27029. 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 26991* | Lemma for dchrisum 26995. 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 26992* | Lemma for dchrisum 26995. 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 26993* | Lemma for dchrisum 26995. 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 26994* | Lemma for dchrisum 26995. 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 26995* | 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 26996* | Lemma for dchrmusum 27027 and dchrisumn0 27024. Apply dchrisum 26995 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 26997* | 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 26998* | 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 26999* | Give an expression for log๐ฅ remarkably similar to ฮฃ๐ โค ๐ฅ(๐(๐)ฮ(๐) / ๐) given in dchrvmasumlem1 26998. 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โ((๐ด / ๐) / ๐)) / ๐)))) | ||
Theorem | dchrvmasum2if 27000* | Combine the results of dchrvmasumlem1 26998 and dchrvmasum2lem 26999 inside a conditional. (Contributed by Mario Carneiro, 4-May-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐บ = (DChrโ๐) & โข ๐ท = (Baseโ๐บ) & โข 1 = (0gโ๐บ) & โข (๐ โ ๐ โ ๐ท) & โข (๐ โ ๐ โ 1 ) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ 1 โค ๐ด) โ โข (๐ โ (ฮฃ๐ โ (1...(โโ๐ด))((๐โ(๐ฟโ๐)) ยท ((ฮโ๐) / ๐)) + if(๐, (logโ๐ด), 0)) = ฮฃ๐ โ (1...(โโ๐ด))(((๐โ(๐ฟโ๐)) ยท ((ฮผโ๐) / ๐)) ยท ฮฃ๐ โ (1...(โโ(๐ด / ๐)))((๐โ(๐ฟโ๐)) ยท ((logโif(๐, (๐ด / ๐), ๐)) / ๐)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |