P. 128 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prmdvdsfz 12701*	Each integer greater than 1 and less then or equal to a fixed number is divisible by a prime less then or equal to this fixed number. (Contributed by AV, 15-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I ) )
Theorem	nprmdvds1 12702	No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.)
|- ( P e. Prime -> -. P || 1 )
Theorem	isprm5lem 12703*	Lemma for isprm5 12704. The interesting direction (showing that one only needs to check prime divisors up to the square root of P). (Contributed by Jim Kingdon, 20-Oct-2024.)
|- ( ph -> P e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) )   &    |- ( ph -> X e. ( 2 ... ( P - 1 ) ) )   =>    |- ( ph -> -. X || P )
Theorem	isprm5 12704*	One need only check prime divisors of P up to sqr P in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) ) )
Theorem	divgcdodd 12705	Either A / ( A gcd B ) is odd or B / ( A gcd B ) is odd. (Contributed by Scott Fenton, 19-Apr-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
5.2.2  Coprimality and Euclid's lemma (cont.) This section is about coprimality with respect to primes, and a special version of Euclid's lemma for primes is provided, see euclemma 12708.
Theorem	coprm 12706	A prime number either divides an integer or is coprime to it, but not both. Theorem 1.8 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N <-> ( P gcd N ) = 1 ) )
Theorem	prmrp 12707	Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
Theorem	euclemma 12708	Euclid's lemma. A prime number divides the product of two integers iff it divides at least one of them. Theorem 1.9 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( P || ( M x. N ) <-> ( P || M \/ P || N ) ) )
Theorem	isprm6 12709*	A number is prime iff it satisfies Euclid's lemma euclemma 12708. (Contributed by Mario Carneiro, 6-Sep-2015.)
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) )
Theorem	prmdvdsexp 12710	A prime divides a positive power of an integer iff it divides the integer. (Contributed by Mario Carneiro, 24-Feb-2014.) (Revised by Mario Carneiro, 17-Jul-2014.)
|- ( ( P e. Prime /\ A e. ZZ /\ N e. NN ) -> ( P || ( A ^ N ) <-> P || A ) )
Theorem	prmdvdsexpb 12711	A prime divides a positive power of another iff they are equal. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 24-Feb-2014.)
|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P = Q ) )
Theorem	prmdvdsexpr 12712	If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN0 ) -> ( P || ( Q ^ N ) -> P = Q ) )
Theorem	prmexpb 12713	Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.)
|- ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) ) -> ( ( P ^ M ) = ( Q ^ N ) <-> ( P = Q /\ M = N ) ) )
Theorem	prmfac1 12714	The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.)
|- ( ( N e. NN0 /\ P e. Prime /\ P || ( ! ` N ) ) -> P <_ N )
Theorem	rpexp 12715	If two numbers A and B are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A ^ N ) gcd B ) = 1 <-> ( A gcd B ) = 1 ) )
Theorem	rpexp1i 12716	Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ M e. NN0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd B ) = 1 ) )
Theorem	rpexp12i 12717	Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( A gcd B ) = 1 -> ( ( A ^ M ) gcd ( B ^ N ) ) = 1 ) )
Theorem	prmndvdsfaclt 12718	A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021.)
|- ( ( P e. Prime /\ N e. NN0 ) -> ( N < P -> -. P || ( ! ` N ) ) )
Theorem	cncongrprm 12719	Corollary 2 of Cancellability of Congruences: Two products with a common factor are congruent modulo a prime number not dividing the common factor iff the other factors are congruent modulo the prime number. (Contributed by AV, 13-Jul-2021.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. Prime /\ -. P || C ) ) -> ( ( ( A x. C ) mod P ) = ( ( B x. C ) mod P ) <-> ( A mod P ) = ( B mod P ) ) )
Theorem	isevengcd2 12720	The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.)
|- ( Z e. ZZ -> ( 2 || Z <-> ( 2 gcd Z ) = 2 ) )
Theorem	isoddgcd1 12721	The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.)
|- ( Z e. ZZ -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )
Theorem	3lcm2e6 12722	The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 27-Aug-2020.)
|- ( 3 lcm 2 ) = 6
5.2.3  Non-rationality of square root of 2
Theorem	sqrt2irrlem 12723	Lemma for sqrt2irr 12724. This is the core of the proof: - if A / B = sqr ( 2 ), then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( sqr ` 2 ) = ( A / B ) )   =>    |- ( ph -> ( ( A / 2 ) e. ZZ /\ ( B / 2 ) e. NN ) )
Theorem	sqrt2irr 12724	The square root of 2 is not rational. That is, for any rational number, ( sqr ` 2 ) does not equal it. However, if we were to say "the square root of 2 is irrational" that would mean something stronger: "for any rational number, ( sqr ` 2 ) is apart from it" (the two statements are equivalent given excluded middle). See sqrt2irrap 12742 for the proof that the square root of two is irrational. The proof's core is proven in sqrt2irrlem 12723, which shows that if A / B = sqr ( 2 ), then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- ( sqr ` 2 ) e/ QQ
Theorem	sqrt2re 12725	The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)
|- ( sqr ` 2 ) e. RR
Theorem	sqrt2irr0 12726	The square root of 2 is not rational. (Contributed by AV, 23-Dec-2022.)
|- ( sqr ` 2 ) e. ( RR \ QQ )
Theorem	pw2dvdslemn 12727*	Lemma for pw2dvds 12728. If a natural number has some power of two which does not divide it, there is a highest power of two which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.)
|- ( ( N e. NN /\ A e. NN /\ -. ( 2 ^ A ) || N ) -> E. m e. NN0 ( ( 2 ^ m ) || N /\ -. ( 2 ^ ( m + 1 ) ) || N ) )
Theorem	pw2dvds 12728*	A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.)
|- ( N e. NN -> E. m e. NN0 ( ( 2 ^ m ) || N /\ -. ( 2 ^ ( m + 1 ) ) || N ) )
Theorem	pw2dvdseulemle 12729	Lemma for pw2dvdseu 12730. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> ( 2 ^ A ) || N )   &    |- ( ph -> -. ( 2 ^ ( B + 1 ) ) || N )   =>    |- ( ph -> A <_ B )
Theorem	pw2dvdseu 12730*	A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.)
|- ( N e. NN -> E! m e. NN0 ( ( 2 ^ m ) || N /\ -. ( 2 ^ ( m + 1 ) ) || N ) )
Theorem	oddpwdclemxy 12731*	Lemma for oddpwdc 12736. Another way of stating that decomposing a natural number into a power of two and an odd number is unique. (Contributed by Jim Kingdon, 16-Nov-2021.)
|- ( ( ( ( X e. NN /\ -. 2 || X ) /\ Y e. NN0 ) /\ A = ( ( 2 ^ Y ) x. X ) ) -> ( X = ( A / ( 2 ^ ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) ) ) /\ Y = ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) ) )
Theorem	oddpwdclemdvds 12732*	Lemma for oddpwdc 12736. A natural number is divisible by the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.)
|- ( A e. NN -> ( 2 ^ ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) ) || A )
Theorem	oddpwdclemndvds 12733*	Lemma for oddpwdc 12736. A natural number is not divisible by one more than the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.)
|- ( A e. NN -> -. ( 2 ^ ( ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) + 1 ) ) || A )
Theorem	oddpwdclemodd 12734*	Lemma for oddpwdc 12736. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.)
|- ( A e. NN -> -. 2 || ( A / ( 2 ^ ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) ) ) )
Theorem	oddpwdclemdc 12735*	Lemma for oddpwdc 12736. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.)
|- ( ( ( ( X e. NN /\ -. 2 || X ) /\ Y e. NN0 ) /\ A = ( ( 2 ^ Y ) x. X ) ) <-> ( A e. NN /\ ( X = ( A / ( 2 ^ ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) ) ) /\ Y = ( iota_ z e. NN0 ( ( 2 ^ z ) || A /\ -. ( 2 ^ ( z + 1 ) ) || A ) ) ) ) )
Theorem	oddpwdc 12736*	The function F that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)
|- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   =>    |- F : ( J X. NN0 ) -1-1-onto-> NN
Theorem	sqpweven 12737*	The greatest power of two dividing the square of an integer is an even power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)
|- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   =>    |- ( A e. NN -> 2 || ( 2nd ` ( `' F ` ( A ^ 2 ) ) ) )
Theorem	2sqpwodd 12738*	The greatest power of two dividing twice the square of an integer is an odd power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)
|- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   =>    |- ( A e. NN -> -. 2 || ( 2nd ` ( `' F ` ( 2 x. ( A ^ 2 ) ) ) ) )
Theorem	sqne2sq 12739	The square of a natural number can never be equal to two times the square of a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.)
|- ( ( A e. NN /\ B e. NN ) -> ( A ^ 2 ) =/= ( 2 x. ( B ^ 2 ) ) )
Theorem	znege1 12740	The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.)
|- ( ( A e. ZZ /\ B e. ZZ /\ A =/= B ) -> 1 <_ ( abs ` ( A - B ) ) )
Theorem	sqrt2irraplemnn 12741	Lemma for sqrt2irrap 12742. The square root of 2 is apart from a positive rational expressed as a numerator and denominator. (Contributed by Jim Kingdon, 2-Oct-2021.)
|- ( ( A e. NN /\ B e. NN ) -> ( sqr ` 2 ) # ( A / B ) )
Theorem	sqrt2irrap 12742	The square root of 2 is irrational. That is, for any rational number, ( sqr ` 2 ) is apart from it. In the absence of excluded middle, we can distinguish between this and "the square root of 2 is not rational" which is sqrt2irr 12724. (Contributed by Jim Kingdon, 2-Oct-2021.)
|- ( Q e. QQ -> ( sqr ` 2 ) # Q )
5.2.4  Properties of the canonical representation of a rational
Syntax	cnumer 12743	Extend class notation to include canonical numerator function.
class numer
Syntax	cdenom 12744	Extend class notation to include canonical denominator function.
class denom
Definition	df-numer 12745*	The canonical numerator of a rational is the numerator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
Definition	df-denom 12746*	The canonical denominator of a rational is the denominator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
Theorem	qnumval 12747*	Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> (numer ` A ) = ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
Theorem	qdenval 12748*	Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> (denom ` A ) = ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
Theorem	qnumdencl 12749	Lemma for qnumcl 12750 and qdencl 12751. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> ( (numer ` A ) e. ZZ /\ (denom ` A ) e. NN ) )
Theorem	qnumcl 12750	The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> (numer ` A ) e. ZZ )
Theorem	qdencl 12751	The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> (denom ` A ) e. NN )
Theorem	fnum 12752	Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- numer : QQ --> ZZ
Theorem	fden 12753	Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- denom : QQ --> NN
Theorem	qnumdenbi 12754	Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( B gcd C ) = 1 /\ A = ( B / C ) ) <-> ( (numer ` A ) = B /\ (denom ` A ) = C ) ) )
Theorem	qnumdencoprm 12755	The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> ( (numer ` A ) gcd (denom ` A ) ) = 1 )
Theorem	qeqnumdivden 12756	Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> A = ( (numer ` A ) / (denom ` A ) ) )
Theorem	qmuldeneqnum 12757	Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> ( A x. (denom ` A ) ) = (numer ` A ) )
Theorem	divnumden 12758	Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( (numer ` ( A / B ) ) = ( A / ( A gcd B ) ) /\ (denom ` ( A / B ) ) = ( B / ( A gcd B ) ) ) )
Theorem	divdenle 12759	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 12760	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 12761	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 12762	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 12763	nn0gcdsq 12762 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 12764	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 12765	Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> (numer ` ( A ^ 2 ) ) = ( (numer ` A ) ^ 2 ) )
Theorem	densq 12766	Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> (denom ` ( A ^ 2 ) ) = ( (denom ` A ) ^ 2 ) )
Theorem	qden1elz 12767	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 12768	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 12769	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 )
5.2.5  Euler's theorem
Syntax	codz 12770	Extend class notation with the order function on the class of integers modulo N.
class odZ
Syntax	cphi 12771	Extend class notation with the Euler phi function.
class phi
Definition	df-odz 12772*	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 12773*	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 12774*	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 12775*	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 12776	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 12777	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 12778*	Lemma for phibnd 12779. (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 12779	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 12780	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 12781	Value of the Euler phi function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( phi ` 1 ) = 1
Theorem	dfphi2 12782*	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 12783*	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 12784	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 12785	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 12786*	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 12787*	Lemma for phimul 12788. (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 12788	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 12789*	Lemma for eulerth 12795. (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 12790*	Lemma for eulerth 12795. 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 12791*	Lemma for eulerth 12795. 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 12792*	Lemma for eulerth 12795. (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 12793*	Lemma for eulerth 12795. 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 12794*	Lemma for eulerth 12795. 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 12795	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 12796	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 12797	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 12798	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 12799	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 12800*	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 )