![]() |
Metamath
Proof Explorer Theorem List (p. 169 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pczdvds 16801 | Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ ((π β β β§ (π β β€ β§ π β 0)) β (πβ(π pCnt π)) β₯ π) | ||
Theorem | pcdvds 16802 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β (πβ(π pCnt π)) β₯ π) | ||
Theorem | pczndvds 16803 | Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
β’ ((π β β β§ (π β β€ β§ π β 0)) β Β¬ (πβ((π pCnt π) + 1)) β₯ π) | ||
Theorem | pcndvds 16804 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β Β¬ (πβ((π pCnt π) + 1)) β₯ π) | ||
Theorem | pczndvds2 16805 | The remainder after dividing out all factors of π is not divisible by π. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ ((π β β β§ (π β β€ β§ π β 0)) β Β¬ π β₯ (π / (πβ(π pCnt π)))) | ||
Theorem | pcndvds2 16806 | The remainder after dividing out all factors of π is not divisible by π. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β Β¬ π β₯ (π / (πβ(π pCnt π)))) | ||
Theorem | pcdvdsb 16807 | πβπ΄ divides π if and only if π΄ is at most the count of π. (Contributed by Mario Carneiro, 3-Oct-2014.) |
β’ ((π β β β§ π β β€ β§ π΄ β β0) β (π΄ β€ (π pCnt π) β (πβπ΄) β₯ π)) | ||
Theorem | pcelnn 16808 | There are a positive number of powers of a prime π in π iff π divides π. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β ((π pCnt π) β β β π β₯ π)) | ||
Theorem | pceq0 16809 | There are zero powers of a prime π in π iff π does not divide π. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β ((π pCnt π) = 0 β Β¬ π β₯ π)) | ||
Theorem | pcidlem 16810 | The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ ((π β β β§ π΄ β β0) β (π pCnt (πβπ΄)) = π΄) | ||
Theorem | pcid 16811 | The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ ((π β β β§ π΄ β β€) β (π pCnt (πβπ΄)) = π΄) | ||
Theorem | pcneg 16812 | The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ ((π β β β§ π΄ β β) β (π pCnt -π΄) = (π pCnt π΄)) | ||
Theorem | pcabs 16813 | The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ ((π β β β§ π΄ β β) β (π pCnt (absβπ΄)) = (π pCnt π΄)) | ||
Theorem | pcdvdstr 16814 | The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ ((π β β β§ (π΄ β β€ β§ π΅ β β€ β§ π΄ β₯ π΅)) β (π pCnt π΄) β€ (π pCnt π΅)) | ||
Theorem | pcgcd1 16815 | The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.) |
β’ (((π β β β§ π΄ β β€ β§ π΅ β β€) β§ (π pCnt π΄) β€ (π pCnt π΅)) β (π pCnt (π΄ gcd π΅)) = (π pCnt π΄)) | ||
Theorem | pcgcd 16816 | The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.) |
β’ ((π β β β§ π΄ β β€ β§ π΅ β β€) β (π pCnt (π΄ gcd π΅)) = if((π pCnt π΄) β€ (π pCnt π΅), (π pCnt π΄), (π pCnt π΅))) | ||
Theorem | pc2dvds 16817* | A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ β₯ π΅ β βπ β β (π pCnt π΄) β€ (π pCnt π΅))) | ||
Theorem | pc11 16818* | The prime count function, viewed as a function from β to (β βm β), is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ = π΅ β βπ β β (π pCnt π΄) = (π pCnt π΅))) | ||
Theorem | pcz 16819* | The prime count function can be used as an indicator that a given rational number is an integer. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π΄ β β β (π΄ β β€ β βπ β β 0 β€ (π pCnt π΄))) | ||
Theorem | pcprmpw2 16820* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ ((π β β β§ π΄ β β) β (βπ β β0 π΄ β₯ (πβπ) β π΄ = (πβ(π pCnt π΄)))) | ||
Theorem | pcprmpw 16821* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ ((π β β β§ π΄ β β) β (βπ β β0 π΄ = (πβπ) β π΄ = (πβ(π pCnt π΄)))) | ||
Theorem | dvdsprmpweq 16822* | If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.) |
β’ ((π β β β§ π΄ β β β§ π β β0) β (π΄ β₯ (πβπ) β βπ β β0 π΄ = (πβπ))) | ||
Theorem | dvdsprmpweqnn 16823* | If an integer greater than 1 divides a prime power, it is a (proper) prime power. (Contributed by AV, 13-Aug-2021.) |
β’ ((π β β β§ π΄ β (β€β₯β2) β§ π β β0) β (π΄ β₯ (πβπ) β βπ β β π΄ = (πβπ))) | ||
Theorem | dvdsprmpweqle 16824* | If a positive integer divides a prime power, it is a prime power with a smaller exponent. (Contributed by AV, 25-Jul-2021.) |
β’ ((π β β β§ π΄ β β β§ π β β0) β (π΄ β₯ (πβπ) β βπ β β0 (π β€ π β§ π΄ = (πβπ)))) | ||
Theorem | difsqpwdvds 16825 | If the difference of two squares is a power of a prime, the prime divides twice the second squared number. (Contributed by AV, 13-Aug-2021.) |
β’ (((π΄ β β0 β§ π΅ β β0 β§ (π΅ + 1) < π΄) β§ (πΆ β β β§ π· β β0)) β ((πΆβπ·) = ((π΄β2) β (π΅β2)) β πΆ β₯ (2 Β· π΅))) | ||
Theorem | pcaddlem 16826 | Lemma for pcadd 16827. The original numbers π΄ and π΅ have been decomposed using the prime count function as (πβπ) Β· (π / π) where π , π are both not divisible by π and π = (π pCnt π΄), and similarly for π΅. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ (π β π β β) & β’ (π β π΄ = ((πβπ) Β· (π / π))) & β’ (π β π΅ = ((πβπ) Β· (π / π))) & β’ (π β π β (β€β₯βπ)) & β’ (π β (π β β€ β§ Β¬ π β₯ π )) & β’ (π β (π β β β§ Β¬ π β₯ π)) & β’ (π β (π β β€ β§ Β¬ π β₯ π)) & β’ (π β (π β β β§ Β¬ π β₯ π)) β β’ (π β π β€ (π pCnt (π΄ + π΅))) | ||
Theorem | pcadd 16827 | An inequality for the prime count of a sum. This is the source of the ultrametric inequality for the p-adic metric. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π pCnt π΄) β€ (π pCnt π΅)) β β’ (π β (π pCnt π΄) β€ (π pCnt (π΄ + π΅))) | ||
Theorem | pcadd2 16828 | The inequality of pcadd 16827 becomes an equality when one of the factors has prime count strictly less than the other. (Contributed by Mario Carneiro, 16-Jan-2015.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π pCnt π΄) < (π pCnt π΅)) β β’ (π β (π pCnt π΄) = (π pCnt (π΄ + π΅))) | ||
Theorem | pcmptcl 16829 | Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) & β’ (π β βπ β β π΄ β β0) β β’ (π β (πΉ:ββΆβ β§ seq1( Β· , πΉ):ββΆβ)) | ||
Theorem | pcmpt 16830* | Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) & β’ (π β βπ β β π΄ β β0) & β’ (π β π β β) & β’ (π β π β β) & β’ (π = π β π΄ = π΅) β β’ (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) | ||
Theorem | pcmpt2 16831* | Dividing two prime count maps yields a number with all dividing primes confined to an interval. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) & β’ (π β βπ β β π΄ β β0) & β’ (π β π β β) & β’ (π β π β β) & β’ (π = π β π΄ = π΅) & β’ (π β π β (β€β₯βπ)) β β’ (π β (π pCnt ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ))) = if((π β€ π β§ Β¬ π β€ π), π΅, 0)) | ||
Theorem | pcmptdvds 16832 | The partial products of the prime power map form a divisibility chain. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) & β’ (π β βπ β β π΄ β β0) & β’ (π β π β β) & β’ (π β π β (β€β₯βπ)) β β’ (π β (seq1( Β· , πΉ)βπ) β₯ (seq1( Β· , πΉ)βπ)) | ||
Theorem | pcprod 16833* | The product of the primes taken to their respective powers reconstructs the original number. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt π)), 1)) β β’ (π β β β (seq1( Β· , πΉ)βπ) = π) | ||
Theorem | sumhash 16834* | The sum of 1 over a set is the size of the set. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 20-May-2014.) |
β’ ((π΅ β Fin β§ π΄ β π΅) β Ξ£π β π΅ if(π β π΄, 1, 0) = (β―βπ΄)) | ||
Theorem | fldivp1 16835 | The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014.) |
β’ ((π β β€ β§ π β β) β ((ββ((π + 1) / π)) β (ββ(π / π))) = if(π β₯ (π + 1), 1, 0)) | ||
Theorem | pcfaclem 16836 | Lemma for pcfac 16837. (Contributed by Mario Carneiro, 20-May-2014.) |
β’ ((π β β0 β§ π β (β€β₯βπ) β§ π β β) β (ββ(π / (πβπ))) = 0) | ||
Theorem | pcfac 16837* | Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.) |
β’ ((π β β0 β§ π β (β€β₯βπ) β§ π β β) β (π pCnt (!βπ)) = Ξ£π β (1...π)(ββ(π / (πβπ)))) | ||
Theorem | pcbc 16838* | Calculate the prime count of a binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.) |
β’ ((π β β β§ πΎ β (0...π) β§ π β β) β (π pCnt (πCπΎ)) = Ξ£π β (1...π)((ββ(π / (πβπ))) β ((ββ((π β πΎ) / (πβπ))) + (ββ(πΎ / (πβπ)))))) | ||
Theorem | qexpz 16839 | If a power of a rational number is an integer, then the number is an integer. In other words, all n-th roots are irrational unless they are integers (so that the original number is an n-th power). (Contributed by Mario Carneiro, 10-Aug-2015.) |
β’ ((π΄ β β β§ π β β β§ (π΄βπ) β β€) β π΄ β β€) | ||
Theorem | expnprm 16840 | A second or higher power of a rational number is not a prime number. Or by contraposition, the n-th root of a prime number is irrational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015.) |
β’ ((π΄ β β β§ π β (β€β₯β2)) β Β¬ (π΄βπ) β β) | ||
Theorem | oddprmdvds 16841* | Every positive integer which is not a power of two is divisible by an odd prime number. (Contributed by AV, 6-Aug-2021.) |
β’ ((πΎ β β β§ Β¬ βπ β β0 πΎ = (2βπ)) β βπ β (β β {2})π β₯ πΎ) | ||
Theorem | prmpwdvds 16842 | A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ (((πΎ β β€ β§ π· β β€) β§ (π β β β§ π β β) β§ (π· β₯ (πΎ Β· (πβπ)) β§ Β¬ π· β₯ (πΎ Β· (πβ(π β 1))))) β (πβπ) β₯ π·) | ||
Theorem | pockthlem 16843 | Lemma for pockthg 16844. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ < π΄) & β’ (π β π = ((π΄ Β· π΅) + 1)) & β’ (π β π β β) & β’ (π β π β₯ π) & β’ (π β π β β) & β’ (π β (π pCnt π΄) β β) & β’ (π β πΆ β β€) & β’ (π β ((πΆβ(π β 1)) mod π) = 1) & β’ (π β (((πΆβ((π β 1) / π)) β 1) gcd π) = 1) β β’ (π β (π pCnt π΄) β€ (π pCnt (π β 1))) | ||
Theorem | pockthg 16844* | The generalized Pocklington's theorem. If π β 1 = π΄ Β· π΅ where π΅ < π΄, then π is prime if and only if for every prime factor π of π΄, there is an π₯ such that π₯β(π β 1) = 1( mod π) and gcd (π₯β((π β 1) / π) β 1, π) = 1. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ < π΄) & β’ (π β π = ((π΄ Β· π΅) + 1)) & β’ (π β βπ β β (π β₯ π΄ β βπ₯ β β€ (((π₯β(π β 1)) mod π) = 1 β§ (((π₯β((π β 1) / π)) β 1) gcd π) = 1))) β β’ (π β π β β) | ||
Theorem | pockthi 16845 | Pocklington's theorem, which gives a sufficient criterion for a number π to be prime. This is the preferred method for verifying large primes, being much more efficient to compute than trial division. This form has been optimized for application to specific large primes; see pockthg 16844 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ π β β & β’ πΊ β β & β’ π = (πΊ Β· π) & β’ π = (π + 1) & β’ π· β β & β’ πΈ β β & β’ π΄ β β & β’ π = (π· Β· (πβπΈ)) & β’ π· < (πβπΈ) & β’ ((π΄βπ) mod π) = (1 mod π) & β’ (((π΄βπΊ) β 1) gcd π) = 1 β β’ π β β | ||
Theorem | unbenlem 16846* | Lemma for unben 16847. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 1) βΎ Ο) β β’ ((π΄ β β β§ βπ β β βπ β π΄ π < π) β π΄ β Ο) | ||
Theorem | unben 16847* | An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ ((π΄ β β β§ βπ β β βπ β π΄ π < π) β π΄ β β) | ||
Theorem | infpnlem1 16848* | Lemma for infpn 16850. The smallest divisor (greater than 1) π of π! + 1 is a prime greater than π. (Contributed by NM, 5-May-2005.) |
β’ πΎ = ((!βπ) + 1) β β’ ((π β β β§ π β β) β (((1 < π β§ (πΎ / π) β β) β§ βπ β β ((1 < π β§ (πΎ / π) β β) β π β€ π)) β (π < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π))))) | ||
Theorem | infpnlem2 16849* | Lemma for infpn 16850. For any positive integer π, there exists a prime number π greater than π. (Contributed by NM, 5-May-2005.) |
β’ πΎ = ((!βπ) + 1) β β’ (π β β β βπ β β (π < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π)))) | ||
Theorem | infpn 16850* | There exist infinitely many prime numbers: for any positive integer π, there exists a prime number π greater than π. (See infpn2 16851 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.) |
β’ (π β β β βπ β β (π < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π)))) | ||
Theorem | infpn2 16851* | There exist infinitely many prime numbers: the set of all primes π is unbounded by infpn 16850, so by unben 16847 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.) |
β’ π = {π β β β£ (1 < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π)))} β β’ π β β | ||
Theorem | prmunb 16852* | The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.) |
β’ (π β β β βπ β β π < π) | ||
Theorem | prminf 16853 | There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.) |
β’ β β β | ||
Theorem | prmreclem1 16854* | Lemma for prmrec 16860. Properties of the "square part" function, which extracts the π of the decomposition π = ππβ2, with π maximal and π squarefree. (Contributed by Mario Carneiro, 5-Aug-2014.) |
β’ π = (π β β β¦ sup({π β β β£ (πβ2) β₯ π}, β, < )) β β’ (π β β β ((πβπ) β β β§ ((πβπ)β2) β₯ π β§ (πΎ β (β€β₯β2) β Β¬ (πΎβ2) β₯ (π / ((πβπ)β2))))) | ||
Theorem | prmreclem2 16855* | Lemma for prmrec 16860. There are at most 2βπΎ squarefree numbers which divide no primes larger than πΎ. (We could strengthen this to 2ββ―(β β© (1...πΎ)) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to πΎ completely determine it because all higher prime counts are zero, and they are all at most 1 because no square divides the number, so there are at most 2βπΎ possibilities. (Contributed by Mario Carneiro, 5-Aug-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (1 / π), 0)) & β’ (π β πΎ β β) & β’ (π β π β β) & β’ π = {π β (1...π) β£ βπ β (β β (1...πΎ)) Β¬ π β₯ π} & β’ π = (π β β β¦ sup({π β β β£ (πβ2) β₯ π}, β, < )) β β’ (π β (β―β{π₯ β π β£ (πβπ₯) = 1}) β€ (2βπΎ)) | ||
Theorem | prmreclem3 16856* | Lemma for prmrec 16860. The main inequality established here is β―π β€ β―{π₯ β π β£ (πβπ₯) = 1} Β· βπ, where {π₯ β π β£ (πβπ₯) = 1} is the set of squarefree numbers in π. This is demonstrated by the map π¦ β¦ β¨π¦ / (πβπ¦)β2, (πβπ¦)β© where πβπ¦ is the largest number whose square divides π¦. (Contributed by Mario Carneiro, 5-Aug-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (1 / π), 0)) & β’ (π β πΎ β β) & β’ (π β π β β) & β’ π = {π β (1...π) β£ βπ β (β β (1...πΎ)) Β¬ π β₯ π} & β’ π = (π β β β¦ sup({π β β β£ (πβ2) β₯ π}, β, < )) β β’ (π β (β―βπ) β€ ((2βπΎ) Β· (ββπ))) | ||
Theorem | prmreclem4 16857* | Lemma for prmrec 16860. Show by induction that the indexed (nondisjoint) union πβπ is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16713, to show that the number of numbers in 1...π that divide π is at most π / π. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (1 / π), 0)) & β’ (π β πΎ β β) & β’ (π β π β β) & β’ π = {π β (1...π) β£ βπ β (β β (1...πΎ)) Β¬ π β₯ π} & β’ (π β seq1( + , πΉ) β dom β ) & β’ (π β Ξ£π β (β€β₯β(πΎ + 1))if(π β β, (1 / π), 0) < (1 / 2)) & β’ π = (π β β β¦ {π β (1...π) β£ (π β β β§ π β₯ π)}) β β’ (π β (π β (β€β₯βπΎ) β (β―ββͺ π β ((πΎ + 1)...π)(πβπ)) β€ (π Β· Ξ£π β ((πΎ + 1)...π)if(π β β, (1 / π), 0)))) | ||
Theorem | prmreclem5 16858* | Lemma for prmrec 16860. Here we show the inequality π / 2 < β―π by decomposing the set (1...π) into the disjoint union of the set π of those numbers that are not divisible by any "large" primes (above πΎ) and the indexed union over πΎ < π of the numbers πβπ that divide the prime π. By prmreclem4 16857 the second of these has size less than π times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part π must be at least π / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (1 / π), 0)) & β’ (π β πΎ β β) & β’ (π β π β β) & β’ π = {π β (1...π) β£ βπ β (β β (1...πΎ)) Β¬ π β₯ π} & β’ (π β seq1( + , πΉ) β dom β ) & β’ (π β Ξ£π β (β€β₯β(πΎ + 1))if(π β β, (1 / π), 0) < (1 / 2)) & β’ π = (π β β β¦ {π β (1...π) β£ (π β β β§ π β₯ π)}) β β’ (π β (π / 2) < ((2βπΎ) Β· (ββπ))) | ||
Theorem | prmreclem6 16859* | Lemma for prmrec 16860. If the series πΉ was convergent, there would be some π such that the sum starting from π + 1 sums to less than 1 / 2; this is a sufficient hypothesis for prmreclem5 16858 to produce the contradictory bound π / 2 < (2βπ)βπ, which is false for π = 2β(2π + 2). (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (1 / π), 0)) β β’ Β¬ seq1( + , πΉ) β dom β | ||
Theorem | prmrec 16860* | The sum of the reciprocals of the primes diverges. Theorem 1.13 in [ApostolNT] p. 18. This is the "second" proof at http://en.wikipedia.org/wiki/Prime_harmonic_series, attributed to Paul ErdΕs. This is Metamath 100 proof #81. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ πΉ = (π β β β¦ Ξ£π β (β β© (1...π))(1 / π)) β β’ Β¬ πΉ β dom β | ||
Theorem | 1arithlem1 16861* | Lemma for 1arith 16865. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) β β’ (π β β β (πβπ) = (π β β β¦ (π pCnt π))) | ||
Theorem | 1arithlem2 16862* | Lemma for 1arith 16865. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) β β’ ((π β β β§ π β β) β ((πβπ)βπ) = (π pCnt π)) | ||
Theorem | 1arithlem3 16863* | Lemma for 1arith 16865. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) β β’ (π β β β (πβπ):ββΆβ0) | ||
Theorem | 1arithlem4 16864* | Lemma for 1arith 16865. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) & β’ πΊ = (π¦ β β β¦ if(π¦ β β, (π¦β(πΉβπ¦)), 1)) & β’ (π β πΉ:ββΆβ0) & β’ (π β π β β) & β’ ((π β§ (π β β β§ π β€ π)) β (πΉβπ) = 0) β β’ (π β βπ₯ β β πΉ = (πβπ₯)) | ||
Theorem | 1arith 16865* | Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function π maps the set of positive integers one-to-one onto the set of prime factorizations π . (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) & β’ π = {π β (β0 βm β) β£ (β‘π β β) β Fin} β β’ π:ββ1-1-ontoβπ | ||
Theorem | 1arith2 16866* | Fundamental theorem of arithmetic, where a prime factorization is represented as a finite monotonic 1-based sequence of primes. Every positive integer has a unique prime factorization. Theorem 1.10 in [ApostolNT] p. 17. This is Metamath 100 proof #80. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) & β’ π = {π β (β0 βm β) β£ (β‘π β β) β Fin} β β’ βπ§ β β β!π β π (πβπ§) = π | ||
Syntax | cgz 16867 | Extend class notation with the set of gaussian integers. |
class β€[i] | ||
Definition | df-gz 16868 | Define the set of gaussian integers, which are complex numbers whose real and imaginary parts are integers. (Note that the [i] is actually part of the symbol token and has no independent meaning.) (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ β€[i] = {π₯ β β β£ ((ββπ₯) β β€ β§ (ββπ₯) β β€)} | ||
Theorem | elgz 16869 | Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β (π΄ β β β§ (ββπ΄) β β€ β§ (ββπ΄) β β€)) | ||
Theorem | gzcn 16870 | A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β π΄ β β) | ||
Theorem | zgz 16871 | An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€ β π΄ β β€[i]) | ||
Theorem | igz 16872 | i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ i β β€[i] | ||
Theorem | gznegcl 16873 | The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β -π΄ β β€[i]) | ||
Theorem | gzcjcl 16874 | The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β (ββπ΄) β β€[i]) | ||
Theorem | gzaddcl 16875 | The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (π΄ + π΅) β β€[i]) | ||
Theorem | gzmulcl 16876 | The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (π΄ Β· π΅) β β€[i]) | ||
Theorem | gzreim 16877 | Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ + (i Β· π΅)) β β€[i]) | ||
Theorem | gzsubcl 16878 | The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (π΄ β π΅) β β€[i]) | ||
Theorem | gzabssqcl 16879 | The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ (π΄ β β€[i] β ((absβπ΄)β2) β β0) | ||
Theorem | 4sqlem5 16880 | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β (π΅ β β€ β§ ((π΄ β π΅) / π) β β€)) | ||
Theorem | 4sqlem6 16881 | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β (-(π / 2) β€ π΅ β§ π΅ < (π / 2))) | ||
Theorem | 4sqlem7 16882 | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β (π΅β2) β€ (((πβ2) / 2) / 2)) | ||
Theorem | 4sqlem8 16883 | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β π β₯ ((π΄β2) β (π΅β2))) | ||
Theorem | 4sqlem9 16884 | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ ((π β§ π) β (π΅β2) = 0) β β’ ((π β§ π) β (πβ2) β₯ (π΄β2)) | ||
Theorem | 4sqlem10 16885 | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ ((π β§ π) β ((((πβ2) / 2) / 2) β (π΅β2)) = 0) β β’ ((π β§ π) β (πβ2) β₯ ((π΄β2) β (((πβ2) / 2) / 2))) | ||
Theorem | 4sqlem1 16886* | Lemma for 4sq 16902. The set π is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that π = β0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ π β β0 | ||
Theorem | 4sqlem2 16887* | Lemma for 4sq 16902. Change bound variables in π. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ (π΄ β π β βπ β β€ βπ β β€ βπ β β€ βπ β β€ π΄ = (((πβ2) + (πβ2)) + ((πβ2) + (πβ2)))) | ||
Theorem | 4sqlem3 16888* | Lemma for 4sq 16902. Sufficient condition to be in π. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π· β β€)) β (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β π) | ||
Theorem | 4sqlem4a 16889* | Lemma for 4sqlem4 16890. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (((absβπ΄)β2) + ((absβπ΅)β2)) β π) | ||
Theorem | 4sqlem4 16890* | Lemma for 4sq 16902. We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ (π΄ β π β βπ’ β β€[i] βπ£ β β€[i] π΄ = (((absβπ’)β2) + ((absβπ£)β2))) | ||
Theorem | mul4sqlem 16891* | Lemma for mul4sq 16892: algebraic manipulations. The extra assumptions involving π are for a part of 4sqlem17 16899 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by π. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π΄ β β€[i]) & β’ (π β π΅ β β€[i]) & β’ (π β πΆ β β€[i]) & β’ (π β π· β β€[i]) & β’ π = (((absβπ΄)β2) + ((absβπ΅)β2)) & β’ π = (((absβπΆ)β2) + ((absβπ·)β2)) & β’ (π β π β β) & β’ (π β ((π΄ β πΆ) / π) β β€[i]) & β’ (π β ((π΅ β π·) / π) β β€[i]) & β’ (π β (π / π) β β0) β β’ (π β ((π / π) Β· (π / π)) β π) | ||
Theorem | mul4sq 16892* | Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 16891. (For the curious, the explicit formula that is used is ( β£ π β£ β2 + β£ π β£ β2)( β£ π β£ β2 + β£ π β£ β2) = β£ πβ Β· π + π Β· πβ β£ β2 + β£ πβ Β· π β π Β· πβ β£ β2.) (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ ((π΄ β π β§ π΅ β π) β (π΄ Β· π΅) β π) | ||
Theorem | 4sqlem11 16893* | Lemma for 4sq 16902. Use the pigeonhole principle to show that the sets {πβ2 β£ π β (0...π)} and {-1 β πβ2 β£ π β (0...π)} have a common element, mod π. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ π΄ = {π’ β£ βπ β (0...π)π’ = ((πβ2) mod π)} & β’ πΉ = (π£ β π΄ β¦ ((π β 1) β π£)) β β’ (π β (π΄ β© ran πΉ) β β ) | ||
Theorem | 4sqlem12 16894* | Lemma for 4sq 16902. For any odd prime π, there is a π < π such that ππ β 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ π΄ = {π’ β£ βπ β (0...π)π’ = ((πβ2) mod π)} & β’ πΉ = (π£ β π΄ β¦ ((π β 1) β π£)) β β’ (π β βπ β (1...(π β 1))βπ’ β β€[i] (((absβπ’)β2) + 1) = (π Β· π)) | ||
Theorem | 4sqlem13 16895* | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) β β’ (π β (π β β β§ π < π)) | ||
Theorem | 4sqlem14 16896* | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) & β’ (π β π β (β€β₯β2)) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β€) & β’ (π β π· β β€) & β’ πΈ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ πΉ = (((π΅ + (π / 2)) mod π) β (π / 2)) & β’ πΊ = (((πΆ + (π / 2)) mod π) β (π / 2)) & β’ π» = (((π· + (π / 2)) mod π) β (π / 2)) & β’ π = ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) & β’ (π β (π Β· π) = (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) β β’ (π β π β β0) | ||
Theorem | 4sqlem15 16897* | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) & β’ (π β π β (β€β₯β2)) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β€) & β’ (π β π· β β€) & β’ πΈ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ πΉ = (((π΅ + (π / 2)) mod π) β (π / 2)) & β’ πΊ = (((πΆ + (π / 2)) mod π) β (π / 2)) & β’ π» = (((π· + (π / 2)) mod π) β (π / 2)) & β’ π = ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) & β’ (π β (π Β· π) = (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) β β’ ((π β§ π = π) β ((((((πβ2) / 2) / 2) β (πΈβ2)) = 0 β§ ((((πβ2) / 2) / 2) β (πΉβ2)) = 0) β§ (((((πβ2) / 2) / 2) β (πΊβ2)) = 0 β§ ((((πβ2) / 2) / 2) β (π»β2)) = 0))) | ||
Theorem | 4sqlem16 16898* | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) & β’ (π β π β (β€β₯β2)) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β€) & β’ (π β π· β β€) & β’ πΈ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ πΉ = (((π΅ + (π / 2)) mod π) β (π / 2)) & β’ πΊ = (((πΆ + (π / 2)) mod π) β (π / 2)) & β’ π» = (((π· + (π / 2)) mod π) β (π / 2)) & β’ π = ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) & β’ (π β (π Β· π) = (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) β β’ (π β (π β€ π β§ ((π = 0 β¨ π = π) β (πβ2) β₯ (π Β· π)))) | ||
Theorem | 4sqlem17 16899* | Lemma for 4sq 16902. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) & β’ (π β π β (β€β₯β2)) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β€) & β’ (π β π· β β€) & β’ πΈ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ πΉ = (((π΅ + (π / 2)) mod π) β (π / 2)) & β’ πΊ = (((πΆ + (π / 2)) mod π) β (π / 2)) & β’ π» = (((π· + (π / 2)) mod π) β (π / 2)) & β’ π = ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) & β’ (π β (π Β· π) = (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) β β’ Β¬ π | ||
Theorem | 4sqlem18 16900* | Lemma for 4sq 16902. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) β β’ (π β π β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |