![]() |
Metamath
Proof Explorer Theorem List (p. 169 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 | pcndvds2 16801 | The remainder after dividing out all factors of π is not divisible by π. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β Β¬ π β₯ (π / (πβ(π pCnt π)))) | ||
Theorem | pcdvdsb 16802 | πβπ΄ divides π if and only if π΄ is at most the count of π. (Contributed by Mario Carneiro, 3-Oct-2014.) |
β’ ((π β β β§ π β β€ β§ π΄ β β0) β (π΄ β€ (π pCnt π) β (πβπ΄) β₯ π)) | ||
Theorem | pcelnn 16803 | There are a positive number of powers of a prime π in π iff π divides π. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β ((π pCnt π) β β β π β₯ π)) | ||
Theorem | pceq0 16804 | There are zero powers of a prime π in π iff π does not divide π. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β ((π pCnt π) = 0 β Β¬ π β₯ π)) | ||
Theorem | pcidlem 16805 | The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ ((π β β β§ π΄ β β0) β (π pCnt (πβπ΄)) = π΄) | ||
Theorem | pcid 16806 | The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ ((π β β β§ π΄ β β€) β (π pCnt (πβπ΄)) = π΄) | ||
Theorem | pcneg 16807 | The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ ((π β β β§ π΄ β β) β (π pCnt -π΄) = (π pCnt π΄)) | ||
Theorem | pcabs 16808 | The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ ((π β β β§ π΄ β β) β (π pCnt (absβπ΄)) = (π pCnt π΄)) | ||
Theorem | pcdvdstr 16809 | The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ ((π β β β§ (π΄ β β€ β§ π΅ β β€ β§ π΄ β₯ π΅)) β (π pCnt π΄) β€ (π pCnt π΅)) | ||
Theorem | pcgcd1 16810 | 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 16811 | 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 16812* | 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 16813* | 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 16814* | 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 16815* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ ((π β β β§ π΄ β β) β (βπ β β0 π΄ β₯ (πβπ) β π΄ = (πβ(π pCnt π΄)))) | ||
Theorem | pcprmpw 16816* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ ((π β β β§ π΄ β β) β (βπ β β0 π΄ = (πβπ) β π΄ = (πβ(π pCnt π΄)))) | ||
Theorem | dvdsprmpweq 16817* | If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.) |
β’ ((π β β β§ π΄ β β β§ π β β0) β (π΄ β₯ (πβπ) β βπ β β0 π΄ = (πβπ))) | ||
Theorem | dvdsprmpweqnn 16818* | 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 16819* | 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 16820 | 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 16821 | Lemma for pcadd 16822. 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 16822 | 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 16823 | The inequality of pcadd 16822 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 16824 | Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) & β’ (π β βπ β β π΄ β β0) β β’ (π β (πΉ:ββΆβ β§ seq1( Β· , πΉ):ββΆβ)) | ||
Theorem | pcmpt 16825* | Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) & β’ (π β βπ β β π΄ β β0) & β’ (π β π β β) & β’ (π β π β β) & β’ (π = π β π΄ = π΅) β β’ (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) | ||
Theorem | pcmpt2 16826* | 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 16827 | 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 16828* | 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 16829* | 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 16830 | 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 16831 | Lemma for pcfac 16832. (Contributed by Mario Carneiro, 20-May-2014.) |
β’ ((π β β0 β§ π β (β€β₯βπ) β§ π β β) β (ββ(π / (πβπ))) = 0) | ||
Theorem | pcfac 16832* | 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 16833* | 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 16834 | 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 16835 | 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 16836* | 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 16837 | A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ (((πΎ β β€ β§ π· β β€) β§ (π β β β§ π β β) β§ (π· β₯ (πΎ Β· (πβπ)) β§ Β¬ π· β₯ (πΎ Β· (πβ(π β 1))))) β (πβπ) β₯ π·) | ||
Theorem | pockthlem 16838 | Lemma for pockthg 16839. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ < π΄) & β’ (π β π = ((π΄ Β· π΅) + 1)) & β’ (π β π β β) & β’ (π β π β₯ π) & β’ (π β π β β) & β’ (π β (π pCnt π΄) β β) & β’ (π β πΆ β β€) & β’ (π β ((πΆβ(π β 1)) mod π) = 1) & β’ (π β (((πΆβ((π β 1) / π)) β 1) gcd π) = 1) β β’ (π β (π pCnt π΄) β€ (π pCnt (π β 1))) | ||
Theorem | pockthg 16839* | 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 16840 | 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 16839 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.) |
β’ π β β & β’ πΊ β β & β’ π = (πΊ Β· π) & β’ π = (π + 1) & β’ π· β β & β’ πΈ β β & β’ π΄ β β & β’ π = (π· Β· (πβπΈ)) & β’ π· < (πβπΈ) & β’ ((π΄βπ) mod π) = (1 mod π) & β’ (((π΄βπΊ) β 1) gcd π) = 1 β β’ π β β | ||
Theorem | unbenlem 16841* | Lemma for unben 16842. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 1) βΎ Ο) β β’ ((π΄ β β β§ βπ β β βπ β π΄ π < π) β π΄ β Ο) | ||
Theorem | unben 16842* | An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ ((π΄ β β β§ βπ β β βπ β π΄ π < π) β π΄ β β) | ||
Theorem | infpnlem1 16843* | Lemma for infpn 16845. 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 16844* | Lemma for infpn 16845. For any positive integer π, there exists a prime number π greater than π. (Contributed by NM, 5-May-2005.) |
β’ πΎ = ((!βπ) + 1) β β’ (π β β β βπ β β (π < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π)))) | ||
Theorem | infpn 16845* | There exist infinitely many prime numbers: for any positive integer π, there exists a prime number π greater than π. (See infpn2 16846 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.) |
β’ (π β β β βπ β β (π < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π)))) | ||
Theorem | infpn2 16846* | There exist infinitely many prime numbers: the set of all primes π is unbounded by infpn 16845, so by unben 16842 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.) |
β’ π = {π β β β£ (1 < π β§ βπ β β ((π / π) β β β (π = 1 β¨ π = π)))} β β’ π β β | ||
Theorem | prmunb 16847* | The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.) |
β’ (π β β β βπ β β π < π) | ||
Theorem | prminf 16848 | There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.) |
β’ β β β | ||
Theorem | prmreclem1 16849* | Lemma for prmrec 16855. 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 16850* | Lemma for prmrec 16855. 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 16851* | Lemma for prmrec 16855. 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 16852* | Lemma for prmrec 16855. Show by induction that the indexed (nondisjoint) union πβπ is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16708, 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 16853* | Lemma for prmrec 16855. 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 16852 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 16854* | Lemma for prmrec 16855. 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 16853 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 16855* | 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 16856* | Lemma for 1arith 16860. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) β β’ (π β β β (πβπ) = (π β β β¦ (π pCnt π))) | ||
Theorem | 1arithlem2 16857* | Lemma for 1arith 16860. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) β β’ ((π β β β§ π β β) β ((πβπ)βπ) = (π pCnt π)) | ||
Theorem | 1arithlem3 16858* | Lemma for 1arith 16860. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) β β’ (π β β β (πβπ):ββΆβ0) | ||
Theorem | 1arithlem4 16859* | Lemma for 1arith 16860. (Contributed by Mario Carneiro, 30-May-2014.) |
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) & β’ πΊ = (π¦ β β β¦ if(π¦ β β, (π¦β(πΉβπ¦)), 1)) & β’ (π β πΉ:ββΆβ0) & β’ (π β π β β) & β’ ((π β§ (π β β β§ π β€ π)) β (πΉβπ) = 0) β β’ (π β βπ₯ β β πΉ = (πβπ₯)) | ||
Theorem | 1arith 16860* | 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 16861* | 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 16862 | Extend class notation with the set of gaussian integers. |
class β€[i] | ||
Definition | df-gz 16863 | 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 16864 | Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β (π΄ β β β§ (ββπ΄) β β€ β§ (ββπ΄) β β€)) | ||
Theorem | gzcn 16865 | A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β π΄ β β) | ||
Theorem | zgz 16866 | An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€ β π΄ β β€[i]) | ||
Theorem | igz 16867 | i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ i β β€[i] | ||
Theorem | gznegcl 16868 | The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β -π΄ β β€[i]) | ||
Theorem | gzcjcl 16869 | The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β€[i] β (ββπ΄) β β€[i]) | ||
Theorem | gzaddcl 16870 | The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (π΄ + π΅) β β€[i]) | ||
Theorem | gzmulcl 16871 | The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (π΄ Β· π΅) β β€[i]) | ||
Theorem | gzreim 16872 | Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ + (i Β· π΅)) β β€[i]) | ||
Theorem | gzsubcl 16873 | The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (π΄ β π΅) β β€[i]) | ||
Theorem | gzabssqcl 16874 | The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ (π΄ β β€[i] β ((absβπ΄)β2) β β0) | ||
Theorem | 4sqlem5 16875 | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β (π΅ β β€ β§ ((π΄ β π΅) / π) β β€)) | ||
Theorem | 4sqlem6 16876 | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β (-(π / 2) β€ π΅ β§ π΅ < (π / 2))) | ||
Theorem | 4sqlem7 16877 | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β (π΅β2) β€ (((πβ2) / 2) / 2)) | ||
Theorem | 4sqlem8 16878 | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) β β’ (π β π β₯ ((π΄β2) β (π΅β2))) | ||
Theorem | 4sqlem9 16879 | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 15-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ ((π β§ π) β (π΅β2) = 0) β β’ ((π β§ π) β (πβ2) β₯ (π΄β2)) | ||
Theorem | 4sqlem10 16880 | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ (π β π΄ β β€) & β’ (π β π β β) & β’ π΅ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ ((π β§ π) β ((((πβ2) / 2) / 2) β (π΅β2)) = 0) β β’ ((π β§ π) β (πβ2) β₯ ((π΄β2) β (((πβ2) / 2) / 2))) | ||
Theorem | 4sqlem1 16881* | Lemma for 4sq 16897. 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 16882* | Lemma for 4sq 16897. Change bound variables in π. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ (π΄ β π β βπ β β€ βπ β β€ βπ β β€ βπ β β€ π΄ = (((πβ2) + (πβ2)) + ((πβ2) + (πβ2)))) | ||
Theorem | 4sqlem3 16883* | Lemma for 4sq 16897. Sufficient condition to be in π. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π· β β€)) β (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β π) | ||
Theorem | 4sqlem4a 16884* | Lemma for 4sqlem4 16885. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ ((π΄ β β€[i] β§ π΅ β β€[i]) β (((absβπ΄)β2) + ((absβπ΅)β2)) β π) | ||
Theorem | 4sqlem4 16885* | Lemma for 4sq 16897. 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 16886* | Lemma for mul4sq 16887: algebraic manipulations. The extra assumptions involving π are for a part of 4sqlem17 16894 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 16887* | 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 16886. (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 16888* | Lemma for 4sq 16897. 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 16889* | Lemma for 4sq 16897. 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 16890* | Lemma for 4sq 16897. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} & β’ (π β π β β) & β’ (π β π = ((2 Β· π) + 1)) & β’ (π β π β β) & β’ (π β (0...(2 Β· π)) β π) & β’ π = {π β β β£ (π Β· π) β π} & β’ π = inf(π, β, < ) β β’ (π β (π β β β§ π < π)) | ||
Theorem | 4sqlem14 16891* | Lemma for 4sq 16897. (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 16892* | Lemma for 4sq 16897. (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 16893* | Lemma for 4sq 16897. (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 16894* | Lemma for 4sq 16897. (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 16895* | Lemma for 4sq 16897. 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(π, β, < ) β β’ (π β π β π) | ||
Theorem | 4sqlem19 16896* | Lemma for 4sq 16897. The proof is by strong induction - we show that if all the integers less than π are in π, then π is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 16895. If π is 0, 1, 2, we show π β π directly; otherwise if π is composite, π is the product of two numbers less than it (and hence in π by assumption), so by mul4sq 16887 π β π. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} β β’ β0 = π | ||
Theorem | 4sq 16897* | Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014.) |
β’ (π΄ β β0 β βπ β β€ βπ β β€ βπ β β€ βπ β β€ π΄ = (((πβ2) + (πβ2)) + ((πβ2) + (πβ2)))) | ||
Syntax | cvdwa 16898 | The arithmetic progression function. |
class AP | ||
Syntax | cvdwm 16899 | The monochromatic arithmetic progression predicate. |
class MonoAP | ||
Syntax | cvdwp 16900 | The polychromatic arithmetic progression predicate. |
class PolyAP |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |