P. 240 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23901-24000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dchrzrhcl 23901	A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. ZZ )   =>    |- ( ph -> ( X ` ( L ` A ) ) e. CC )
Theorem	dchrzrhmul 23902	A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> C e. ZZ )   =>    |- ( ph -> ( X ` ( L ` ( A x. C ) ) ) = ( ( X ` ( L ` A ) ) x. ( X ` ( L ` C ) ) ) )
Theorem	dchrplusg 23903	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .x. = ( +g ` G )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> .x. = ( oF x. |` ( D X. D ) ) )
Theorem	dchrmul 23904	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( X .x. Y ) = ( X oF x. Y ) )
Theorem	dchrmulcl 23905	Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( X .x. Y ) e. D )
Theorem	dchrn0 23906	A Dirichlet character is nonzero on the units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( ( X ` A ) =/= 0 <-> A e. U ) )
Theorem	dchr1cl 23907*	Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> .1. e. D )
Theorem	dchrmulid2 23908*	Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( .1. .x. X ) = X )
Theorem	dchrinvcl 23909*	Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   &    |- K = ( k e. B |-> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) )   =>    |- ( ph -> ( K e. D /\ ( K .x. X ) = .1. ) )
Theorem	dchrabl 23910	The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   =>    |- ( N e. NN -> G e. Abel )
Theorem	dchrfi 23911	The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   =>    |- ( N e. NN -> D e. Fin )
Theorem	dchrghm 23912	A Dirichlet character restricted to the unit group of ℤ/nℤ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- M = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( X |` U ) e. ( H GrpHom M ) )
Theorem	dchr1 23913	Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 0g ` G )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. U )   =>    |- ( ph -> ( .1. ` A ) = 1 )
Theorem	dchreq 23914*	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- U = (Unit ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( X = Y <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )
Theorem	dchrresb 23915	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- U = (Unit ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( ( X |` U ) = ( Y |` U ) <-> X = Y ) )
Theorem	dchrabs 23916	A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- ( ph -> X e. D )   &    |- Z = (ℤ/nℤ ` N )   &    |- U = (Unit ` Z )   &    |- ( ph -> A e. U )   =>    |- ( ph -> ( abs ` ( X ` A ) ) = 1 )
Theorem	dchrinv 23917	The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- ( ph -> X e. D )   &    |- I = ( invg ` G )   =>    |- ( ph -> ( I ` X ) = ( * o. X ) )
Theorem	dchrabs2 23918	A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( abs ` ( X ` A ) ) <_ 1 )
Theorem	dchr1re 23919	The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 0g ` G )   &    |- B = ( Base ` Z )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> .1. : B --> RR )
Theorem	dchrptlem1 23920*	Lemma for dchrpt 23923. (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 23921*	Lemma for dchrpt 23923. (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 23922*	Lemma for dchrpt 23923. (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 23923*	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 23924*	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 23925*	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 23926*	Lemma for sumdchr 23928. (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 23927	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 23928*	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 23929*	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 23930*	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 ) )
14.4.7  Bertrand's postulate
Theorem	bcctr 23931	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 23932*	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 23933	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 23934	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 23935	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 23936	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 23937	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 23938*	Lemma for bpos1 23939. (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 23939*	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 23940	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 23941	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 23942*	Lemma for bpos 23949. Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 23941 and prmfac1 14468, 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 23943*	Lemma for bpos 23949. (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 23944*	Lemma for bpos 23949. 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 23945*	Lemma for bpos 23949. 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 23946*	Lemma for bpos 23949. 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 23947	Lemma for bpos 23949. 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 23948*	Lemma for bpos 23949. 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 23949*	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. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( N e. NN -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
14.4.8  Legendre symbol
Syntax	clgs 23950	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 23951*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). (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 23952	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 23953	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 23954*	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 23955*	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 23956*	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 23957*	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 23958*	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 23959*	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 23960*	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 23961*	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 23962*	Lemma for lgsval2 23968. (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 23963*	Lemma for lgsval4 23972. (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 23964*	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 23965	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 23966	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 23967	The Legendre symbol has absolute value less or equal to 1. Together with lgscl 23966 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 23968	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 23969	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 23970	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 23971	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 23972*	Restate lgsval 23956 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 23973*	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 23974*	Same as lgsval4 23972 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 23975	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 23976	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 23977	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 23978	Lemma for lgsdi 23988 and lgsdir 23986: 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 23979	Lemma for lgsdir2 23984. (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 23980	Lemma for lgsdir2 23984. (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 23981	Lemma for lgsdir2 23984. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
Theorem	lgsdir2lem4 23982	Lemma for lgsdir2 23984. (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 23983	Lemma for lgsdir2 23984. (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 23984	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 23985	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 23986	The Legendre symbol is completely multiplicative in its left argument. Together with lgsqr 24002 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 23987*	Lemma for lgsdi 23988. (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 23988	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 23989	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 23990	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 23991	The Legendre symbol at a square is equal to 1. Together with lgsmod 23977 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 23992	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 23993	The Legendre symbol at 1. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( N e. ZZ -> ( 1 /L N ) = 1 )
Theorem	lgs1 23994	The Legendre symbol at 1. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( A e. ZZ -> ( A /L 1 ) = 1 )
Theorem	lgsdirnn0 23995	Variation on lgsdir 23986 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 23996	Variation on lgsdi 23988 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 23997	Lemma for lgsqr 24002. (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 23998*	Lemma for lgsqr 24002. (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 23999*	Lemma for lgsqr 24002. (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 24000*	Lemma for lgsqr 24002. (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 ) )