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	odzid 13001	Any element raised to the power of its order is 1. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) )
Theorem	odzdvds 13002	The only powers of A that are congruent to 1 are the multiples of the order of A. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( N || ( ( A ^ K ) - 1 ) <-> ( ( odZ ` N ) ` A ) || K ) )
Theorem	odzphi 13003	The order of any group element is a divisor of the Euler phi function. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) || ( phi ` N ) )
5.2.6  Arithmetic modulo a prime number
Theorem	modprm1div 13004	A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) (Proof shortened by AV, 30-May-2023.)
|- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 1 <-> P || ( A - 1 ) ) )
Theorem	m1dvdsndvds 13005	If an integer minus 1 is divisible by a prime number, the integer itself is not divisible by this prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A - 1 ) -> -. P || A ) )
Theorem	modprminv 13006	Show an explicit expression for the modular inverse of A mod P. This is an application of prmdiv 12991. (Contributed by Alexander van der Vekens, 15-May-2018.)
|- R = ( ( A ^ ( P - 2 ) ) mod P )   =>    |- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ ( ( A x. R ) mod P ) = 1 ) )
Theorem	modprminveq 13007	The modular inverse of A mod P is unique. (Contributed by Alexander van der Vekens, 17-May-2018.)
|- R = ( ( A ^ ( P - 2 ) ) mod P )   =>    |- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ ( ( A x. S ) mod P ) = 1 ) <-> S = R ) )
Theorem	vfermltl 13008	Variant of Fermat's little theorem if A is not a multiple of P, see theorem 5.18 in [ApostolNT] p. 113. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 5-Sep-2020.)
|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = 1 )
Theorem	powm2modprm 13009	If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A - 1 ) -> ( ( A ^ ( P - 2 ) ) mod P ) = 1 ) )
Theorem	reumodprminv 13010*	For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018.)
|- ( ( P e. Prime /\ N e. ( 1..^ P ) ) -> E! i e. ( 1 ... ( P - 1 ) ) ( ( N x. i ) mod P ) = 1 )
Theorem	modprm0 13011*	For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.)
|- ( ( P e. Prime /\ N e. ( 1..^ P ) /\ I e. ( 1..^ P ) ) -> E. j e. ( 0..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
Theorem	nnnn0modprm0 13012*	For a positive integer and a nonnegative integer both less than a given prime number there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the positive integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 8-Nov-2018.)
|- ( ( P e. Prime /\ N e. ( 1..^ P ) /\ I e. ( 0..^ P ) ) -> E. j e. ( 0..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 )
Theorem	modprmn0modprm0 13013*	For an integer not being 0 modulo a given prime number and a nonnegative integer less than the prime number, there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 10-Nov-2018.)
|- ( ( P e. Prime /\ N e. ZZ /\ ( N mod P ) =/= 0 ) -> ( I e. ( 0..^ P ) -> E. j e. ( 0..^ P ) ( ( I + ( j x. N ) ) mod P ) = 0 ) )
5.2.7  Pythagorean Triples
Theorem	coprimeprodsq 13014	If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) -> A = ( ( A gcd C ) ^ 2 ) ) )
Theorem	coprimeprodsq2 13015	If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) -> B = ( ( B gcd C ) ^ 2 ) ) )
Theorem	oddprm 13016	A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
|- ( N e. ( Prime \ { 2 } ) -> ( ( N - 1 ) / 2 ) e. NN )
Theorem	nnoddn2prm 13017	A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021.)
|- ( N e. ( Prime \ { 2 } ) -> ( N e. NN /\ -. 2 || N ) )
Theorem	oddn2prm 13018	A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.)
|- ( N e. ( Prime \ { 2 } ) -> -. 2 || N )
Theorem	nnoddn2prmb 13019	A number is a prime number not equal to 2 iff it is an odd prime number. Conversion theorem for two representations of odd primes. (Contributed by AV, 14-Jul-2021.)
|- ( N e. ( Prime \ { 2 } ) <-> ( N e. Prime /\ -. 2 || N ) )
Theorem	prm23lt5 13020	A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
|- ( ( P e. Prime /\ P < 5 ) -> ( P = 2 \/ P = 3 ) )
Theorem	prm23ge5 13021	A prime is either 2 or 3 or greater than or equal to 5. (Contributed by AV, 5-Jul-2021.)
|- ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) )
Theorem	pythagtriplem1 13022*	Lemma for pythagtrip 13040. Prove a weaker version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( 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 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
Theorem	pythagtriplem2 13023*	Lemma for pythagtrip 13040. Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( 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 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
Theorem	pythagtriplem3 13024	Lemma for pythagtrip 13040. Show that C and B are relatively prime under some conditions. (Contributed by Scott Fenton, 8-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 ) ) -> ( B gcd C ) = 1 )
Theorem	pythagtriplem4 13025	Lemma for pythagtrip 13040. Show that C - B and C + B are relatively prime. (Contributed by Scott Fenton, 12-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 ) ) -> ( ( C - B ) gcd ( C + B ) ) = 1 )
Theorem	pythagtriplem10 13026	Lemma for pythagtrip 13040. Show that C - B is positive. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )
Theorem	pythagtriplem6 13027	Lemma for pythagtrip 13040. Calculate ( sqr ` ( C - B ) ). (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 ) ) -> ( sqr ` ( C - B ) ) = ( ( C - B ) gcd A ) )
Theorem	pythagtriplem7 13028	Lemma for pythagtrip 13040. Calculate ( sqr ` ( C + B ) ). (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 ) ) -> ( sqr ` ( C + B ) ) = ( ( C + B ) gcd A ) )
Theorem	pythagtriplem8 13029	Lemma for pythagtrip 13040. Show that ( sqr ` ( C - B ) ) is a positive integer. (Contributed by Scott Fenton, 17-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 ) ) -> ( sqr ` ( C - B ) ) e. NN )
Theorem	pythagtriplem9 13030	Lemma for pythagtrip 13040. Show that ( sqr ` ( C + B ) ) is a positive integer. (Contributed by Scott Fenton, 17-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 ) ) -> ( sqr ` ( C + B ) ) e. NN )
Theorem	pythagtriplem11 13031	Lemma for pythagtrip 13040. Show that M (which will eventually be closely related to the m in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- M = ( ( ( 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 ) ) -> M e. NN )
Theorem	pythagtriplem12 13032	Lemma for pythagtrip 13040. Calculate the square of M. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- M = ( ( ( 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 ) ) -> ( M ^ 2 ) = ( ( C + A ) / 2 ) )
Theorem	pythagtriplem13 13033	Lemma for pythagtrip 13040. Show that N (which will eventually be closely related to the n in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- 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 ) ) -> N e. NN )
Theorem	pythagtriplem14 13034	Lemma for pythagtrip 13040. Calculate the square of N. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- 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 ) ) -> ( N ^ 2 ) = ( ( C - A ) / 2 ) )
Theorem	pythagtriplem15 13035	Lemma for pythagtrip 13040. 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 13036	Lemma for pythagtrip 13040. 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 13037	Lemma for pythagtrip 13040. 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 13038*	Lemma for pythagtrip 13040. 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 13039*	Lemma for pythagtrip 13040. 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 13040*	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 13041	Extend class notation with the prime count function.
class pCnt
Definition	df-pc 13042*	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 13043*	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 13044*	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 13045*	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 13046*	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 13047*	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 13048*	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 13049*	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 13050*	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 13051*	Lemma for pceu 13052. (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 13052*	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 13053*	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 13054*	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 13055	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 13056	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 13057	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 13058	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 13059	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 13060	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 13061	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 13062	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( P e. Prime -> ( P pCnt 1 ) = 0 )
Theorem	pcqcl 13063	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 13064	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 13065	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 13066	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 13067	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 13068	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 13069	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 13070	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 13071	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 13072	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 13073	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 13074	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 13075	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 13076	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 13077	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 13078	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 13079	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 13080	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 13081	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 13082	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 13083	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 13084	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 13085	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 13086	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 13087*	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 13088*	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 13089*	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 13090*	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 13091*	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 13092*	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 13093*	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 13094*	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 13095	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 13096	Lemma for pcadd 13097. 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 13097	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 13098	The inequality of pcadd 13097 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 13099	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 13100*	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 ) )