P. 128 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pcqmul 12701	Multiplication property of the prime power function. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) )
Theorem	pc0 12702	The value of the prime power function at zero. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( P e. Prime -> ( P pCnt 0 ) = +oo )
Theorem	pc1 12703	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( P e. Prime -> ( P pCnt 1 ) = 0 )
Theorem	pcqcl 12704	Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) e. ZZ )
Theorem	pcqdiv 12705	Division property of the prime power function. (Contributed by Mario Carneiro, 10-Aug-2015.)
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( P pCnt ( A / B ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) )
Theorem	pcrec 12706	Prime power of a reciprocal. (Contributed by Mario Carneiro, 10-Aug-2015.)
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( 1 / A ) ) = -u ( P pCnt A ) )
Theorem	pcexp 12707	Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015.)
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ N e. ZZ ) -> ( P pCnt ( A ^ N ) ) = ( N x. ( P pCnt A ) ) )
Theorem	pcxnn0cl 12708	Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
|- ( ( P e. Prime /\ N e. ZZ ) -> ( P pCnt N ) e. NN0* )
Theorem	pcxcl 12709	Extended real closure of the general prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( P e. Prime /\ N e. QQ ) -> ( P pCnt N ) e. RR* )
Theorem	pcxqcl 12710	The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.)
|- ( ( P e. Prime /\ N e. QQ ) -> ( ( P pCnt N ) e. ZZ \/ ( P pCnt N ) = +oo ) )
Theorem	pcge0 12711	The prime count of an integer is greater than or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( P e. Prime /\ N e. ZZ ) -> 0 <_ ( P pCnt N ) )
Theorem	pczdvds 12712	Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( P pCnt N ) ) || N )
Theorem	pcdvds 12713	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ N e. NN ) -> ( P ^ ( P pCnt N ) ) || N )
Theorem	pczndvds 12714	Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )
Theorem	pcndvds 12715	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ N e. NN ) -> -. ( P ^ ( ( P pCnt N ) + 1 ) ) || N )
Theorem	pczndvds2 12716	The remainder after dividing out all factors of P is not divisible by P. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ ( P pCnt N ) ) ) )
Theorem	pcndvds2 12717	The remainder after dividing out all factors of P is not divisible by P. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ N e. NN ) -> -. P || ( N / ( P ^ ( P pCnt N ) ) ) )
Theorem	pcdvdsb 12718	P ^ A divides N if and only if A is at most the count of P. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( P e. Prime /\ N e. ZZ /\ A e. NN0 ) -> ( A <_ ( P pCnt N ) <-> ( P ^ A ) || N ) )
Theorem	pcelnn 12719	There are a positive number of powers of a prime P in N iff P divides N. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> P || N ) )
Theorem	pceq0 12720	There are zero powers of a prime P in N iff P does not divide N. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) = 0 <-> -. P || N ) )
Theorem	pcidlem 12721	The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) = A )
Theorem	pcid 12722	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 12723	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 12724	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 12725	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 12726	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 12727	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 12728*	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 12729*	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 12730*	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 12731*	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 12732*	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	dvdsprmpweq 12733*	If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.)
|- ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 A = ( P ^ n ) ) )
Theorem	dvdsprmpweqnn 12734*	If an integer greater than 1 divides a prime power, it is a (proper) prime power. (Contributed by AV, 13-Aug-2021.)
|- ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) )
Theorem	dvdsprmpweqle 12735*	If a positive integer divides a prime power, it is a prime power with a smaller exponent. (Contributed by AV, 25-Jul-2021.)
|- ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 ( n <_ N /\ A = ( P ^ n ) ) ) )
Theorem	difsqpwdvds 12736	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.)
|- ( ( ( A e. NN0 /\ B e. NN0 /\ ( B + 1 ) < A ) /\ ( C e. Prime /\ D e. NN0 ) ) -> ( ( C ^ D ) = ( ( A ^ 2 ) - ( B ^ 2 ) ) -> C || ( 2 x. B ) ) )
Theorem	pcaddlem 12737	Lemma for pcadd 12738. 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 12738	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 12739	The inequality of pcadd 12738 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 12740	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 12741*	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 12742*	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 12743	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 12744*	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	sumhashdc 12745*	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 /\ A. x e. B DECID x e. A ) -> sum_ k e. B if ( k e. A , 1 , 0 ) = (♯ ` A ) )
Theorem	fldivp1 12746	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 12747	Lemma for pcfac 12748. (Contributed by Mario Carneiro, 20-May-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )
Theorem	pcfac 12748*	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 12749*	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 12750	If a power of a rational number is an integer, then the number is an integer. (Contributed by Mario Carneiro, 10-Aug-2015.)
|- ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) -> A e. ZZ )
Theorem	expnprm 12751	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 not rational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015.)
|- ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> -. ( A ^ N ) e. Prime )
Theorem	oddprmdvds 12752*	Every positive integer which is not a power of two is divisible by an odd prime number. (Contributed by AV, 6-Aug-2021.)
|- ( ( K e. NN /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> E. p e. ( Prime \ { 2 } ) p || K )
5.2.9  Pocklington's theorem
Theorem	prmpwdvds 12753	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 12754	Lemma for pockthg 12755. (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 12755*	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 12756	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 12755 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
5.2.10  Infinite primes theorem
Theorem	infpnlem1 12757*	Lemma for infpn 12759. 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 12758*	Lemma for infpn 12759. For any positive integer 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 12759*	There exist infinitely many prime numbers: for any positive integer N, there exists a prime number j greater than N. (See infpn2 12902 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	prmunb 12760*	The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.)
|- ( N e. NN -> E. p e. Prime N < p )
5.2.11  Fundamental theorem of arithmetic
Theorem	1arithlem1 12761*	Lemma for 1arith 12765. (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 12762*	Lemma for 1arith 12765. (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 12763*	Lemma for 1arith 12765. (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 12764*	Lemma for 1arith 12765. (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 12765*	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 12766*	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.)
|- 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
5.2.12  Lagrange's four-square theorem
Syntax	cgz 12767	Extend class notation with the set of gaussian integers.
class ZZ[_i]
Definition	df-gz 12768	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 12769	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 12770	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> A e. CC )
Theorem	zgz 12771	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> A e. ZZ[_i] )
Theorem	igz 12772	_i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- _i e. ZZ[_i]
Theorem	gznegcl 12773	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 12774	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> ( * ` A ) e. ZZ[_i] )
Theorem	gzaddcl 12775	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 12776	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 12777	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 12778	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 12779	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 12780	Lemma for 4sq 12808. (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 12781	Lemma for 4sq 12808. (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 12782	Lemma for 4sq 12808. (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 12783	Lemma for 4sq 12808. (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 12784	Lemma for 4sq 12808. (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 12785	Lemma for 4sq 12808. (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 12786*	Lemma for 4sq 12808. 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 12787*	Lemma for 4sq 12808. 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 12788*	Lemma for 4sq 12808. 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 12789*	Lemma for 4sqlem4 12790. (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 12790*	Lemma for 4sq 12808. 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 12791*	Lemma for mul4sq 12792: algebraic manipulations. The extra assumptions involving M would let us 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 12792*	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 12791. (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	4sqlemafi 12793*	Lemma for 4sq 12808. A is finite. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. NN )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   =>    |- ( ph -> A e. Fin )
Theorem	4sqlemffi 12794*	Lemma for 4sq 12808. ran F is finite. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. NN )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> ran F e. Fin )
Theorem	4sqleminfi 12795*	Lemma for 4sq 12808. A i^i ran F is finite. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. NN )   &    |- 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 ) e. Fin )
Theorem	4sqexercise1 12796*	Exercise which may help in understanding the proof of 4sqlemsdc 12798. (Contributed by Jim Kingdon, 25-May-2025.)
|- S = { n | E. x e. ZZ n = ( x ^ 2 ) }   =>    |- ( A e. NN0 -> DECID A e. S )
Theorem	4sqexercise2 12797*	Exercise which may help in understanding the proof of 4sqlemsdc 12798. (Contributed by Jim Kingdon, 30-May-2025.)
|- S = { n | E. x e. ZZ E. y e. ZZ n = ( ( x ^ 2 ) + ( y ^ 2 ) ) }   =>    |- ( A e. NN0 -> DECID A e. S )
Theorem	4sqlemsdc 12798*	Lemma for 4sq 12808. The property of being the sum of four squares is decidable. The proof involves showing that (for a particular A) there are only a finite number of possible ways that it could be the sum of four squares, so checking each of those possibilities in turn decides whether the number is the sum of four squares. If this proof is hard to follow, especially because of its length, the simplified versions at 4sqexercise1 12796 and 4sqexercise2 12797 may help clarify, as they are using very much the same techniques on simplified versions of this lemma. (Contributed by Jim Kingdon, 25-May-2025.)
|- 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. NN0 -> DECID A e. S )
Theorem	4sqlem11 12799*	Lemma for 4sq 12808. 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. Note that although the conclusion is stated in terms of A i^i ran F being nonempty, it is also inhabited by 4sqleminfi 12795 and fin0 6997. (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 12800*	Lemma for 4sq 12808. 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 ) )