P. 133 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pcid 13201	The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- ( ( P e. Prime /\ A e. ZZ ) -> ( P pCnt ( P ^ A ) ) = A )
Theorem	pcneg 13202	The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt -u A ) = ( P pCnt A ) )
Theorem	pcabs 13203	The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )
Theorem	pcdvdstr 13204	The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) -> ( P pCnt A ) <_ ( P pCnt B ) )
Theorem	pcgcd1 13205	The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( P pCnt A ) <_ ( P pCnt B ) ) -> ( P pCnt ( A gcd B ) ) = ( P pCnt A ) )
Theorem	pcgcd 13206	The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( P pCnt ( A gcd B ) ) = if ( ( P pCnt A ) <_ ( P pCnt B ) , ( P pCnt A ) , ( P pCnt B ) ) )
Theorem	pc2dvds 13207*	A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
Theorem	pc11 13208*	The prime count function, viewed as a function from NN to ( NN ^m Prime ), is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) ) )
Theorem	pcz 13209*	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.)
|- ( A e. QQ -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) )
Theorem	pcprmpw2 13210*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
Theorem	pcprmpw 13211*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A = ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
Theorem	pcaddlem 13212	Lemma for pcadd 13213. The original numbers A and B have been decomposed using the prime count function as ( P ^ M ) x. ( R / S ) where R , S are both not divisible by P and M = ( P pCnt A ), and similarly for B. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- ( ph -> P e. Prime )   &    |- ( ph -> A = ( ( P ^ M ) x. ( R / S ) ) )   &    |- ( ph -> B = ( ( P ^ N ) x. ( T / U ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> ( R e. ZZ /\ -. P || R ) )   &    |- ( ph -> ( S e. NN /\ -. P || S ) )   &    |- ( ph -> ( T e. ZZ /\ -. P || T ) )   &    |- ( ph -> ( U e. NN /\ -. P || U ) )   =>    |- ( ph -> M <_ ( P pCnt ( A + B ) ) )
Theorem	pcadd 13213	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.)
|- ( ph -> P e. Prime )   &    |- ( ph -> A e. QQ )   &    |- ( ph -> B e. QQ )   &    |- ( ph -> ( P pCnt A ) <_ ( P pCnt B ) )   =>    |- ( ph -> ( P pCnt A ) <_ ( P pCnt ( A + B ) ) )
Theorem	pcadd2 13214	The inequality of pcadd 13213 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.)
|- ( ph -> P e. Prime )   &    |- ( ph -> A e. QQ )   &    |- ( ph -> B e. QQ )   &    |- ( ph -> ( P pCnt A ) < ( P pCnt B ) )   =>    |- ( ph -> ( P pCnt A ) = ( P pCnt ( A + B ) ) )
Theorem	pcmptcl 13215	Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )   &    |- ( ph -> A. n e. Prime A e. NN0 )   =>    |- ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
Theorem	pcmpt 13216*	Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )   &    |- ( ph -> A. n e. Prime A e. NN0 )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( n = P -> A = B )   =>    |- ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` N ) ) = if ( P <_ N , B , 0 ) )
Theorem	pcmpt2 13217*	Dividing two prime count maps yields a number with all dividing primes confined to an interval. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )   &    |- ( ph -> A. n e. Prime A e. NN0 )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( n = P -> A = B )   &    |- ( ph -> M e. ( ZZ>= ` N ) )   =>    |- ( ph -> ( P pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )
Theorem	pcmptdvds 13218	The partial products of the prime power map form a divisibility chain. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )   &    |- ( ph -> A. n e. Prime A e. NN0 )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` N ) )   =>    |- ( ph -> ( seq 1 ( x. , F ) ` N ) || ( seq 1 ( x. , F ) ` M ) )
Theorem	pcprod 13219*	The product of the primes taken to their respective powers reconstructs the original number. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( N e. NN -> ( seq 1 ( x. , F ) ` N ) = N )
Theorem	sumhash 13220*	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.)
|- ( ( B e. Fin /\ A C_ B ) -> sum_ k e. B if ( k e. A , 1 , 0 ) = ( # ` A ) )
Theorem	fldivp1 13221	The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014.)
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( |_ ` ( ( M + 1 ) / N ) ) - ( |_ ` ( M / N ) ) ) = if ( N || ( M + 1 ) , 1 , 0 ) )
Theorem	pcfaclem 13222	Lemma for pcfac 13223. (Contributed by Mario Carneiro, 20-May-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )
Theorem	pcfac 13223*	Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( P pCnt ( ! ` N ) ) = sum_ k e. ( 1 ... M ) ( |_ ` ( N / ( P ^ k ) ) ) )
Theorem	pcbc 13224*	Calculate the prime count of a binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
|- ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( N _C K ) ) = sum_ k e. ( 1 ... N ) ( ( |_ ` ( N / ( P ^ k ) ) ) - ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) )
Theorem	qexpz 13225	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.)
|- ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) -> A e. ZZ )
Theorem	expnprm 13226	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.)
|- ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> -. ( A ^ N ) e. Prime )
6.2.6  Pocklington's theorem
Theorem	prmpwdvds 13227	A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
|- ( ( ( K e. ZZ /\ D e. ZZ ) /\ ( P e. Prime /\ N e. NN ) /\ ( D || ( K x. ( P ^ N ) ) /\ -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) ) -> ( P ^ N ) || D )
Theorem	pockthlem 13228	Lemma for pockthg 13229. (Contributed by Mario Carneiro, 2-Mar-2014.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> B < A )   &    |- ( ph -> N = ( ( A x. B ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> P || N )   &    |- ( ph -> Q e. Prime )   &    |- ( ph -> ( Q pCnt A ) e. NN )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> ( ( C ^ ( N - 1 ) ) mod N ) = 1 )   &    |- ( ph -> ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) = 1 )   =>    |- ( ph -> ( Q pCnt A ) <_ ( Q pCnt ( P - 1 ) ) )
Theorem	pockthg 13229*	The generalized Pocklington's theorem. If N - 1 = A x. B where B < A, then N is prime if and only if for every prime factor p of A, there is an x such that x ^ ( N - 1 ) = 1 ( mod N ) and gcd ( x ^ ( ( N - 1 ) / p ) - 1 , N ) = 1. (Contributed by Mario Carneiro, 2-Mar-2014.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> B < A )   &    |- ( ph -> N = ( ( A x. B ) + 1 ) )   &    |- ( ph -> A. p e. Prime ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) )   =>    |- ( ph -> N e. Prime )
Theorem	pockthi 13230	Pocklington's theorem, which gives a sufficient criterion for a number N 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 13229 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.)
|- P e. Prime   &    |- G e. NN   &    |- M = ( G x. P )   &    |- N = ( M + 1 )   &    |- D e. NN   &    |- E e. NN   &    |- A e. NN   &    |- M = ( D x. ( P ^ E ) )   &    |- D < ( P ^ E )   &    |- ( ( A ^ M ) mod N ) = ( 1 mod N )   &    |- ( ( ( A ^ G ) - 1 ) gcd N ) = 1   =>    |- N e. Prime
6.2.7  Infinite primes theorem
Theorem	unbenlem 13231*	Lemma for unben 13232. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )   =>    |- ( ( A C_ NN /\ A. m e. NN E. n e. A m < n ) -> A ~~ om )
Theorem	unben 13232*	An unbounded set of natural numbers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( ( A C_ NN /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )
Theorem	infpnlem1 13233*	Lemma for infpn 13235. The smallest divisor (greater than 1) M of N ! + 1 is a prime greater than N. (Contributed by NM, 5-May-2005.)
|- K = ( ( ! ` N ) + 1 )   =>    |- ( ( N e. NN /\ M e. NN ) -> ( ( ( 1 < M /\ ( K / M ) e. NN ) /\ A. j e. NN ( ( 1 < j /\ ( K / j ) e. NN ) -> M <_ j ) ) -> ( N < M /\ A. j e. NN ( ( M / j ) e. NN -> ( j = 1 \/ j = M ) ) ) ) )
Theorem	infpnlem2 13234*	Lemma for infpn 13235. For any natural number N, there exists a prime number j greater than N. (Contributed by NM, 5-May-2005.)
|- K = ( ( ! ` N ) + 1 )   =>    |- ( N e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) )
Theorem	infpn 13235*	There exist infinitely many prime numbers: for any natural number N, there exists a prime number j greater than N. (See infpn2 13236 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.)
|- ( N e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) )
Theorem	infpn2 13236*	There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn 13235, so by unben 13232 it is infinite. (Contributed by NM, 5-May-2005.)
|- S = { n e. NN | ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) }   =>    |- S ~~ NN
Theorem	prmunb 13237*	The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.)
|- ( N e. NN -> E. p e. Prime N < p )
Theorem	prminf 13238	There are an infinite number of primes. (Contributed by Paul Chapman, 28-Nov-2012.)
|- Prime ~~ NN
6.2.8  Sum of prime reciprocals
Theorem	prmreclem1 13239*	Lemma for prmrec 13245. Properties of the "square part" function, which extracts the m of the decomposition N = r m ^ 2, with m maximal and r squarefree. (Contributed by Mario Carneiro, 5-Aug-2014.)
|- Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )   =>    |- ( N e. NN -> ( ( Q ` N ) e. NN /\ ( ( Q ` N ) ^ 2 ) || N /\ ( K e. ( ZZ>= ` 2 ) -> -. ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) ) )
Theorem	prmreclem2 13240*	Lemma for prmrec 13245. There are at most 2 ^ K squarefree numbers which divide no primes larger than K. (We could strengthen this to 2 ^ # ( Prime i^i ( 1 ... K ) ) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to K 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 ^ K possibilities. (Contributed by Mario Carneiro, 5-Aug-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )   &    |- ( ph -> K e. NN )   &    |- ( ph -> N e. NN )   &    |- M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }   &    |- Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )   =>    |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )
Theorem	prmreclem3 13241*	Lemma for prmrec 13245. The main inequality established here is # M <_ # { x e. M | ( Q ` x ) = 1 } x. sqr N, where { x e. M | ( Q ` x ) = 1 } is the set of squarefree numbers in M. This is demonstrated by the map y |-> <. y / ( Q ` y ) ^ 2 , ( Q ` y ) >. where Q ` y is the largest number whose square divides y. (Contributed by Mario Carneiro, 5-Aug-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )   &    |- ( ph -> K e. NN )   &    |- ( ph -> N e. NN )   &    |- M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }   &    |- Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )   =>    |- ( ph -> ( # ` M ) <_ ( ( 2 ^ K ) x. ( sqr ` N ) ) )
Theorem	prmreclem4 13242*	Lemma for prmrec 13245. Show by induction that the indexed (nondisjoint) union W ` k is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 13119, to show that the number of numbers in 1 ... N that divide k is at most N / k. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )   &    |- ( ph -> K e. NN )   &    |- ( ph -> N e. NN )   &    |- M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }   &    |- ( ph -> seq 1 ( + , F ) e. dom ~~> )   &    |- ( ph -> sum_ k e. ( ZZ>= ` ( K + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) )   &    |- W = ( p e. NN |-> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } )   =>    |- ( ph -> ( N e. ( ZZ>= ` K ) -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
Theorem	prmreclem5 13243*	Lemma for prmrec 13245. Here we show the inequality N / 2 < # M by decomposing the set ( 1 ... N ) into the disjoint union of the set M of those numbers that are not divisible by any "large" primes (above K) and the indexed union over K < k of the numbers W ` k that divide the prime k. By prmreclem4 13242 the second of these has size less than N times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part M must be at least N / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )   &    |- ( ph -> K e. NN )   &    |- ( ph -> N e. NN )   &    |- M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }   &    |- ( ph -> seq 1 ( + , F ) e. dom ~~> )   &    |- ( ph -> sum_ k e. ( ZZ>= ` ( K + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) )   &    |- W = ( p e. NN |-> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } )   =>    |- ( ph -> ( N / 2 ) < ( ( 2 ^ K ) x. ( sqr ` N ) ) )
Theorem	prmreclem6 13244*	Lemma for prmrec 13245. If the series F was convergent, there would be some k such that the sum starting from k + 1 sums to less than 1 / 2; this is a sufficient hypothesis for prmreclem5 13243 to produce the contradictory bound N / 2 < ( 2 ^ k ) sqr N, which is false for N = 2 ^ ( 2 k + 2 ). (Contributed by Mario Carneiro, 6-Aug-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )   =>    |- -. seq 1 ( + , F ) e. dom ~~>
Theorem	prmrec 13245*	The sum of the reciprocals of the primes diverges. This is the "second" proof at http://en.wikipedia.org/wiki/Prime_harmonic_series, attributed to Paul Erdős. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- F = ( n e. NN |-> sum_ k e. ( Prime i^i ( 1 ... n ) ) ( 1 / k ) )   =>    |- -. F e. dom ~~>
6.2.9  Fundamental theorem of arithmetic
Theorem	1arithlem1 13246*	Lemma for 1arith 13250. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( N e. NN -> ( M ` N ) = ( p e. Prime |-> ( p pCnt N ) ) )
Theorem	1arithlem2 13247*	Lemma for 1arith 13250. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( ( N e. NN /\ P e. Prime ) -> ( ( M ` N ) ` P ) = ( P pCnt N ) )
Theorem	1arithlem3 13248*	Lemma for 1arith 13250. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( N e. NN -> ( M ` N ) : Prime --> NN0 )
Theorem	1arithlem4 13249*	Lemma for 1arith 13250. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   &    |- G = ( y e. NN |-> if ( y e. Prime , ( y ^ ( F ` y ) ) , 1 ) )   &    |- ( ph -> F : Prime --> NN0 )   &    |- ( ph -> N e. NN )   &    |- ( ( ph /\ ( q e. Prime /\ N <_ q ) ) -> ( F ` q ) = 0 )   =>    |- ( ph -> E. x e. NN F = ( M ` x ) )
Theorem	1arith 13250*	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 M maps the set of positive integers one-to-one onto the set of prime factorizations R. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   &    |- R = { e e. ( NN0 ^m Prime ) | ( `' e " NN ) e. Fin }   =>    |- M : NN -1-1-onto-> R
Theorem	1arith2 13251*	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. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   &    |- R = { e e. ( NN0 ^m Prime ) | ( `' e " NN ) e. Fin }   =>    |- A. z e. NN E! g e. R ( M ` z ) = g
6.2.10  Lagrange's four-square theorem
Syntax	cgz 13252	Extend class notation with the set of gaussian integers.
class ZZ [ _i ]
Definition	df-gz 13253	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.)
|- ZZ [ _i ] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
Theorem	elgz 13254	Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ [ _i ] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
Theorem	gzcn 13255	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ [ _i ] -> A e. CC )
Theorem	zgz 13256	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> A e. ZZ [ _i ] )
Theorem	igz 13257	_i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- _i e. ZZ [ _i ]
Theorem	gznegcl 13258	The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ [ _i ] -> -u A e. ZZ [ _i ] )
Theorem	gzcjcl 13259	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ [ _i ] -> ( * ` A ) e. ZZ [ _i ] )
Theorem	gzaddcl 13260	The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. ZZ [ _i ] /\ B e. ZZ [ _i ] ) -> ( A + B ) e. ZZ [ _i ] )
Theorem	gzmulcl 13261	The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. ZZ [ _i ] /\ B e. ZZ [ _i ] ) -> ( A x. B ) e. ZZ [ _i ] )
Theorem	gzreim 13262	Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. ZZ [ _i ] )
Theorem	gzsubcl 13263	The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. ZZ [ _i ] /\ B e. ZZ [ _i ] ) -> ( A - B ) e. ZZ [ _i ] )
Theorem	gzabssqcl 13264	The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( A e. ZZ [ _i ] -> ( ( abs ` A ) ^ 2 ) e. NN0 )
Theorem	4sqlem5 13265	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )
Theorem	4sqlem6 13266	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( -u ( M / 2 ) <_ B /\ B < ( M / 2 ) ) )
Theorem	4sqlem7 13267	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( B ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
Theorem	4sqlem8 13268	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> M || ( ( A ^ 2 ) - ( B ^ 2 ) ) )
Theorem	4sqlem9 13269	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- ( ( ph /\ ps ) -> ( B ^ 2 ) = 0 )   =>    |- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( A ^ 2 ) )
Theorem	4sqlem10 13270	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- ( ( ph /\ ps ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( B ^ 2 ) ) = 0 )   =>    |- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
Theorem	4sqlem1 13271*	Lemma for 4sq 13287. The set S is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that S = NN0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- S C_ NN0
Theorem	4sqlem2 13272*	Lemma for 4sq 13287. Change bound variables in S. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( A e. S <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
Theorem	4sqlem3 13273*	Lemma for 4sq 13287. Sufficient condition to be in S. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. S )
Theorem	4sqlem4a 13274*	Lemma for 4sqlem4 13275. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( ( A e. ZZ [ _i ] /\ B e. ZZ [ _i ] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. S )
Theorem	4sqlem4 13275*	Lemma for 4sq 13287. 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.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( A e. S <-> E. u e. ZZ [ _i ] E. v e. ZZ [ _i ] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
Theorem	mul4sqlem 13276*	Lemma for mul4sq 13277: algebraic manipulations. The extra assumptions involving M are for a part of 4sqlem17 13284 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by M. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> A e. ZZ [ _i ] )   &    |- ( ph -> B e. ZZ [ _i ] )   &    |- ( ph -> C e. ZZ [ _i ] )   &    |- ( ph -> D e. ZZ [ _i ] )   &    |- X = ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) )   &    |- Y = ( ( ( abs ` C ) ^ 2 ) + ( ( abs ` D ) ^ 2 ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> ( ( A - C ) / M ) e. ZZ [ _i ] )   &    |- ( ph -> ( ( B - D ) / M ) e. ZZ [ _i ] )   &    |- ( ph -> ( X / M ) e. NN0 )   =>    |- ( ph -> ( ( X / M ) x. ( Y / M ) ) e. S )
Theorem	mul4sq 13277*	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 13276. (For the curious, the explicit formula that is used is ( | a | ^ 2 + | b | ^ 2 ) ( | c | ^ 2 + | d | ^ 2 ) = | a * x. c + b x. d * | ^ 2 + | a * x. d - b x. c * | ^ 2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )
Theorem	4sqlem11 13278*	Lemma for 4sq 13287. Use the pigeonhole principle to show that the sets { m ^ 2 | m e. ( 0 ... N ) } and { -u 1 - n ^ 2 | n e. ( 0 ... N ) } have a common element, mod P. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> ( A i^i ran F ) =/= (/) )
Theorem	4sqlem12 13279*	Lemma for 4sq 13287. For any odd prime P, there is a k < P such that k P - 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> E. k e. ( 1 ... ( P - 1 ) ) E. u e. ZZ [ _i ] ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) )
Theorem	4sqlem13 13280*	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = sup ( T , RR , `' < )   =>    |- ( ph -> ( T =/= (/) /\ M < P ) )
Theorem	4sqlem14 13281*	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = sup ( T , RR , `' < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ph -> R e. NN0 )
Theorem	4sqlem15 13282*	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = sup ( T , RR , `' < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ( ph /\ R = M ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )
Theorem	4sqlem16 13283*	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = sup ( T , RR , `' < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ph -> ( R <_ M /\ ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) ) )
Theorem	4sqlem17 13284*	Lemma for 4sq 13287. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = sup ( T , RR , `' < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- -. ph
Theorem	4sqlem18 13285*	Lemma for 4sq 13287. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = sup ( T , RR , `' < )   =>    |- ( ph -> P e. S )
Theorem	4sqlem19 13286*	Lemma for 4sq 13287. The proof is by strong induction - we show that if all the integers less than k are in S, then k 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 13285. If k is 0 , 1 , 2, we show k e. S directly; otherwise if k is composite, k is the product of two numbers less than it (and hence in S by assumption), so by mul4sq 13277 k e. S. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- NN0 = S
Theorem	4sq 13287*	Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( A e. NN0 <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
6.2.11  Van der Waerden's theorem
Syntax	cvdwa 13288	The arithmetic progression function.
class AP
Syntax	cvdwm 13289	The monochromatic arithmetic progression predicate.
class MonoAP
Syntax	cvdwp 13290	The polychromatic arithmetic progression predicate.
class PolyAP
Definition	df-vdwap 13291*	Define the arithmetic progression function, which takes as input a length k, a start point a, and a step d and outputs the set of points in this progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- AP = ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
Definition	df-vdwmc 13292*	Define the "contains a monochromatic AP" predicate. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- MonoAP = { <. k , f >. | E. c ( ran (AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }
Definition	df-vdwpc 13293*	Define the "contains a polychromatic colleciton of APs" predicate. See vdwpc 13303 for more information. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- PolyAP = { <. <. m , k >. , f >. | E. a e. NN E. d e. ( NN ^m ( 1 ... m ) ) ( A. i e. ( 1 ... m ) ( ( a + ( d ` i ) ) (AP ` k ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = m ) }
Theorem	vdwapfval 13294*	Define the arithmetic progression function, which takes as input a length k, a start point a, and a step d and outputs the set of points in this progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( K e. NN0 -> (AP ` K ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
Theorem	vdwapf 13295	The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( K e. NN0 -> (AP ` K ) : ( NN X. NN ) --> ~P NN )
Theorem	vdwapval 13296*	Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( X e. ( A (AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) ) )
Theorem	vdwapun 13297	Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014.)
|- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A (AP ` ( K + 1 ) ) D ) = ( { A } u. ( ( A + D ) (AP ` K ) D ) ) )
Theorem	vdwapid1 13298	The first element of an arithmetic progression. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A (AP ` K ) D ) )
Theorem	vdwap0 13299	Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ( A e. NN /\ D e. NN ) -> ( A (AP ` 0 ) D ) = (/) )
Theorem	vdwap1 13300	Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ( A e. NN /\ D e. NN ) -> ( A (AP ` 1 ) D ) = { A } )