P. 124 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12301-12400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pythagtrip 12301*	Parameterize the Pythagorean triples. If A, B, and C are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml. This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.)
|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
5.2.8  The prime count function
Syntax	cpc 12302	Extend class notation with the prime count function.
class pCnt
Definition	df-pc 12303*	Define the prime count function, which returns the largest exponent of a given prime (or other positive integer) that divides the number. For rational numbers, it returns negative values according to the power of a prime in the denominator. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- pCnt = ( p e. Prime , r e. QQ |-> if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) ) )
Theorem	pclem0 12304*	Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
|- A = { n e. NN0 | ( P ^ n ) || N }   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> 0 e. A )
Theorem	pclemub 12305*	Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
|- A = { n e. NN0 | ( P ^ n ) || N }   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> E. x e. ZZ A. y e. A y <_ x )
Theorem	pclemdc 12306*	Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.)
|- A = { n e. NN0 | ( P ^ n ) || N }   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> A. x e. ZZ DECID x e. A )
Theorem	pcprecl 12307*	Closure of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- A = { n e. NN0 | ( P ^ n ) || N }   &    |- S = sup ( A , RR , < )   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
Theorem	pcprendvds 12308*	Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- A = { n e. NN0 | ( P ^ n ) || N }   &    |- S = sup ( A , RR , < )   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( S + 1 ) ) || N )
Theorem	pcprendvds2 12309*	Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- A = { n e. NN0 | ( P ^ n ) || N }   &    |- S = sup ( A , RR , < )   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ S ) ) )
Theorem	pcpre1 12310*	Value of the prime power pre-function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 26-Apr-2016.)
|- A = { n e. NN0 | ( P ^ n ) || N }   &    |- S = sup ( A , RR , < )   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ N = 1 ) -> S = 0 )
Theorem	pcpremul 12311*	Multiplicative property of the prime count pre-function. Note that the primality of P is essential for this property; ( 4 pCnt 2 ) = 0 but ( 4 pCnt ( 2 x. 2 ) ) = 1 =/= 2 x. ( 4 pCnt 2 ) = 0. Since this is needed to show uniqueness for the real prime count function (over QQ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- S = sup ( { n e. NN0 | ( P ^ n ) || M } , RR , < )   &    |- T = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )   &    |- U = sup ( { n e. NN0 | ( P ^ n ) || ( M x. N ) } , RR , < )   =>    |- ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) = U )
Theorem	pceulem 12312*	Lemma for pceu 12313. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )   &    |- T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )   &    |- U = sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < )   &    |- V = sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> N =/= 0 )   &    |- ( ph -> ( x e. ZZ /\ y e. NN ) )   &    |- ( ph -> N = ( x / y ) )   &    |- ( ph -> ( s e. ZZ /\ t e. NN ) )   &    |- ( ph -> N = ( s / t ) )   =>    |- ( ph -> ( S - T ) = ( U - V ) )
Theorem	pceu 12313*	Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )   &    |- T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )   =>    |- ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
Theorem	pcval 12314*	The value of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
|- S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )   &    |- T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )   =>    |- ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) = ( iota z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) ) )
Theorem	pczpre 12315*	Connect the prime count pre-function to the actual prime count function, when restricted to the integers. (Contributed by Mario Carneiro, 23-Feb-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- S = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )   =>    |- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) = S )
Theorem	pczcl 12316	Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P pCnt N ) e. NN0 )
Theorem	pccl 12317	Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ N e. NN ) -> ( P pCnt N ) e. NN0 )
Theorem	pccld 12318	Closure of the prime power function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> P e. Prime )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( P pCnt N ) e. NN0 )
Theorem	pcmul 12319	Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) )
Theorem	pcdiv 12320	Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014.)
|- ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( P pCnt ( A / B ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) )
Theorem	pcqmul 12321	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 12322	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 12323	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( P e. Prime -> ( P pCnt 1 ) = 0 )
Theorem	pcqcl 12324	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 12325	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 12326	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 12327	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 12328	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 12329	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	pcge0 12330	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 12331	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 12332	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 12333	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 12334	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 12335	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 12336	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 12337	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 12338	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 12339	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 12340	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 12341	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 12342	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 12343	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 12344	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 12345	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 12346	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 12347*	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 12348*	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 12349*	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 12350*	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 12351*	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 12352*	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 12353*	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 12354*	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 12355	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 12356	Lemma for pcadd 12357. 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 12357	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	pcmptcl 12358	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 12359*	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 12360*	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 12361	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 12362*	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 12363*	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 12364	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 12365	Lemma for pcfac 12366. (Contributed by Mario Carneiro, 20-May-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )
Theorem	pcfac 12366*	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 12367*	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 12368	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 12369	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 12370*	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 12371	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 12372	Lemma for pockthg 12373. (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 12373*	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 12374	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 12373 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 12375*	Lemma for infpn 12377. 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 12376*	Lemma for infpn 12377. 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 12377*	There exist infinitely many prime numbers: for any positive integer N, there exists a prime number j greater than N. (See infpn2 12475 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 12378*	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 12379*	Lemma for 1arith 12383. (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 12380*	Lemma for 1arith 12383. (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 12381*	Lemma for 1arith 12383. (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 12382*	Lemma for 1arith 12383. (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 12383*	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 12384*	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 12385	Extend class notation with the set of gaussian integers.
class ZZ[_i]
Definition	df-gz 12386	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 12387	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 12388	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> A e. CC )
Theorem	zgz 12389	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> A e. ZZ[_i] )
Theorem	igz 12390	_i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- _i e. ZZ[_i]
Theorem	gznegcl 12391	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 12392	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> ( * ` A ) e. ZZ[_i] )
Theorem	gzaddcl 12393	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 12394	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 12395	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 12396	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 12397	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 12398	Lemma for 4sq (not yet proved here). (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 12399	Lemma for 4sq (not yet proved here) . (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 12400	Lemma for 4sq (not yet proved here) . (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 ) )