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	divdenle 13001	Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. ZZ /\ B e. NN ) -> (denom ` ( A / B ) ) <_ B )
Theorem	qnumgt0 13002	A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( 0 < A <-> 0 < (numer ` A ) ) )
Theorem	qgt0numnn 13003	A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( ( A e. QQ /\ 0 < A ) -> (numer ` A ) e. NN )
Theorem	nn0gcdsq 13004	Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
Theorem	zgcdsq 13005	nn0gcdsq 13004 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
Theorem	numdensq 13006	Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( (numer ` ( A ^ 2 ) ) = ( (numer ` A ) ^ 2 ) /\ (denom ` ( A ^ 2 ) ) = ( (denom ` A ) ^ 2 ) ) )
Theorem	numsq 13007	Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> (numer ` ( A ^ 2 ) ) = ( (numer ` A ) ^ 2 ) )
Theorem	densq 13008	Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> (denom ` ( A ^ 2 ) ) = ( (denom ` A ) ^ 2 ) )
Theorem	qden1elz 13009	A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( (denom ` A ) = 1 <-> A e. ZZ ) )
Theorem	nn0sqrtelqelz 13010	If a nonnegative integer has a rational square root, that root must be an integer. (Contributed by Jim Kingdon, 24-May-2022.)
|- ( ( A e. NN0 /\ ( sqr ` A ) e. QQ ) -> ( sqr ` A ) e. ZZ )
Theorem	nonsq 13011	Any integer strictly between two adjacent squares has a non-rational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> -. ( sqr ` A ) e. QQ )
Theorem	nn0sqdcq 13012*	A nonnegative integer is a perfect square or not. This is similar to nn0sqdc 11167 but expresses the idea of being a perfect square as having a rational number which, when squared, gives the original number. (Contributed by Jim Kingdon, 25-Aug-2026.)
|- ( N e. NN0 -> DECID E. q e. QQ N = ( q ^ 2 ) )
Theorem	sqrtrirr 13013*	The square root of a nonnegative integer is either rational or irrational. (Contributed by Jim Kingdon, 24-Aug-2026.)
|- ( A e. NN0 -> ( ( sqr ` A ) e. QQ \/ ( ( sqr ` A ) e. RR /\ A. q e. QQ ( sqr ` A ) # q ) ) )
5.2.5  Euler's theorem
Syntax	codz 13014	Extend class notation with the order function on the class of integers modulo N.
class odZ
Syntax	cphi 13015	Extend class notation with the Euler phi function.
class phi
Definition	df-odz 13016*	Define the order function on the class of integers modulo N. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
Definition	df-phi 13017*	Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than n and coprime to it, see definition in [ApostolNT] p. 25. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
Theorem	phivalfi 13018*	Finiteness of an expression used to define the Euler phi function. (Contributed by Jim Kingon, 28-May-2022.)
|- ( N e. NN -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } e. Fin )
Theorem	phival 13019*	Value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( N e. NN -> ( phi ` N ) = (♯ ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
Theorem	phicl2 13020	Bounds and closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( N e. NN -> ( phi ` N ) e. ( 1 ... N ) )
Theorem	phicl 13021	Closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( N e. NN -> ( phi ` N ) e. NN )
Theorem	phibndlem 13022*	Lemma for phibnd 13023. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) )
Theorem	phibnd 13023	A slightly tighter bound on the value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( N e. ( ZZ>= ` 2 ) -> ( phi ` N ) <_ ( N - 1 ) )
Theorem	phicld 13024	Closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> N e. NN )   =>    |- ( ph -> ( phi ` N ) e. NN )
Theorem	phi1 13025	Value of the Euler phi function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( phi ` 1 ) = 1
Theorem	dfphi2 13026*	Alternate definition of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|- ( N e. NN -> ( phi ` N ) = (♯ ` { x e. ( 0..^ N ) | ( x gcd N ) = 1 } ) )
Theorem	hashdvds 13027*	The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ( ZZ>= ` ( A - 1 ) ) )   &    |- ( ph -> C e. ZZ )   =>    |- ( ph -> (♯ ` { x e. ( A ... B ) | N || ( x - C ) } ) = ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )
Theorem	phiprmpw 13028	Value of the Euler phi function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
|- ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )
Theorem	phiprm 13029	Value of the Euler phi function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
Theorem	crth 13030*	The Chinese Remainder Theorem: the function that maps x to its remainder classes mod M and mod N is 1-1 and onto when M and N are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.)
|- S = ( 0..^ ( M x. N ) )   &    |- T = ( ( 0..^ M ) X. ( 0..^ N ) )   &    |- F = ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. )   &    |- ( ph -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )   =>    |- ( ph -> F : S -1-1-onto-> T )
Theorem	phimullem 13031*	Lemma for phimul 13032. (Contributed by Mario Carneiro, 24-Feb-2014.)
|- S = ( 0..^ ( M x. N ) )   &    |- T = ( ( 0..^ M ) X. ( 0..^ N ) )   &    |- F = ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. )   &    |- ( ph -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )   &    |- U = { y e. ( 0..^ M ) | ( y gcd M ) = 1 }   &    |- V = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- W = { y e. S | ( y gcd ( M x. N ) ) = 1 }   =>    |- ( ph -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) )
Theorem	phimul 13032	The Euler phi function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
|- ( ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) )
Theorem	eulerthlem1 13033*	Lemma for eulerth 13039. (Contributed by Mario Carneiro, 8-May-2015.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- T = ( 1 ... ( phi ` N ) )   &    |- ( ph -> F : T -1-1-onto-> S )   &    |- G = ( x e. T |-> ( ( A x. ( F ` x ) ) mod N ) )   =>    |- ( ph -> G : T --> S )
Theorem	eulerthlemfi 13034*	Lemma for eulerth 13039. The set S is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   =>    |- ( ph -> S e. Fin )
Theorem	eulerthlemrprm 13035*	Lemma for eulerth 13039. N and prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( N gcd prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) ) = 1 )
Theorem	eulerthlema 13036*	Lemma for eulerth 13039. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( ( ( A ^ ( phi ` N ) ) x. prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) ) mod N ) = ( prod_ x e. ( 1 ... ( phi ` N ) ) ( ( A x. ( F ` x ) ) mod N ) mod N ) )
Theorem	eulerthlemh 13037*	Lemma for eulerth 13039. A permutation of ( 1 ... ( phi ` N ) ). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   &    |- H = ( `' F o. ( y e. ( 1 ... ( phi ` N ) ) |-> ( ( A x. ( F ` y ) ) mod N ) ) )   =>    |- ( ph -> H : ( 1 ... ( phi ` N ) ) -1-1-onto-> ( 1 ... ( phi ` N ) ) )
Theorem	eulerthlemth 13038*	Lemma for eulerth 13039. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
Theorem	eulerth 13039	Euler's theorem, a generalization of Fermat's little theorem. If A and N are coprime, then A ^ phi ( N ) == 1 (mod N). This is Metamath 100 proof #10. Also called Euler-Fermat theorem, see theorem 5.17 in [ApostolNT] p. 113. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
Theorem	fermltl 13040	Fermat's little theorem. When P is prime, A ^ P == A (mod P) for any A, see theorem 5.19 in [ApostolNT] p. 114. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
|- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ P ) mod P ) = ( A mod P ) )
Theorem	prmdiv 13041	Show an explicit expression for the modular inverse of A mod P. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- R = ( ( A ^ ( P - 2 ) ) mod P )   =>    |- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( R e. ( 1 ... ( P - 1 ) ) /\ P || ( ( A x. R ) - 1 ) ) )
Theorem	prmdiveq 13042	The modular inverse of A mod P is unique. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- R = ( ( A ^ ( P - 2 ) ) mod P )   =>    |- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( S e. ( 0 ... ( P - 1 ) ) /\ P || ( ( A x. S ) - 1 ) ) <-> S = R ) )
Theorem	prmdivdiv 13043	The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- R = ( ( A ^ ( P - 2 ) ) mod P )   =>    |- ( ( P e. Prime /\ A e. ( 1 ... ( P - 1 ) ) ) -> A = ( ( R ^ ( P - 2 ) ) mod P ) )
Theorem	hashgcdlem 13044*	A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- A = { y e. ( 0..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }   &    |- B = { z e. ( 0..^ M ) | ( z gcd M ) = N }   &    |- F = ( x e. A |-> ( x x. N ) )   =>    |- ( ( M e. NN /\ N e. NN /\ N || M ) -> F : A -1-1-onto-> B )
Theorem	dvdsfi 13045*	A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)
|- ( N e. NN -> { x e. NN | x || N } e. Fin )
Theorem	hashgcdeq 13046*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( M e. NN /\ N e. NN ) -> (♯ ` { x e. ( 0..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) )
Theorem	phisum 13047*	The divisor sum identity of the totient function. Theorem 2.2 in [ApostolNT] p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )
Theorem	odzval 13048*	Value of the order function. This is a function of functions; the inner argument selects the base (i.e., mod N for some N, often prime) and the outer argument selects the integer or equivalence class (if you want to think about it that way) from the integers mod N. In order to ensure the supremum is well-defined, we only define the expression when A and N are coprime. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
Theorem	odzcllem 13049	- Lemma for odzcl 13050, showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( odZ ` N ) ` A ) e. NN /\ N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )
Theorem	odzcl 13050	The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) e. NN )
Theorem	odzid 13051	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 13052	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 13053	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 13054	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 13055	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 13056	Show an explicit expression for the modular inverse of A mod P. This is an application of prmdiv 13041. (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 13057	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 13058	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 13059	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 13060*	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 13061*	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 13062*	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 13063*	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 13064	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 13065	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 13066	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 13067	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 13068	A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.)
|- ( N e. ( Prime \ { 2 } ) -> -. 2 || N )
Theorem	nnoddn2prmb 13069	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 13070	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 13071	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 13072*	Lemma for pythagtrip 13090. 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 13073*	Lemma for pythagtrip 13090. 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 13074	Lemma for pythagtrip 13090. 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 13075	Lemma for pythagtrip 13090. 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 13076	Lemma for pythagtrip 13090. 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 13077	Lemma for pythagtrip 13090. 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 13078	Lemma for pythagtrip 13090. 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 13079	Lemma for pythagtrip 13090. 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 13080	Lemma for pythagtrip 13090. 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 13081	Lemma for pythagtrip 13090. 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 13082	Lemma for pythagtrip 13090. 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 13083	Lemma for pythagtrip 13090. 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 13084	Lemma for pythagtrip 13090. 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 13085	Lemma for pythagtrip 13090. 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 13086	Lemma for pythagtrip 13090. 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 13087	Lemma for pythagtrip 13090. 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 13088*	Lemma for pythagtrip 13090. 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 13089*	Lemma for pythagtrip 13090. 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 13090*	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 13091	Extend class notation with the prime count function.
class pCnt
Definition	df-pc 13092*	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 13093*	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 13094*	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 13095*	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 13096*	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 13097*	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 13098*	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 13099*	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 13100*	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 )