P. 131 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13001-13100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pcqmul 13001	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 13002	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 13003	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( P e. Prime -> ( P pCnt 1 ) = 0 )
Theorem	pcqcl 13004	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 13005	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 13006	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 13007	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 13008	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 13009	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 13010	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 13011	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 13012	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 13013	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 13014	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 13015	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 13016	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 13017	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 13018	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 13019	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 13020	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 13021	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 13022	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 13023	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 13024	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 13025	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 13026	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 13027	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 13028*	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 13029*	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 13030*	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 13031*	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 13032*	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 13033*	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 13034*	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 13035*	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 13036	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 13037	Lemma for pcadd 13038. 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 13038	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 13039	The inequality of pcadd 13038 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 13040	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 13041*	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 13042*	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 13043	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 13044*	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 13045*	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 13046	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 13047	Lemma for pcfac 13048. (Contributed by Mario Carneiro, 20-May-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )
Theorem	pcfac 13048*	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 13049*	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 13050	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 13051	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 13052*	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 13053	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 13054	Lemma for pockthg 13055. (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 13055*	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 13056	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 13055 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 13057*	Lemma for infpn 13059. 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 13058*	Lemma for infpn 13059. 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 13059*	There exist infinitely many prime numbers: for any positive integer N, there exists a prime number j greater than N. (See infpn2 13207 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 13060*	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 13061*	Lemma for 1arith 13065. (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 13062*	Lemma for 1arith 13065. (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 13063*	Lemma for 1arith 13065. (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 13064*	Lemma for 1arith 13065. (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 13065*	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 13066*	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 13067	Extend class notation with the set of gaussian integers.
class ZZ[_i]
Definition	df-gz 13068	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 13069	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 13070	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> A e. CC )
Theorem	zgz 13071	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> A e. ZZ[_i] )
Theorem	igz 13072	_i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- _i e. ZZ[_i]
Theorem	gznegcl 13073	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 13074	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> ( * ` A ) e. ZZ[_i] )
Theorem	gzaddcl 13075	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 13076	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 13077	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 13078	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 13079	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 13080	Lemma for 4sq 13108. (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 13081	Lemma for 4sq 13108. (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 13082	Lemma for 4sq 13108. (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 13083	Lemma for 4sq 13108. (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 13084	Lemma for 4sq 13108. (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 13085	Lemma for 4sq 13108. (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 13086*	Lemma for 4sq 13108. 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 13087*	Lemma for 4sq 13108. 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 13088*	Lemma for 4sq 13108. 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 13089*	Lemma for 4sqlem4 13090. (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 13090*	Lemma for 4sq 13108. 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 13091*	Lemma for mul4sq 13092: 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 13092*	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 13091. (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 13093*	Lemma for 4sq 13108. 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 13094*	Lemma for 4sq 13108. 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 13095*	Lemma for 4sq 13108. 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 13096*	Exercise which may help in understanding the proof of 4sqlemsdc 13098. (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 13097*	Exercise which may help in understanding the proof of 4sqlemsdc 13098. (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 13098*	Lemma for 4sq 13108. 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 13096 and 4sqexercise2 13097 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 13099*	Lemma for 4sq 13108. 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 13095 and fin0 7142. (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 13100*	Lemma for 4sq 13108. 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 ) )