P. 154 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rprelogbdiv 15301	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 15302	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 15303	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 15304	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 15305	The general logarithm function is monotone/increasing. See logleb 15219. (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 15306	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 15218. (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 15307	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 15308	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 15309	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 15310	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 15311	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 15312	Lemma for logbgcd1irrap 15314. 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 15313	Lemma for logbgcd1irrap 15314. 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 15314	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 15315	Example for logbgcd1irr 15311. The logarithm of nine to base two is not rational. Also see 2logb9irrap 15321 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 15316	The logarithm of a prime to a different prime base is not rational. For example, ( 2 logb 3 ) e. ( RR \ QQ ) (see 2logb3irr 15317). (Contributed by AV, 31-Dec-2022.)
|- ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> ( B logb X ) e. ( RR \ QQ ) )
Theorem	2logb3irr 15317	Example for logbprmirr 15316. The logarithm of three to base two is not rational. (Contributed by AV, 31-Dec-2022.)
|- ( 2 logb 3 ) e. ( RR \ QQ )
Theorem	2logb9irrALT 15318	Alternate proof of 2logb9irr 15315: 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 15319	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 12359 resp. 2logb9irr 15315), satisfying the statement in 2irrexpq 15320. (Contributed by AV, 29-Dec-2022.)
|- ( ( sqr ` 2 ) ^c ( 2 logb 9 ) ) = 3
Theorem	2irrexpq 15320*	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 12359, 2logb9irr 15315 and sqrt2cxp2logb9e3 15319. 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 15322. (Contributed by AV, 23-Dec-2022.)
|- E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ
Theorem	2logb9irrap 15321	Example for logbgcd1irrap 15314. 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 15322*	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 12375, 2logb9irrap 15321 and sqrt2cxp2logb9e3 15319. 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 15323	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11668, 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 15324	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 12431, ( 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 15325	Extend class notation with the divisor function.
class sigma
Definition	df-sgm 15326*	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 15327*	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 15328*	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 15329*	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 15330	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 15331	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 15332	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 15333*	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 15334*	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 15335*	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 8021. (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 15336*	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 15337	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 15338	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 15339	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 15340	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 15341	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 15342	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 15343	Lemma for perfect 15345. (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 15344	Lemma for perfect 15345. (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 15345*	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 15341. 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 15347 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 15346	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 15347*	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 15348	{ -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 15349	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 15350	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 15351*	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 15352*	Lemma for lgsfcl2 15355. (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 15353*	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 15354*	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 15355*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 }, see zabsle1 15348). (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 15356*	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 15357*	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 15358*	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 15359*	Lemma for lgsval2 15365. (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 15360*	Lemma for lgsval4 15369. (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 15361*	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 15362	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 15363	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 15364	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 15363 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 15365	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 15366	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 15367	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 15368	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 15369*	Restate lgsval 15353 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 15370*	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 15371*	Same as lgsval4 15369 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 15372	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 15373	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 15374	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 15375	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 15376	Lemma for lgsdi 15386 and lgsdir 15384: 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 15377	Lemma for lgsdir2 15382. (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 15378	Lemma for lgsdir2 15382. (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 15379	Lemma for lgsdir2 15382. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
Theorem	lgsdir2lem4 15380	Lemma for lgsdir2 15382. (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 15381	Lemma for lgsdir2 15382. (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 15382	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 15383	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 15384	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 15385*	Lemma for lgsdi 15386. (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 15386	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 15387	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 15388	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 15389	The Legendre symbol at a square is equal to 1. Together with lgsmod 15375 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 15390	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 15391	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 ) )
Theorem	1lgs 15392	The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( N e. ZZ -> ( 1 /L N ) = 1 )
Theorem	lgs1 15393	The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( A e. ZZ -> ( A /L 1 ) = 1 )
Theorem	lgsmodeq 15394	The Legendre (Jacobi) symbol is preserved under reduction mod n when n is odd. Theorem 9.9(c) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( ( A mod N ) = ( B mod N ) -> ( A /L N ) = ( B /L N ) ) )
Theorem	lgsmulsqcoprm 15395	The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( ( A ^ 2 ) x. B ) /L N ) = ( B /L N ) )
Theorem	lgsdirnn0 15396	Variation on lgsdir 15384 valid for all A , B but only for positive N. (The exact location of the failure of this law is for A = 0, B < 0, N = -u 1 in which case ( 0 /L -u 1 ) = 1 but ( B /L -u 1 ) = -u 1.) (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
Theorem	lgsdinn0 15397	Variation on lgsdi 15386 valid for all M , N but only for positive A. (The exact location of the failure of this law is for A = -u 1, M = 0, and some N in which case ( -u 1 /L 0 ) = 1 but ( -u 1 /L N ) = -u 1 when -u 1 is not a quadratic residue mod N.) (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( ( A e. NN0 /\ M e. ZZ /\ N e. ZZ ) -> ( A /L ( M x. N ) ) = ( ( A /L M ) x. ( A /L N ) ) )
11.3.5  Gauss' Lemma Gauss' Lemma is valid for any integer not dividing the given prime number. In the following, only the special case for 2 (not dividing any odd prime) is proven, see gausslemma2d 15418. The general case is still to prove.
Theorem	gausslemma2dlem0a 15398	Auxiliary lemma 1 for gausslemma2d 15418. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   =>    |- ( ph -> P e. NN )
Theorem	gausslemma2dlem0b 15399	Auxiliary lemma 2 for gausslemma2d 15418. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> H e. NN )
Theorem	gausslemma2dlem0c 15400	Auxiliary lemma 3 for gausslemma2d 15418. (Contributed by AV, 13-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> ( ( ! ` H ) gcd P ) = 1 )