P. 123 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12201-12300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pw2dvds 12201*	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 12202	Lemma for pw2dvdseu 12203. 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 12203*	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 12204*	Lemma for oddpwdc 12209. 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 12205*	Lemma for oddpwdc 12209. 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 12206*	Lemma for oddpwdc 12209. 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 12207*	Lemma for oddpwdc 12209. 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 12208*	Lemma for oddpwdc 12209. 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 12209*	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 12210*	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 12211*	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 12212	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 12213	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 12214	Lemma for sqrt2irrap 12215. 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 12215	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 12197. (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 12216	Extend class notation to include canonical numerator function.
class numer
Syntax	cdenom 12217	Extend class notation to include canonical denominator function.
class denom
Definition	df-numer 12218*	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 12219*	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 12220*	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 12221*	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 12222	Lemma for qnumcl 12223 and qdencl 12224. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> ( (numer ` A ) e. ZZ /\ (denom ` A ) e. NN ) )
Theorem	qnumcl 12223	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 12224	The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( A e. QQ -> (denom ` A ) e. NN )
Theorem	fnum 12225	Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- numer : QQ --> ZZ
Theorem	fden 12226	Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- denom : QQ --> NN
Theorem	qnumdenbi 12227	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 12228	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 12229	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 12230	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 12231	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 12232	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 12233	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 12234	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 12235	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 12236	nn0gcdsq 12235 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 12237	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 12238	Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> (numer ` ( A ^ 2 ) ) = ( (numer ` A ) ^ 2 ) )
Theorem	densq 12239	Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> (denom ` ( A ^ 2 ) ) = ( (denom ` A ) ^ 2 ) )
Theorem	qden1elz 12240	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 12241	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 12242	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 12243	Extend class notation with the order function on the class of integers modulo N.
class odZ
Syntax	cphi 12244	Extend class notation with the Euler phi function.
class phi
Definition	df-odz 12245*	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 12246*	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 12247*	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 12248*	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 12249	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 12250	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 12251*	Lemma for phibnd 12252. (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 12252	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 12253	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 12254	Value of the Euler phi function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( phi ` 1 ) = 1
Theorem	dfphi2 12255*	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 12256*	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 12257	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 12258	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 12259*	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 12260*	Lemma for phimul 12261. (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 12261	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 12262*	Lemma for eulerth 12268. (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 12263*	Lemma for eulerth 12268. 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 12264*	Lemma for eulerth 12268. 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 12265*	Lemma for eulerth 12268. (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 12266*	Lemma for eulerth 12268. 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 12267*	Lemma for eulerth 12268. 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 12268	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 12269	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 12270	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 12271	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 12272	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 12273*	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	hashgcdeq 12274*	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 12275*	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 12276*	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 12277	- Lemma for odzcl 12278, 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 12278	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 12279	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 12280	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 12281	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 12282	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 12283	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 12284	Show an explicit expression for the modular inverse of A mod P. This is an application of prmdiv 12270. (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 12285	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 12286	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 12287	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 12288*	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 12289*	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 12290*	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 12291*	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 12292	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 12293	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 12294	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 12295	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 12296	A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.)
|- ( N e. ( Prime \ { 2 } ) -> -. 2 || N )
Theorem	nnoddn2prmb 12297	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 12298	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 12299	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 12300*	Lemma for pythagtrip 12318. 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 ) )