P. 160 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lgsdir2lem1 15901	Lemma for lgsdir2 15906. (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 15902	Lemma for lgsdir2 15906. (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 15903	Lemma for lgsdir2 15906. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
Theorem	lgsdir2lem4 15904	Lemma for lgsdir2 15906. (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 15905	Lemma for lgsdir2 15906. (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 15906	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 15907	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 15908	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 15909*	Lemma for lgsdi 15910. (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 15910	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 15911	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 15912	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 15913	The Legendre symbol at a square is equal to 1. Together with lgsmod 15899 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 15914	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 15915	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 15916	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 15917	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 15918	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 15919	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 15920	Variation on lgsdir 15908 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 15921	Variation on lgsdi 15910 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 15942. The general case is still to prove.
Theorem	gausslemma2dlem0a 15922	Auxiliary lemma 1 for gausslemma2d 15942. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   =>    |- ( ph -> P e. NN )
Theorem	gausslemma2dlem0b 15923	Auxiliary lemma 2 for gausslemma2d 15942. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> H e. NN )
Theorem	gausslemma2dlem0c 15924	Auxiliary lemma 3 for gausslemma2d 15942. (Contributed by AV, 13-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> ( ( ! ` H ) gcd P ) = 1 )
Theorem	gausslemma2dlem0d 15925	Auxiliary lemma 4 for gausslemma2d 15942. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> M e. NN0 )
Theorem	gausslemma2dlem0e 15926	Auxiliary lemma 5 for gausslemma2d 15942. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> ( M x. 2 ) < ( P / 2 ) )
Theorem	gausslemma2dlem0f 15927	Auxiliary lemma 6 for gausslemma2d 15942. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> ( M + 1 ) <_ H )
Theorem	gausslemma2dlem0g 15928	Auxiliary lemma 7 for gausslemma2d 15942. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- H = ( ( P - 1 ) / 2 )   =>    |- ( ph -> M <_ H )
Theorem	gausslemma2dlem0h 15929	Auxiliary lemma 8 for gausslemma2d 15942. (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 15930	Auxiliary lemma 9 for gausslemma2d 15942. (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 15931*	Lemma for gausslemma2dlem1 15934. (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 15932	Lemma for gausslemma2dlem1 15934. 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 15933*	Lemma for gausslemma2dlem1 15934. (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 15934*	Lemma 1 for gausslemma2d 15942. (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 15935*	Lemma 2 for gausslemma2d 15942. (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 15936*	Lemma 3 for gausslemma2d 15942. (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 15937*	Lemma 4 for gausslemma2d 15942. (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 15938*	Lemma for gausslemma2dlem5 15939. (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 15939*	Lemma 5 for gausslemma2d 15942. (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 15940*	Lemma 6 for gausslemma2d 15942. (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 15941*	Lemma 7 for gausslemma2d 15942. (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 15942*	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 15943*	Lemma for lgseisen 15947. 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 15944*	Lemma for lgseisen 15947. 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 15945*	Lemma for lgseisen 15947. (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 15946*	Lemma for lgseisen 15947. (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 15947*	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 15948*	Lemma for lgsquad 15953. 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 15949*	Lemma for lgsquad 15953. 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 15950*	Lemma for lgsquad 15953. 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 15951*	Lemma for lgsquad 15953. Count the members of S with even coordinates, and combine with lgsquadlem1 15950 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 15952*	Lemma for lgsquad 15953. (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 15953	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 15954	Lemma for lgsquad2 15956. (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 15955*	Lemma for lgsquad2 15956. (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 15956	Extend lgsquad 15953 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 15957	Extend lgsquad2 15956 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 15958	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 15959*	Lemma 1 for 2lgslem1a 15961. (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 15960	Lemma 2 for 2lgslem1a 15961. (Contributed by AV, 18-Jun-2021.)
|- ( ( N e. ZZ /\ I e. ZZ ) -> ( ( |_ ` ( N / 4 ) ) < I <-> ( N / 2 ) < ( I x. 2 ) ) )
Theorem	2lgslem1a 15961*	Lemma 1 for 2lgslem1 15964. (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 15962*	Lemma 2 for 2lgslem1 15964. (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 15963	Lemma 3 for 2lgslem1 15964. (Contributed by AV, 19-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
Theorem	2lgslem1 15964*	Lemma 1 for 2lgs 15977. (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 15965	Lemma 2 for 2lgs 15977. (Contributed by AV, 20-Jun-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. Prime /\ -. 2 || P ) -> N e. ZZ )
Theorem	2lgslem3a 15966	Lemma for 2lgslem3a1 15970. (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 15967	Lemma for 2lgslem3b1 15971. (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 15968	Lemma for 2lgslem3c1 15972. (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 15969	Lemma for 2lgslem3d1 15973. (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 15970	Lemma 1 for 2lgslem3 15974. (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 15971	Lemma 2 for 2lgslem3 15974. (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 15972	Lemma 3 for 2lgslem3 15974. (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 15973	Lemma 4 for 2lgslem3 15974. (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 15974	Lemma 3 for 2lgs 15977. (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 ) )
Theorem	2lgs2 15975	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
|- ( 2 /L 2 ) = 0
Theorem	2lgslem4 15976	Lemma 4 for 2lgs 15977: special case of 2lgs 15977 for P = 2. (Contributed by AV, 20-Jun-2021.)
|- ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } )
Theorem	2lgs 15977	The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime P iff P == pm 1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of ( N /L 2 ) (lgs2 15890) to some degree, by demanding that reciprocity extend to the case Q = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.)
|- ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
Theorem	2lgsoddprmlem1 15978	Lemma 1 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )
Theorem	2lgsoddprmlem2 15979	Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )
Theorem	2lgsoddprmlem3a 15980	Lemma 1 for 2lgsoddprmlem3 15984. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 1 ^ 2 ) - 1 ) / 8 ) = 0
Theorem	2lgsoddprmlem3b 15981	Lemma 2 for 2lgsoddprmlem3 15984. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1
Theorem	2lgsoddprmlem3c 15982	Lemma 3 for 2lgsoddprmlem3 15984. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3
Theorem	2lgsoddprmlem3d 15983	Lemma 4 for 2lgsoddprmlem3 15984. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )
Theorem	2lgsoddprmlem3 15984	Lemma 3 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) )
Theorem	2lgsoddprmlem4 15985	Lemma 4 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )
Theorem	2lgsoddprm 15986	The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in [ApostolNT] p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ( ( 2 /L P ) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.)
|- ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
11.4.7  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 15987*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( A e. S <-> E. x e. ZZ[_i] A = ( ( abs ` x ) ^ 2 ) )
Theorem	2sqlem2 15988*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( A e. S <-> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
Theorem	mul2sq 15989	Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )
Theorem	2sqlem3 15990	Lemma for 2sqlem5 15992. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )   &    |- ( ph -> P || ( ( C x. B ) + ( A x. D ) ) )   =>    |- ( ph -> N e. S )
Theorem	2sqlem4 15991	Lemma for 2sqlem5 15992. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )   =>    |- ( ph -> N e. S )
Theorem	2sqlem5 15992	Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( N x. P ) e. S )   &    |- ( ph -> P e. S )   =>    |- ( ph -> N e. S )
Theorem	2sqlem6 15993*	Lemma for 2sq . If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> A. p e. Prime ( p || B -> p e. S ) )   &    |- ( ph -> ( A x. B ) e. S )   =>    |- ( ph -> A e. S )
Theorem	2sqlem7 15994*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   =>    |- Y C_ ( S i^i NN )
Theorem	2sqlem8a 15995*	Lemma for 2sqlem8 15996. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> ( A gcd B ) = 1 )   &    |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( C gcd D ) e. NN )
Theorem	2sqlem8 15996*	Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> ( A gcd B ) = 1 )   &    |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- E = ( C / ( C gcd D ) )   &    |- F = ( D / ( C gcd D ) )   =>    |- ( ph -> M e. S )
Theorem	2sqlem9 15997*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. Y )   =>    |- ( ph -> M e. S )
Theorem	2sqlem10 15998*	Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   =>    |- ( ( A e. Y /\ B e. NN /\ B || A ) -> B e. S )
PART 12  GRAPH THEORY
12.1  Vertices and edges
12.1.1  The edge function extractor for extensible structures
Syntax	cedgf 15999	Extend class notation with an edge function.
class .ef
Definition	df-edgf 16000	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 16001 instead. (New usage is discouraged.)
|- .ef = Slot ; 1 8