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	pythagtriplem15 13001	Lemma for pythagtrip 13006. Show the relationship between M, N, and A. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- M = ( ( ( sqr ` ( C + B ) ) + ( sqr ` ( C - B ) ) ) / 2 )   &    |- N = ( ( ( sqr ` ( C + B ) ) - ( sqr ` ( C - B ) ) ) / 2 )   =>    |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A = ( ( M ^ 2 ) - ( N ^ 2 ) ) )
Theorem	pythagtriplem16 13002	Lemma for pythagtrip 13006. Show the relationship between M, N, and B. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- M = ( ( ( sqr ` ( C + B ) ) + ( sqr ` ( C - B ) ) ) / 2 )   &    |- N = ( ( ( sqr ` ( C + B ) ) - ( sqr ` ( C - B ) ) ) / 2 )   =>    |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B = ( 2 x. ( M x. N ) ) )
Theorem	pythagtriplem17 13003	Lemma for pythagtrip 13006. Show the relationship between M, N, and C. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- M = ( ( ( sqr ` ( C + B ) ) + ( sqr ` ( C - B ) ) ) / 2 )   &    |- N = ( ( ( sqr ` ( C + B ) ) - ( sqr ` ( C - B ) ) ) / 2 )   =>    |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C = ( ( M ^ 2 ) + ( N ^ 2 ) ) )
Theorem	pythagtriplem18 13004*	Lemma for pythagtrip 13006. Wrap the previous M and N up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> E. n e. NN E. m e. NN ( A = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ B = ( 2 x. ( m x. n ) ) /\ C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
Theorem	pythagtriplem19 13005*	Lemma for pythagtrip 13006. Introduce k and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
Theorem	pythagtrip 13006*	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 13007	Extend class notation with the prime count function.
class pCnt
Definition	df-pc 13008*	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 13009*	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 13010*	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 13011*	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 13012*	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 13013*	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 13014*	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 13015*	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 13016*	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 13017*	Lemma for pceu 13018. (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 13018*	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 13019*	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 13020*	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 13021	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 13022	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 13023	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 13024	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 13025	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 13026	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 13027	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 13028	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( P e. Prime -> ( P pCnt 1 ) = 0 )
Theorem	pcqcl 13029	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 13030	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 13031	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 13032	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 13033	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 13034	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 13035	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 13036	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 13037	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 13038	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 13039	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 13040	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 13041	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 13042	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 13043	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 13044	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 13045	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 13046	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 13047	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 13048	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 13049	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 13050	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 13051	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 13052	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 13053*	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 13054*	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 13055*	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 13056*	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 13057*	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 13058*	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 13059*	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 13060*	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 13061	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 13062	Lemma for pcadd 13063. 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 13063	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 13064	The inequality of pcadd 13063 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 13065	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 13066*	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 13067*	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 13068	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 13069*	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 13070*	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 13071	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 13072	Lemma for pcfac 13073. (Contributed by Mario Carneiro, 20-May-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( |_ ` ( N / ( P ^ M ) ) ) = 0 )
Theorem	pcfac 13073*	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 13074*	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 13075	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 13076	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 13077*	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 13078	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 13079	Lemma for pockthg 13080. (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 13080*	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 13081	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 13080 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 13082*	Lemma for infpn 13084. 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 13083*	Lemma for infpn 13084. 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 13084*	There exist infinitely many prime numbers: for any positive integer N, there exists a prime number j greater than N. (See infpn2 13291 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 13085*	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 13086*	Lemma for 1arith 13090. (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 13087*	Lemma for 1arith 13090. (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 13088*	Lemma for 1arith 13090. (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 13089*	Lemma for 1arith 13090. (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 13090*	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 13091*	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 13092	Extend class notation with the set of gaussian integers.
class ZZ[_i]
Definition	df-gz 13093	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 13094	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 13095	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> A e. CC )
Theorem	zgz 13096	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> A e. ZZ[_i] )
Theorem	igz 13097	_i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- _i e. ZZ[_i]
Theorem	gznegcl 13098	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 13099	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> ( * ` A ) e. ZZ[_i] )
Theorem	gzaddcl 13100	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] )