P. 211 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 21001-21100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dchrptlem1 21001*	Lemma for dchrpt 21004. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- .x. = (.g ` H )   &    |- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. Word U )   &    |- ( ph -> H dom DProd S )   &    |- ( ph -> ( H DProd S ) = U )   &    |- P = ( HdProj S )   &    |- O = ( od ` H )   &    |- T = ( -u 1 ^ c ( 2 / ( O ` ( W ` I ) ) ) )   &    |- ( ph -> I e. dom W )   &    |- ( ph -> ( ( P ` I ) ` A ) =/= .1. )   &    |- X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )   =>    |- ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( X ` C ) = ( T ^ M ) )
Theorem	dchrptlem2 21002*	Lemma for dchrpt 21004. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- .x. = (.g ` H )   &    |- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. Word U )   &    |- ( ph -> H dom DProd S )   &    |- ( ph -> ( H DProd S ) = U )   &    |- P = ( HdProj S )   &    |- O = ( od ` H )   &    |- T = ( -u 1 ^ c ( 2 / ( O ` ( W ` I ) ) ) )   &    |- ( ph -> I e. dom W )   &    |- ( ph -> ( ( P ` I ) ` A ) =/= .1. )   &    |- X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )   =>    |- ( ph -> E. x e. D ( x ` A ) =/= 1 )
Theorem	dchrptlem3 21003*	Lemma for dchrpt 21004. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- .x. = (.g ` H )   &    |- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. Word U )   &    |- ( ph -> H dom DProd S )   &    |- ( ph -> ( H DProd S ) = U )   =>    |- ( ph -> E. x e. D ( x ` A ) =/= 1 )
Theorem	dchrpt 21004*	For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E. x e. D ( x ` A ) =/= 1 )
Theorem	dchrsum2 21005*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- U = (Unit ` Z )   =>    |- ( ph -> sum_ a e. U ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )
Theorem	dchrsum 21006*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- B = ( Base ` Z )   =>    |- ( ph -> sum_ a e. B ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )
Theorem	sumdchr2 21007*	Lemma for sumdchr 21009. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 1r ` Z )   &    |- B = ( Base ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. B )   =>    |- ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) )
Theorem	dchrhash 21008	There are exactly phi ( N ) Dirichlet characters modulo N. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   =>    |- ( N e. NN -> ( # ` D ) = ( phi ` N ) )
Theorem	sumdchr 21009*	An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 1r ` Z )   &    |- B = ( Base ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. B )   =>    |- ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( phi ` N ) , 0 ) )
Theorem	dchr2sum 21010*	An orthogonality relation for Dirichlet characters: the sum of X ( a ) x. * Y ( a ) over all a is nonzero only when X = Y. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> sum_ a e. B ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) = if ( X = Y , ( phi ` N ) , 0 ) )
Theorem	sum2dchr 21011*	An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. B )   &    |- ( ph -> C e. U )   =>    |- ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) )
13.4.7  Bertrand's postulate
Theorem	bcctr 21012	Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN0 -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
Theorem	pcbcctr 21013*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
Theorem	bcmono 21014	The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
|- ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )
Theorem	bcmax 21015	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )
Theorem	bcp1ctr 21016	Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( N e. NN0 -> ( ( 2 x. ( N + 1 ) ) _C ( N + 1 ) ) = ( ( ( 2 x. N ) _C N ) x. ( 2 x. ( ( ( 2 x. N ) + 1 ) / ( N + 1 ) ) ) ) )
Theorem	bclbnd 21017	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
Theorem	efexple 21018	Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( A ^ N ) <_ B <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
Theorem	bpos1lem 21019*	Lemma for bpos1 21020. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) -> ph )   &    |- ( N e. ( ZZ>= ` P ) -> ph )   &    |- P e. Prime   &    |- A e. NN0   &    |- ( A x. 2 ) = B   &    |- A < P   &    |- ( P < B \/ P = B )   =>    |- ( N e. ( ZZ>= ` A ) -> ph )
Theorem	bpos1 21020*	Bertrand's postulate, checked numerically for N <_ 6 4, using the prime sequence 2 , 3 , 5 , 7 , 1 3 , 2 3 , 4 3 , 8 3. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ( ( N e. NN /\ N <_ ; 6 4 ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
Theorem	bposlem1 21021	An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
|- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
Theorem	bposlem2 21022	There are no odd primes in the range ( 2 N / 3 , N ] dividing the N-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> 2 < P )   &    |- ( ph -> ( ( 2 x. N ) / 3 ) < P )   &    |- ( ph -> P <_ N )   =>    |- ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = 0 )
Theorem	bposlem3 21023*	Lemma for bpos 21030. Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 21022 and prmfac1 13073, respectively, and it does not have any in the range ( N , 2 N ] by hypothesis, the product of the primes up through 2 N / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   =>    |- ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )
Theorem	bposlem4 21024*	Lemma for bpos 21030. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   &    |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )   =>    |- ( ph -> M e. ( 3 ... K ) )
Theorem	bposlem5 21025*	Lemma for bpos 21030. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   &    |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )   =>    |- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^ c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
Theorem	bposlem6 21026*	Lemma for bpos 21030. By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   &    |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )   =>    |- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^ c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^ c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
Theorem	bposlem7 21027*	Lemma for bpos 21030. The function F is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- F = ( n e. NN |-> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) ) )   &    |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( _e ^ 2 ) <_ A )   &    |- ( ph -> ( _e ^ 2 ) <_ B )   =>    |- ( ph -> ( A < B -> ( F ` B ) < ( F ` A ) ) )
Theorem	bposlem8 21028	Lemma for bpos 21030. Evaluate F ( 6 4 ) and show it is less than log 2. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- F = ( n e. NN |-> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) ) )   &    |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )   =>    |- ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) )
Theorem	bposlem9 21029*	Lemma for bpos 21030. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- F = ( n e. NN |-> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) ) )   &    |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ; 6 4 < N )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   =>    |- ( ph -> ps )
Theorem	bpos 21030*	Bertrand's postulate: there is a prime between N and 2 N for every positive integer N. This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( N e. NN -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
13.4.8  Legendre symbol
Syntax	clgs 21031	Extend class notation with the Legendre symbol function.
class / L
Definition	df-lgs 21032*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers). (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	lgslem1 21033	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 21034	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 21035*	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 21036*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 } although this representation is less useful to us). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- 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 21037*	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	lgsfval 21038*	Value 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 ) )   =>    |- ( 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 21039*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 } although this representation is less useful to us). (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 21040*	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 21041*	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 21042*	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 21043*	Lemma for lgsval2 21049. (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 21044*	Lemma for lgsval4 21053. (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 21045*	The Legendre symbol is an integer with absolute value less 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 21046	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 21047	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 21048	The Legendre symbol has absolute value less or equal to 1. Together with lgscl 21047 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 21049	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 21050	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 21051	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 21052	The Legendre symbol is equivalent to a ^ ( ( p - 1 ) / 2 ), mod p. (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 21053*	Restate lgsval 21037 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 21054*	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 21055*	Same as lgsval4 21053 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	lgsneg 21056	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 21057	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 21058	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 21059	Lemma for lgsdi 21069 and lgsdir 21067: 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 21060	Lemma for lgsdir2 21065. (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 21061	Lemma for lgsdir2 21065. (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 21062	Lemma for lgsdir2 21065. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
Theorem	lgsdir2lem4 21063	Lemma for lgsdir2 21065. (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 21064	Lemma for lgsdir2 21065. (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 21065	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 21066	The Legendre symbol is completely multiplicative at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ B e. ZZ /\ P e. Prime ) -> ( ( A x. B ) / L P ) = ( ( A / L P ) x. ( B / L P ) ) )
Theorem	lgsdir 21067	The Legendre symbol is completely multiplicative in its left argument. Together with lgsqr 21083 this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (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 21068*	Lemma for lgsdi 21069. (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 21069	The Legendre symbol is completely multiplicative in its right argument. (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 21070	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 21071	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 21072	The Legendre symbol at a square is equal to 1. Together with lgsmod 21058 this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.)
|- ( ( A e. NN /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ 2 ) / L N ) = 1 )
Theorem	lgssq2 21073	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	1lgs 21074	The Legendre symbol at 1. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( N e. ZZ -> ( 1 / L N ) = 1 )
Theorem	lgs1 21075	The Legendre symbol at 1. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( A e. ZZ -> ( A / L 1 ) = 1 )
Theorem	lgsdirnn0 21076	Variation on lgsdir 21067 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 21077	Variation on lgsdi 21069 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 ) ) )
Theorem	lgsqrlem1 21078	Lemma for lgsqr 21083. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` P )   &    |- S = (Poly1 ` Y )   &    |- B = ( Base ` S )   &    |- D = ( deg1 ` Y )   &    |- O = (eval1 ` Y )   &    |- .^ = (.g ` (mulGrp ` S ) )   &    |- X = (var1 ` Y )   &    |- .- = ( -g ` S )   &    |- .1. = ( 1r ` S )   &    |- T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )   &    |- L = ( ZRHom ` Y )   &    |- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> ( ( A ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) )   =>    |- ( ph -> ( ( O ` T ) ` ( L ` A ) ) = ( 0g ` Y ) )
Theorem	lgsqrlem2 21079*	Lemma for lgsqr 21083. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` P )   &    |- S = (Poly1 ` Y )   &    |- B = ( Base ` S )   &    |- D = ( deg1 ` Y )   &    |- O = (eval1 ` Y )   &    |- .^ = (.g ` (mulGrp ` S ) )   &    |- X = (var1 ` Y )   &    |- .- = ( -g ` S )   &    |- .1. = ( 1r ` S )   &    |- T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )   &    |- L = ( ZRHom ` Y )   &    |- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )   =>    |- ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
Theorem	lgsqrlem3 21080*	Lemma for lgsqr 21083. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` P )   &    |- S = (Poly1 ` Y )   &    |- B = ( Base ` S )   &    |- D = ( deg1 ` Y )   &    |- O = (eval1 ` Y )   &    |- .^ = (.g ` (mulGrp ` S ) )   &    |- X = (var1 ` Y )   &    |- .- = ( -g ` S )   &    |- .1. = ( 1r ` S )   &    |- T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )   &    |- L = ( ZRHom ` Y )   &    |- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> ( A / L P ) = 1 )   =>    |- ( ph -> ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
Theorem	lgsqrlem4 21081*	Lemma for lgsqr 21083. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` P )   &    |- S = (Poly1 ` Y )   &    |- B = ( Base ` S )   &    |- D = ( deg1 ` Y )   &    |- O = (eval1 ` Y )   &    |- .^ = (.g ` (mulGrp ` S ) )   &    |- X = (var1 ` Y )   &    |- .- = ( -g ` S )   &    |- .1. = ( 1r ` S )   &    |- T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )   &    |- L = ( ZRHom ` Y )   &    |- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> ( A / L P ) = 1 )   =>    |- ( ph -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )
Theorem	lgsqrlem5 21082*	Lemma for lgsqr 21083. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A / L P ) = 1 ) -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )
Theorem	lgsqr 21083*	The Legendre symbol for odd primes is 1 iff the number is not a multiple of the prime (in which case it is 0, see lgsne0 21070) and the number is a quadratic residue mod P (it is -u 1 for nonresidues by the process of elimination from lgsabs1 21071). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A / L P ) = 1 <-> ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) ) )
Theorem	lgsdchrval 21084*	The Legendre symbol function X ( m ) = ( m / L N ), where N is an odd positive number, is a Dirichlet character modulo N. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- L = ( ZRHom ` Z )   &    |- X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m / L N ) ) ) )   =>    |- ( ( ( N e. NN /\ -. 2 || N ) /\ A e. ZZ ) -> ( X ` ( L ` A ) ) = ( A / L N ) )
Theorem	lgsdchr 21085*	The Legendre symbol function X ( m ) = ( m / L N ), where N is an odd positive number, is a real Dirichlet character modulo N. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- L = ( ZRHom ` Z )   &    |- X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m / L N ) ) ) )   =>    |- ( ( N e. NN /\ -. 2 || N ) -> ( X e. D /\ X : B --> RR ) )
13.4.9  Quadratic reciprocity
Theorem	lgseisenlem1 21086*	Lemma for lgseisen 21090. 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 21087*	Lemma for lgseisen 21090. 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 21088*	Lemma for lgseisen 21090. (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 )   &    |- 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 21089*	Lemma for lgseisen 21090. The function M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-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 )   &    |- 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 21090*	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	lgsquadlem1 21091*	Lemma for lgsquad 21094. 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 21092*	Lemma for lgsquad 21094. Count the members of S with even coordinates, and combine with lgsquadlem1 21091 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 21093*	Lemma for lgsquad 21094. (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 21094	The Law of Quadratic Reciprocity. 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. (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 21095	Lemma for lgsquad2 21097. (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 21096*	Lemma for lgsquad2 21097. (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 21097	Extend lgsquad 21094 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 21098	Extend lgsquad2 21097 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 21099	The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime P iff P == 1 mod 4. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( P e. ( Prime \ { 2 } ) -> ( ( -u 1 / L P ) = 1 <-> ( P mod 4 ) = 1 ) )
13.4.10  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 21100*	Lemma for 2sq 21113. (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 ) )