P. 161 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16001-16100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lgslem3 16001*	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 16002*	Lemma for lgsfcl2 16005. (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 16003*	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 16004*	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 16005*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 }, see zabsle1 15998). (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 16006*	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 16007*	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 16008*	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 16009*	Lemma for lgsval2 16015. (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 16010*	Lemma for lgsval4 16019. (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 16011*	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 16012	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 16013	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 16014	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 16013 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 16015	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 16016	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 16017	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 16018	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 16019*	Restate lgsval 16003 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 16020*	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 16021*	Same as lgsval4 16019 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 16022	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 16023	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 16024	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 16025	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 16026	Lemma for lgsdi 16036 and lgsdir 16034: 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 16027	Lemma for lgsdir2 16032. (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 16028	Lemma for lgsdir2 16032. (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 16029	Lemma for lgsdir2 16032. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
Theorem	lgsdir2lem4 16030	Lemma for lgsdir2 16032. (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 16031	Lemma for lgsdir2 16032. (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 16032	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 16033	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 16034	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 16035*	Lemma for lgsdi 16036. (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 16036	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 16037	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 16038	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 16039	The Legendre symbol at a square is equal to 1. Together with lgsmod 16025 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 16040	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 16041	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 16042	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 16043	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 16044	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 16045	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 16046	Variation on lgsdir 16034 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 16047	Variation on lgsdi 16036 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.4.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 16068. The general case is still to prove.
Theorem	gausslemma2dlem0a 16048	Auxiliary lemma 1 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   =>    |- ( ph -> P e. NN )
Theorem	gausslemma2dlem0b 16049	Auxiliary lemma 2 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> H e. NN )
Theorem	gausslemma2dlem0c 16050	Auxiliary lemma 3 for gausslemma2d 16068. (Contributed by AV, 13-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> ( ( ! ` H ) gcd P ) = 1 )
Theorem	gausslemma2dlem0d 16051	Auxiliary lemma 4 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> M e. NN0 )
Theorem	gausslemma2dlem0e 16052	Auxiliary lemma 5 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> ( M x. 2 ) < ( P / 2 ) )
Theorem	gausslemma2dlem0f 16053	Auxiliary lemma 6 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> ( M + 1 ) <_ H )
Theorem	gausslemma2dlem0g 16054	Auxiliary lemma 7 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> M <_ H )
Theorem	gausslemma2dlem0h 16055	Auxiliary lemma 8 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- N = ( H - M )   =>    |- ( ph -> N e. NN0 )
Theorem	gausslemma2dlem0i 16056	Auxiliary lemma 9 for gausslemma2d 16068. (Contributed by AV, 14-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- N = ( H - M )   =>    |- ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
Theorem	gausslemma2dlem1a 16057*	Lemma for gausslemma2dlem1 16060. (Contributed by AV, 1-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   =>    |- ( ph -> ran R = ( 1 ... H ) )
Theorem	gausslemma2dlem1cl 16058	Lemma for gausslemma2dlem1 16060. Closure of the body of the definition of R. (Contributed by Jim Kingdon, 10-Aug-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- ( ph -> A e. ( 1 ... H ) )   =>    |- ( ph -> if ( ( A x. 2 ) < ( P / 2 ) , ( A x. 2 ) , ( P - ( A x. 2 ) ) ) e. ZZ )
Theorem	gausslemma2dlem1f1o 16059*	Lemma for gausslemma2dlem1 16060. (Contributed by Jim Kingdon, 9-Aug-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   =>    |- ( ph -> R : ( 1 ... H ) -1-1-onto-> ( 1 ... H ) )
Theorem	gausslemma2dlem1 16060*	Lemma 1 for gausslemma2d 16068. (Contributed by AV, 5-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   =>    |- ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
Theorem	gausslemma2dlem2 16061*	Lemma 2 for gausslemma2d 16068. (Contributed by AV, 4-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) )
Theorem	gausslemma2dlem3 16062*	Lemma 3 for gausslemma2d 16068. (Contributed by AV, 4-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )
Theorem	gausslemma2dlem4 16063*	Lemma 4 for gausslemma2d 16068. (Contributed by AV, 16-Jun-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
Theorem	gausslemma2dlem5a 16064*	Lemma for gausslemma2dlem5 16065. (Contributed by AV, 8-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) mod P ) )
Theorem	gausslemma2dlem5 16065*	Lemma 5 for gausslemma2d 16068. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) )
Theorem	gausslemma2dlem6 16066*	Lemma 6 for gausslemma2d 16068. (Contributed by AV, 16-Jun-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) )
Theorem	gausslemma2dlem7 16067*	Lemma 7 for gausslemma2d 16068. (Contributed by AV, 13-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 )
Theorem	gausslemma2d 16068*	Gauss' Lemma (see also theorem 9.6 in [ApostolNT] p. 182) for integer 2: Let p be an odd prime. Let S = {2, 4, 6, ..., p - 1}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( 2 /L P ) = ( -u 1 ^ N ) )
11.4.6  Quadratic reciprocity
Theorem	lgseisenlem1 16069*	Lemma for lgseisen 16073. If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ), then for any even 1 <_ u <_ P - 1, M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   =>    |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
Theorem	lgseisenlem2 16070*	Lemma for lgseisen 16073. The function M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   &    |- S = ( ( Q x. ( 2 x. y ) ) mod P )   =>    |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
Theorem	lgseisenlem3 16071*	Lemma for lgseisen 16073. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   &    |- S = ( ( Q x. ( 2 x. y ) ) mod P )   &    |- Y = (ℤ/nℤ ` P )   &    |- G = (mulGrp ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( ph -> ( G gsumg ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( 1r ` Y ) )
Theorem	lgseisenlem4 16072*	Lemma for lgseisen 16073. (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   &    |- S = ( ( Q x. ( 2 x. y ) ) mod P )   &    |- Y = (ℤ/nℤ ` P )   &    |- G = (mulGrp ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) )
Theorem	lgseisen 16073*	Eisenstein's lemma, an expression for ( P /L Q ) when P , Q are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> ( Q /L P ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
Theorem	lgsquadlemsfi 16074*	Lemma for lgsquad 16079. S is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> S e. Fin )
Theorem	lgsquadlemofi 16075*	Lemma for lgsquad 16079. There are finitely many members of S with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
Theorem	lgsquadlem1 16076*	Lemma for lgsquad 16079. Count the members of S with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )
Theorem	lgsquadlem2 16077*	Lemma for lgsquad 16079. Count the members of S with even coordinates, and combine with lgsquadlem1 16076 to get the total count of lattice points in S (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
Theorem	lgsquadlem3 16078*	Lemma for lgsquad 16079. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )
Theorem	lgsquad 16079	The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] p. 185. If P and Q are distinct odd primes, then the product of the Legendre symbols ( P /L Q ) and ( Q /L P ) is the parity of ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ). This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity. This is Metamath 100 proof #7. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) /\ P =/= Q ) -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) ) ) )
Theorem	lgsquad2lem1 16080	Lemma for lgsquad2 16082. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> -. 2 || M )   &    |- ( ph -> N e. NN )   &    |- ( ph -> -. 2 || N )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( A x. B ) = M )   &    |- ( ph -> ( ( A /L N ) x. ( N /L A ) ) = ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )   &    |- ( ph -> ( ( B /L N ) x. ( N /L B ) ) = ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )   =>    |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Theorem	lgsquad2lem2 16081*	Lemma for lgsquad2 16082. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> -. 2 || M )   &    |- ( ph -> N e. NN )   &    |- ( ph -> -. 2 || N )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )   &    |- ( ps <-> A. x e. ( 1 ... k ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )   =>    |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Theorem	lgsquad2 16082	Extend lgsquad 16079 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> -. 2 || M )   &    |- ( ph -> N e. NN )   &    |- ( ph -> -. 2 || N )   &    |- ( ph -> ( M gcd N ) = 1 )   =>    |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Theorem	lgsquad3 16083	Extend lgsquad2 16082 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) -> ( M /L N ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )
Theorem	m1lgs 16084	The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime P iff P == 1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( P e. ( Prime \ { 2 } ) -> ( ( -u 1 /L P ) = 1 <-> ( P mod 4 ) = 1 ) )
Theorem	2lgslem1a1 16085*	Lemma 1 for 2lgslem1a 16087. (Contributed by AV, 16-Jun-2021.)
|- ( ( P e. NN /\ -. 2 || P ) -> A. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i x. 2 ) = ( ( i x. 2 ) mod P ) )
Theorem	2lgslem1a2 16086	Lemma 2 for 2lgslem1a 16087. (Contributed by AV, 18-Jun-2021.)
|- ( ( N e. ZZ /\ I e. ZZ ) -> ( ( |_ ` ( N / 4 ) ) < I <-> ( N / 2 ) < ( I x. 2 ) ) )
Theorem	2lgslem1a 16087*	Lemma 1 for 2lgslem1 16090. (Contributed by AV, 18-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } = { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } )
Theorem	2lgslem1b 16088*	Lemma 2 for 2lgslem1 16090. (Contributed by AV, 18-Jun-2021.)
|- I = ( A ... B )   &    |- F = ( j e. I |-> ( j x. 2 ) )   =>    |- F : I -1-1-onto-> { x e. ZZ | E. i e. I x = ( i x. 2 ) }
Theorem	2lgslem1c 16089	Lemma 3 for 2lgslem1 16090. (Contributed by AV, 19-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
Theorem	2lgslem1 16090*	Lemma 1 for 2lgs 16103. (Contributed by AV, 19-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> (♯ ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )
Theorem	2lgslem2 16091	Lemma 2 for 2lgs 16103. (Contributed by AV, 20-Jun-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. Prime /\ -. 2 || P ) -> N e. ZZ )
Theorem	2lgslem3a 16092	Lemma for 2lgslem3a1 16096. (Contributed by AV, 14-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 1 ) ) -> N = ( 2 x. K ) )
Theorem	2lgslem3b 16093	Lemma for 2lgslem3b1 16097. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 3 ) ) -> N = ( ( 2 x. K ) + 1 ) )
Theorem	2lgslem3c 16094	Lemma for 2lgslem3c1 16098. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 5 ) ) -> N = ( ( 2 x. K ) + 1 ) )
Theorem	2lgslem3d 16095	Lemma for 2lgslem3d1 16099. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 7 ) ) -> N = ( ( 2 x. K ) + 2 ) )
Theorem	2lgslem3a1 16096	Lemma 1 for 2lgslem3 16100. (Contributed by AV, 15-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 1 ) -> ( N mod 2 ) = 0 )
Theorem	2lgslem3b1 16097	Lemma 2 for 2lgslem3 16100. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 3 ) -> ( N mod 2 ) = 1 )
Theorem	2lgslem3c1 16098	Lemma 3 for 2lgslem3 16100. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 5 ) -> ( N mod 2 ) = 1 )
Theorem	2lgslem3d1 16099	Lemma 4 for 2lgslem3 16100. (Contributed by AV, 15-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 7 ) -> ( N mod 2 ) = 0 )
Theorem	2lgslem3 16100	Lemma 3 for 2lgs 16103. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )