P. 158 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rplogb1 15701	The logarithm of 1 to an arbitrary base B is 0. Property 1(b) of [Cohen4] p. 361. See log1 15619. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. RR+ /\ B # 1 ) -> ( B logb 1 ) = 0 )
Theorem	rpelogb 15702	The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using _e as the base in logb is the same as log. Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.)
|- ( A e. RR+ -> ( _e logb A ) = ( log ` A ) )
Theorem	rplogbchbase 15703	Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.)
|- ( ( ( A e. RR+ /\ A # 1 ) /\ ( B e. RR+ /\ B # 1 ) /\ X e. RR+ ) -> ( A logb X ) = ( ( B logb X ) / ( B logb A ) ) )
Theorem	relogbval 15704	Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
Theorem	relogbzcl 15705	Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) e. RR )
Theorem	rplogbreexp 15706	Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ C e. RR+ /\ E e. RR ) -> ( B logb ( C ^c E ) ) = ( E x. ( B logb C ) ) )
Theorem	rplogbzexp 15707	Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) )
Theorem	rprelogbmul 15708	The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A x. C ) ) = ( ( B logb A ) + ( B logb C ) ) )
Theorem	rprelogbmulexp 15709	The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ ( A e. RR+ /\ C e. RR+ /\ E e. RR ) ) -> ( B logb ( A x. ( C ^c E ) ) ) = ( ( B logb A ) + ( E x. ( B logb C ) ) ) )
Theorem	rprelogbdiv 15710	The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A / C ) ) = ( ( B logb A ) - ( B logb C ) ) )
Theorem	relogbexpap 15711	Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
|- ( ( B e. RR+ /\ B # 1 /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )
Theorem	nnlogbexp 15712	Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )
Theorem	logbrec 15713	Logarithm of a reciprocal changes sign. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ A e. RR+ ) -> ( B logb ( 1 / A ) ) = -u ( B logb A ) )
Theorem	logbleb 15714	The general logarithm function is monotone/increasing. See logleb 15628. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( B logb X ) <_ ( B logb Y ) ) )
Theorem	logblt 15715	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 15627. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X < Y <-> ( B logb X ) < ( B logb Y ) ) )
Theorem	rplogbcxp 15716	Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.)
|- ( ( B e. RR+ /\ B # 1 /\ X e. RR ) -> ( B logb ( B ^c X ) ) = X )
Theorem	rpcxplogb 15717	Identity law for the general logarithm. (Contributed by AV, 22-May-2020.)
|- ( ( B e. RR+ /\ B # 1 /\ X e. RR+ ) -> ( B ^c ( B logb X ) ) = X )
Theorem	relogbcxpbap 15718	The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( ( B logb X ) = Y <-> ( B ^c Y ) = X ) )
Theorem	logbgt0b 15719	The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.)
|- ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( B logb A ) <-> 1 < A ) )
Theorem	logbgcd1irr 15720	The logarithm of an integer greater than 1 to an integer base greater than 1 is not rational if the argument and the base are relatively prime. For example, ( 2 logb 9 ) e. ( RR \ QQ ). (Contributed by AV, 29-Dec-2022.)
|- ( ( X e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) /\ ( X gcd B ) = 1 ) -> ( B logb X ) e. ( RR \ QQ ) )
Theorem	logbgcd1irraplemexp 15721	Lemma for logbgcd1irrap 15723. Apartness of X ^ N and B ^ M. (Contributed by Jim Kingdon, 11-Jul-2024.)
|- ( ph -> X e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. ( ZZ>= ` 2 ) )   &    |- ( ph -> ( X gcd B ) = 1 )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( X ^ N ) # ( B ^ M ) )
Theorem	logbgcd1irraplemap 15722	Lemma for logbgcd1irrap 15723. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.)
|- ( ph -> X e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. ( ZZ>= ` 2 ) )   &    |- ( ph -> ( X gcd B ) = 1 )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( B logb X ) # ( M / N ) )
Theorem	logbgcd1irrap 15723	The logarithm of an integer greater than 1 to an integer base greater than 1 is irrational (in the sense of being apart from any rational number) if the argument and the base are relatively prime. For example, ( 2 logb 9 ) # Q where Q is rational. (Contributed by AV, 29-Dec-2022.)
|- ( ( ( X e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) /\ ( ( X gcd B ) = 1 /\ Q e. QQ ) ) -> ( B logb X ) # Q )
Theorem	2logb9irr 15724	Example for logbgcd1irr 15720. The logarithm of nine to base two is not rational. Also see 2logb9irrap 15730 which says that it is irrational (in the sense of being apart from any rational number). (Contributed by AV, 29-Dec-2022.)
|- ( 2 logb 9 ) e. ( RR \ QQ )
Theorem	logbprmirr 15725	The logarithm of a prime to a different prime base is not rational. For example, ( 2 logb 3 ) e. ( RR \ QQ ) (see 2logb3irr 15726). (Contributed by AV, 31-Dec-2022.)
|- ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> ( B logb X ) e. ( RR \ QQ ) )
Theorem	2logb3irr 15726	Example for logbprmirr 15725. The logarithm of three to base two is not rational. (Contributed by AV, 31-Dec-2022.)
|- ( 2 logb 3 ) e. ( RR \ QQ )
Theorem	2logb9irrALT 15727	Alternate proof of 2logb9irr 15724: The logarithm of nine to base two is not rational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( 2 logb 9 ) e. ( RR \ QQ )
Theorem	sqrt2cxp2logb9e3 15728	The square root of two to the power of the logarithm of nine to base two is three. ( sqr ` 2 ) and ( 2 logb 9 ) are not rational (see sqrt2irr0 12759 resp. 2logb9irr 15724), satisfying the statement in 2irrexpq 15729. (Contributed by AV, 29-Dec-2022.)
|- ( ( sqr ` 2 ) ^c ( 2 logb 9 ) ) = 3
Theorem	2irrexpq 15729*	There exist real numbers a and b which are not rational such that ( a ^ b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named non-rational numbers ( sqr ` 2 ) and ( 2 logb 9 ), see sqrt2irr0 12759, 2logb9irr 15724 and sqrt2cxp2logb9e3 15728. Therefore, this proof is acceptable/usable in intuitionistic logic. For a theorem which is the same but proves that a and b are irrational (in the sense of being apart from any rational number), see 2irrexpqap 15731. (Contributed by AV, 23-Dec-2022.)
|- E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ
Theorem	2logb9irrap 15730	Example for logbgcd1irrap 15723. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.)
|- ( Q e. QQ -> ( 2 logb 9 ) # Q )
Theorem	2irrexpqap 15731*	There exist real numbers a and b which are irrational (in the sense of being apart from any rational number) such that ( a ^ b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers ( sqr ` 2 ) and ( 2 logb 9 ), see sqrt2irrap 12775, 2logb9irrap 15730 and sqrt2cxp2logb9e3 15728. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.)
|- E. a e. RR E. b e. RR ( A. p e. QQ a # p /\ A. q e. QQ b # q /\ ( a ^c b ) e. QQ )
11.2.5  Quartic binomial expansion
Theorem	binom4 15732	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 12068, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 4 ) = ( ( ( A ^ 4 ) + ( 4 x. ( ( A ^ 3 ) x. B ) ) ) + ( ( 6 x. ( ( A ^ 2 ) x. ( B ^ 2 ) ) ) + ( ( 4 x. ( A x. ( B ^ 3 ) ) ) + ( B ^ 4 ) ) ) ) )
11.3  Basic number theory
11.3.1  Wilson's theorem
Theorem	wilthlem1 15733	The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ZZ / P ZZ are 1 and -u 1 == P - 1. (Note that from prmdiveq 12831, ( N ^ ( P - 2 ) ) mod P is the modular inverse of N in ZZ / P ZZ. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N = ( ( N ^ ( P - 2 ) ) mod P ) <-> ( N = 1 \/ N = ( P - 1 ) ) ) )
11.3.2  Number-theoretical functions
Syntax	csgm 15734	Extend class notation with the divisor function.
class sigma
Definition	df-sgm 15735*	Define the sum of positive divisors function ( x sigma n ), which is the sum of the xth powers of the positive integer divisors of n, see definition in [ApostolNT] p. 38. For x = 0, ( x sigma n ) counts the number of divisors of n, i.e. ( 0 sigma n ) is the divisor function, see remark in [ApostolNT] p. 38. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
Theorem	sgmval 15736*	The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^c A ) )
Theorem	sgmval2 15737*	The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )
Theorem	0sgm 15738*	The value of the sum-of-divisors function, usually denoted σ<SUB>0</SUB>(<i>n</i>). (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( A e. NN -> ( 0 sigma A ) = (♯ ` { p e. NN | p || A } ) )
Theorem	sgmf 15739	The divisor function is a function into the complex numbers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
|- sigma : ( CC X. NN ) --> CC
Theorem	sgmcl 15740	Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) e. CC )
Theorem	sgmnncl 15741	Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. NN0 /\ B e. NN ) -> ( A sigma B ) e. NN )
Theorem	dvdsppwf1o 15742*	A bijection between the divisors of a prime power and the integers less than or equal to the exponent. (Contributed by Mario Carneiro, 5-May-2016.)
|- F = ( n e. ( 0 ... A ) |-> ( P ^ n ) )   =>    |- ( ( P e. Prime /\ A e. NN0 ) -> F : ( 0 ... A ) -1-1-onto-> { x e. NN | x || ( P ^ A ) } )
Theorem	mpodvdsmulf1o 15743*	If M and N are two coprime integers, multiplication forms a bijection from the set of pairs <. j , k >. where j || M and k || N, to the set of divisors of M x. N. (Contributed by GG, 18-Apr-2025.)
|- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- X = { x e. NN | x || M }   &    |- Y = { x e. NN | x || N }   &    |- Z = { x e. NN | x || ( M x. N ) }   =>    |- ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )
Theorem	fsumdvdsmul 15744*	Product of two divisor sums. (This is also the main part of the proof that " sum_ k || N F ( k ) is a multiplicative function if F is".) (Contributed by Mario Carneiro, 2-Jul-2015.) Avoid ax-mulf 8160. (Revised by GG, 18-Apr-2025.)
|- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- X = { x e. NN | x || M }   &    |- Y = { x e. NN | x || N }   &    |- Z = { x e. NN | x || ( M x. N ) }   &    |- ( ( ph /\ j e. X ) -> A e. CC )   &    |- ( ( ph /\ k e. Y ) -> B e. CC )   &    |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) = D )   &    |- ( i = ( j x. k ) -> C = D )   =>    |- ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ i e. Z C )
Theorem	sgmppw 15745*	The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( A sigma ( P ^ N ) ) = sum_ k e. ( 0 ... N ) ( ( P ^c A ) ^ k ) )
Theorem	0sgmppw 15746	A prime power P ^ K has K + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( P e. Prime /\ K e. NN0 ) -> ( 0 sigma ( P ^ K ) ) = ( K + 1 ) )
Theorem	1sgmprm 15747	The sum of divisors for a prime is P + 1 because the only divisors are 1 and P. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( P e. Prime -> ( 1 sigma P ) = ( P + 1 ) )
Theorem	1sgm2ppw 15748	The sum of the divisors of 2 ^ ( N - 1 ). (Contributed by Mario Carneiro, 17-May-2016.)
|- ( N e. NN -> ( 1 sigma ( 2 ^ ( N - 1 ) ) ) = ( ( 2 ^ N ) - 1 ) )
Theorem	sgmmul 15749	The divisor function for fixed parameter A is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.)
|- ( ( A e. CC /\ ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) ) -> ( A sigma ( M x. N ) ) = ( ( A sigma M ) x. ( A sigma N ) ) )
11.3.3  Perfect Number Theorem
Theorem	mersenne 15750	A Mersenne prime is a prime number of the form 2 ^ P - 1. This theorem shows that the P in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> P e. Prime )
Theorem	perfect1 15751	Euclid's contribution to the Euclid-Euler theorem. A number of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ) is a perfect number. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ ( P - 1 ) ) x. ( ( 2 ^ P ) - 1 ) ) ) = ( ( 2 ^ P ) x. ( ( 2 ^ P ) - 1 ) ) )
Theorem	perfectlem1 15752	Lemma for perfect 15754. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> -. 2 || B )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
Theorem	perfectlem2 15753	Lemma for perfect 15754. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by Wolf Lammen, 17-Sep-2020.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> -. 2 || B )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
Theorem	perfect 15754*	The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer N is a perfect number (that is, its divisor sum is 2 N) if and only if it is of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ), where 2 ^ p - 1 is prime (a Mersenne prime), and therefore p is also prime, see mersenne 15750. This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( N e. NN /\ 2 || N ) -> ( ( 1 sigma N ) = ( 2 x. N ) <-> E. p e. ZZ ( ( ( 2 ^ p ) - 1 ) e. Prime /\ N = ( ( 2 ^ ( p - 1 ) ) x. ( ( 2 ^ p ) - 1 ) ) ) ) )
11.3.4  Quadratic residues and the Legendre symbol If the congruence ( ( x ^ 2 ) mod p ) = ( n mod p ) has a solution we say that n is a quadratic residue mod p. If the congruence has no solution we say that n is a quadratic nonresidue mod p, see definition in [ApostolNT] p. 178. The Legendre symbol ( n /L p ) is defined in a way that its value is 1 if n is a quadratic residue mod p and -u 1 if n is a quadratic nonresidue mod p (and 0 if p divides n). Originally, the Legendre symbol ( N /L P ) was defined for odd primes P only (and arbitrary integers N) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 15756 for the "Legendre symbol" /L is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol".
Syntax	clgs 15755	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 15756*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- /L = ( a e. ZZ , n e. ZZ |-> if ( n = 0 , if ( ( a ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) ) ) )
Theorem	zabsle1 15757	{ -u 1 , 0 , 1 } is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.)
|- ( Z e. ZZ -> ( Z e. { -u 1 , 0 , 1 } <-> ( abs ` Z ) <_ 1 ) )
Theorem	lgslem1 15758	When a is coprime to the prime p, a ^ ( ( p - 1 ) / 2 ) is equivalent mod p to 1 or -u 1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } )
Theorem	lgslem2 15759	The set Z of all integers with absolute value at most 1 contains { -u 1 , 0 , 1 }. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( -u 1 e. Z /\ 0 e. Z /\ 1 e. Z )
Theorem	lgslem3 15760*	The set Z of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. Z /\ B e. Z ) -> ( A x. B ) e. Z )
Theorem	lgslem4 15761*	Lemma for lgsfcl2 15764. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
Theorem	lgsval 15762*	Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) = if ( N = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) ) )
Theorem	lgsfvalg 15763*	Value of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. NN /\ M e. NN ) -> ( F ` M ) = if ( M e. Prime , ( if ( M = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( M - 1 ) / 2 ) ) + 1 ) mod M ) - 1 ) ) ^ ( M pCnt N ) ) , 1 ) )
Theorem	lgsfcl2 15764*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 }, see zabsle1 15757). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   &    |- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> Z )
Theorem	lgscllem 15765*	The Legendre symbol is an element of Z. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   &    |- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z )
Theorem	lgsfcl 15766*	Closure of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> ZZ )
Theorem	lgsfle1 15767*	The function F has magnitude less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M e. NN ) -> ( abs ` ( F ` M ) ) <_ 1 )
Theorem	lgsval2lem 15768*	Lemma for lgsval2 15774. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. Prime ) -> ( A /L N ) = if ( N = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( N - 1 ) / 2 ) ) + 1 ) mod N ) - 1 ) ) )
Theorem	lgsval4lem 15769*	Lemma for lgsval4 15778. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) )
Theorem	lgscl2 15770*	The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z )
Theorem	lgs0 15771	The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( A e. ZZ -> ( A /L 0 ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )
Theorem	lgscl 15772	The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
Theorem	lgsle1 15773	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 15772 this implies that it takes values in { -u 1 , 0 , 1 }. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) <_ 1 )
Theorem	lgsval2 15774	The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ P e. Prime ) -> ( A /L P ) = if ( P = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) ) )
Theorem	lgs2 15775	The Legendre symbol at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( A e. ZZ -> ( A /L 2 ) = if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) )
Theorem	lgsval3 15776	The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( A /L P ) = ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) )
Theorem	lgsvalmod 15777	The Legendre symbol is equivalent to a ^ ( ( p - 1 ) / 2 ), mod p. This theorem is also called "Euler's criterion", see theorem 9.2 in [ApostolNT] p. 180, or a representation of Euler's criterion using the Legendre symbol. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) mod P ) = ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) )
Theorem	lgsval4 15778*	Restate lgsval 15762 for nonzero N, where the function F has been abbreviated into a self-referential expression taking the value of /L on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L N ) = ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) )
Theorem	lgsfcl3 15779*	Closure of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> ZZ )
Theorem	lgsval4a 15780*	Same as lgsval4 15778 for positive N. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. NN ) -> ( A /L N ) = ( seq 1 ( x. , F ) ` N ) )
Theorem	lgscl1 15781	The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. { -u 1 , 0 , 1 } )
Theorem	lgsneg 15782	The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) )
Theorem	lgsneg1 15783	The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. NN0 /\ N e. ZZ ) -> ( A /L -u N ) = ( A /L N ) )
Theorem	lgsmod 15784	The Legendre (Jacobi) symbol is preserved under reduction mod n when n is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( A mod N ) /L N ) = ( A /L N ) )
Theorem	lgsdilem 15785	Lemma for lgsdi 15795 and lgsdir 15793: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ N e. ZZ ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> if ( ( N < 0 /\ ( A x. B ) < 0 ) , -u 1 , 1 ) = ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. if ( ( N < 0 /\ B < 0 ) , -u 1 , 1 ) ) )
Theorem	lgsdir2lem1 15786	Lemma for lgsdir2 15791. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( ( 1 mod 8 ) = 1 /\ ( -u 1 mod 8 ) = 7 ) /\ ( ( 3 mod 8 ) = 3 /\ ( -u 3 mod 8 ) = 5 ) )
Theorem	lgsdir2lem2 15787	Lemma for lgsdir2 15791. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( K e. ZZ /\ 2 || ( K + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... K ) -> ( A mod 8 ) e. S ) ) )   &    |- M = ( K + 1 )   &    |- N = ( M + 1 )   &    |- N e. S   =>    |- ( N e. ZZ /\ 2 || ( N + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... N ) -> ( A mod 8 ) e. S ) ) )
Theorem	lgsdir2lem3 15788	Lemma for lgsdir2 15791. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
Theorem	lgsdir2lem4 15789	Lemma for lgsdir2 15791. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) e. { 1 , 7 } ) -> ( ( ( A x. B ) mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
Theorem	lgsdir2lem5 15790	Lemma for lgsdir2 15791. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( ( A mod 8 ) e. { 3 , 5 } /\ ( B mod 8 ) e. { 3 , 5 } ) ) -> ( ( A x. B ) mod 8 ) e. { 1 , 7 } )
Theorem	lgsdir2 15791	The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A x. B ) /L 2 ) = ( ( A /L 2 ) x. ( B /L 2 ) ) )
Theorem	lgsdirprm 15792	The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.)
|- ( ( A e. ZZ /\ B e. ZZ /\ P e. Prime ) -> ( ( A x. B ) /L P ) = ( ( A /L P ) x. ( B /L P ) ) )
Theorem	lgsdir 15793	The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that A and B are odd positive integers). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ N e. ZZ ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
Theorem	lgsdilem2 15794*	Lemma for lgsdi 15795. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> N =/= 0 )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) )   =>    |- ( ph -> ( seq 1 ( x. , F ) ` ( abs ` M ) ) = ( seq 1 ( x. , F ) ` ( abs ` ( M x. N ) ) ) )
Theorem	lgsdi 15795	The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that M and N are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.)
|- ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( A /L ( M x. N ) ) = ( ( A /L M ) x. ( A /L N ) ) )
Theorem	lgsne0 15796	The Legendre symbol is nonzero (and hence equal to 1 or -u 1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )
Theorem	lgsabs1 15797	The Legendre symbol is nonzero (and hence equal to 1 or -u 1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )
Theorem	lgssq 15798	The Legendre symbol at a square is equal to 1. Together with lgsmod 15784 this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.) (Revised by AV, 20-Jul-2021.)
|- ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ 2 ) /L N ) = 1 )
Theorem	lgssq2 15799	The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.)
|- ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L ( N ^ 2 ) ) = 1 )
Theorem	lgsprme0 15800	The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in [ApostolNT] p. 179. (Contributed by AV, 20-Jul-2021.)
|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) = 0 <-> ( A mod P ) = 0 ) )