Home | Metamath
Proof Explorer Theorem List (p. 266 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | perfect 26501* | The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer π is a perfect number (that is, its divisor sum is 2π) if and only if it is of the form 2β(π β 1) Β· (2βπ β 1), where 2βπ β 1 is prime (a Mersenne prime). (It follows from this that π is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ ((π β β β§ 2 β₯ π) β ((1 Ο π) = (2 Β· π) β βπ β β€ (((2βπ) β 1) β β β§ π = ((2β(π β 1)) Β· ((2βπ) β 1))))) | ||
Syntax | cdchr 26502 | Extend class notation with the group of Dirichlet characters. |
class DChr | ||
Definition | df-dchr 26503* | The group of Dirichlet characters mod π is the set of monoid homomorphisms from β€ / πβ€ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ DChr = (π β β β¦ β¦(β€/nβ€βπ) / π§β¦β¦{π₯ β ((mulGrpβπ§) MndHom (mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} / πβ¦{β¨(Baseβndx), πβ©, β¨(+gβndx), ( βf Β· βΎ (π Γ π))β©}) | ||
Theorem | dchrval 26504* | Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ (π β π· = {π₯ β ((mulGrpβπ) MndHom (mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) β β’ (π β πΊ = {β¨(Baseβndx), π·β©, β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©}) | ||
Theorem | dchrbas 26505* | Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ π· = (BaseβπΊ) β β’ (π β π· = {π₯ β ((mulGrpβπ) MndHom (mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) | ||
Theorem | dchrelbas 26506 | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on β€/nβ€ to the multiplicative monoid of β, which is zero off the group of units of β€/nβ€. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ π· = (BaseβπΊ) β β’ (π β (π β π· β (π β ((mulGrpβπ) MndHom (mulGrpββfld)) β§ ((π΅ β π) Γ {0}) β π))) | ||
Theorem | dchrelbas2 26507* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on β€/nβ€ to the multiplicative monoid of β, which is zero off the group of units of β€/nβ€. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ π· = (BaseβπΊ) β β’ (π β (π β π· β (π β ((mulGrpβπ) MndHom (mulGrpββfld)) β§ βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β π)))) | ||
Theorem | dchrelbas3 26508* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on β€/nβ€ to the multiplicative monoid of β, which is zero off the group of units of β€/nβ€. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ π· = (BaseβπΊ) β β’ (π β (π β π· β (π:π΅βΆβ β§ (βπ₯ β π βπ¦ β π (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(1rβπ)) = 1 β§ βπ₯ β π΅ ((πβπ₯) β 0 β π₯ β π))))) | ||
Theorem | dchrelbasd 26509* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on β€/nβ€ to the multiplicative monoid of β, which is zero off the group of units of β€/nβ€. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ π· = (BaseβπΊ) & β’ (π = π₯ β π = π΄) & β’ (π = π¦ β π = πΆ) & β’ (π = (π₯(.rβπ)π¦) β π = πΈ) & β’ (π = (1rβπ) β π = π) & β’ ((π β§ π β π) β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β πΈ = (π΄ Β· πΆ)) & β’ (π β π = 1) β β’ (π β (π β π΅ β¦ if(π β π, π, 0)) β π·) | ||
Theorem | dchrrcl 26510 | Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) β β’ (π β π· β π β β) | ||
Theorem | dchrmhm 26511 | A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) β β’ π· β ((mulGrpβπ) MndHom (mulGrpββfld)) | ||
Theorem | dchrf 26512 | A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ (π β π β π·) β β’ (π β π:π΅βΆβ) | ||
Theorem | dchrelbas4 26513* | A Dirichlet character is a monoid homomorphism from the multiplicative monoid on β€/nβ€ to the multiplicative monoid of β, which is zero off the group of units of β€/nβ€. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ πΏ = (β€RHomβπ) β β’ (π β π· β (π β β β§ π β ((mulGrpβπ) MndHom (mulGrpββfld)) β§ βπ₯ β β€ (1 < (π₯ gcd π) β (πβ(πΏβπ₯)) = 0))) | ||
Theorem | dchrzrh1 26514 | Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β π·) β β’ (π β (πβ(πΏβ1)) = 1) | ||
Theorem | dchrzrhcl 26515 | A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β π·) & β’ (π β π΄ β β€) β β’ (π β (πβ(πΏβπ΄)) β β) | ||
Theorem | dchrzrhmul 26516 | A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β π·) & β’ (π β π΄ β β€) & β’ (π β πΆ β β€) β β’ (π β (πβ(πΏβ(π΄ Β· πΆ))) = ((πβ(πΏβπ΄)) Β· (πβ(πΏβπΆ)))) | ||
Theorem | dchrplusg 26517 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ Β· = (+gβπΊ) & β’ (π β π β β) β β’ (π β Β· = ( βf Β· βΎ (π· Γ π·))) | ||
Theorem | dchrmul 26518 | Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ Β· = (+gβπΊ) & β’ (π β π β π·) & β’ (π β π β π·) β β’ (π β (π Β· π) = (π βf Β· π)) | ||
Theorem | dchrmulcl 26519 | Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ Β· = (+gβπΊ) & β’ (π β π β π·) & β’ (π β π β π·) β β’ (π β (π Β· π) β π·) | ||
Theorem | dchrn0 26520 | A Dirichlet character is nonzero on the units of β€/nβ€. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β π·) & β’ (π β π΄ β π΅) β β’ (π β ((πβπ΄) β 0 β π΄ β π)) | ||
Theorem | dchr1cl 26521* | Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ 1 = (π β π΅ β¦ if(π β π, 1, 0)) & β’ (π β π β β) β β’ (π β 1 β π·) | ||
Theorem | dchrmulid2 26522* | Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ 1 = (π β π΅ β¦ if(π β π, 1, 0)) & β’ Β· = (+gβπΊ) & β’ (π β π β π·) β β’ (π β ( 1 Β· π) = π) | ||
Theorem | dchrinvcl 26523* | Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ 1 = (π β π΅ β¦ if(π β π, 1, 0)) & β’ Β· = (+gβπΊ) & β’ (π β π β π·) & β’ πΎ = (π β π΅ β¦ if(π β π, (1 / (πβπ)), 0)) β β’ (π β (πΎ β π· β§ (πΎ Β· π) = 1 )) | ||
Theorem | dchrabl 26524 | The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ πΊ = (DChrβπ) β β’ (π β β β πΊ β Abel) | ||
Theorem | dchrfi 26525 | The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) β β’ (π β β β π· β Fin) | ||
Theorem | dchrghm 26526 | 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.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π = (Unitβπ) & β’ π» = ((mulGrpβπ) βΎs π) & β’ π = ((mulGrpββfld) βΎs (β β {0})) & β’ (π β π β π·) β β’ (π β (π βΎ π) β (π» GrpHom π)) | ||
Theorem | dchr1 26527 | Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ 1 = (0gβπΊ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ (π β π΄ β π) β β’ (π β ( 1 βπ΄) = 1) | ||
Theorem | dchreq 26528* | A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π = (Unitβπ) & β’ (π β π β π·) & β’ (π β π β π·) β β’ (π β (π = π β βπ β π (πβπ) = (πβπ))) | ||
Theorem | dchrresb 26529 | A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π = (Unitβπ) & β’ (π β π β π·) & β’ (π β π β π·) β β’ (π β ((π βΎ π) = (π βΎ π) β π = π)) | ||
Theorem | dchrabs 26530 | A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) & β’ (π β π β π·) & β’ π = (β€/nβ€βπ) & β’ π = (Unitβπ) & β’ (π β π΄ β π) β β’ (π β (absβ(πβπ΄)) = 1) | ||
Theorem | dchrinv 26531 | The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of π are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) & β’ (π β π β π·) & β’ πΌ = (invgβπΊ) β β’ (π β (πΌβπ) = (β β π)) | ||
Theorem | dchrabs2 26532 | A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π·) & β’ (π β π΄ β π΅) β β’ (π β (absβ(πβπ΄)) β€ 1) | ||
Theorem | dchr1re 26533 | The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ 1 = (0gβπΊ) & β’ π΅ = (Baseβπ) & β’ (π β π β β) β β’ (π β 1 :π΅βΆβ) | ||
Theorem | dchrptlem1 26534* | Lemma for dchrpt 26537. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ 1 = (1rβπ) & β’ (π β π β β) & β’ (π β π΄ β 1 ) & β’ π = (Unitβπ) & β’ π» = ((mulGrpβπ) βΎs π) & β’ Β· = (.gβπ») & β’ π = (π β dom π β¦ ran (π β β€ β¦ (π Β· (πβπ)))) & β’ (π β π΄ β π) & β’ (π β π β Word π) & β’ (π β π»dom DProd π) & β’ (π β (π» DProd π) = π) & β’ π = (π»dProjπ) & β’ π = (odβπ») & β’ π = (-1βπ(2 / (πβ(πβπΌ)))) & β’ (π β πΌ β dom π) & β’ (π β ((πβπΌ)βπ΄) β 1 ) & β’ π = (π’ β π β¦ (β©ββπ β β€ (((πβπΌ)βπ’) = (π Β· (πβπΌ)) β§ β = (πβπ)))) β β’ (((π β§ πΆ β π) β§ (π β β€ β§ ((πβπΌ)βπΆ) = (π Β· (πβπΌ)))) β (πβπΆ) = (πβπ)) | ||
Theorem | dchrptlem2 26535* | Lemma for dchrpt 26537. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ 1 = (1rβπ) & β’ (π β π β β) & β’ (π β π΄ β 1 ) & β’ π = (Unitβπ) & β’ π» = ((mulGrpβπ) βΎs π) & β’ Β· = (.gβπ») & β’ π = (π β dom π β¦ ran (π β β€ β¦ (π Β· (πβπ)))) & β’ (π β π΄ β π) & β’ (π β π β Word π) & β’ (π β π»dom DProd π) & β’ (π β (π» DProd π) = π) & β’ π = (π»dProjπ) & β’ π = (odβπ») & β’ π = (-1βπ(2 / (πβ(πβπΌ)))) & β’ (π β πΌ β dom π) & β’ (π β ((πβπΌ)βπ΄) β 1 ) & β’ π = (π’ β π β¦ (β©ββπ β β€ (((πβπΌ)βπ’) = (π Β· (πβπΌ)) β§ β = (πβπ)))) β β’ (π β βπ₯ β π· (π₯βπ΄) β 1) | ||
Theorem | dchrptlem3 26536* | Lemma for dchrpt 26537. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ 1 = (1rβπ) & β’ (π β π β β) & β’ (π β π΄ β 1 ) & β’ π = (Unitβπ) & β’ π» = ((mulGrpβπ) βΎs π) & β’ Β· = (.gβπ») & β’ π = (π β dom π β¦ ran (π β β€ β¦ (π Β· (πβπ)))) & β’ (π β π΄ β π) & β’ (π β π β Word π) & β’ (π β π»dom DProd π) & β’ (π β (π» DProd π) = π) β β’ (π β βπ₯ β π· (π₯βπ΄) β 1) | ||
Theorem | dchrpt 26537* | 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.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ 1 = (1rβπ) & β’ (π β π β β) & β’ (π β π΄ β 1 ) & β’ (π β π΄ β π΅) β β’ (π β βπ₯ β π· (π₯βπ΄) β 1) | ||
Theorem | dchrsum2 26538* | An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character π is 0 if π is non-principal and Ο(π) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ 1 = (0gβπΊ) & β’ (π β π β π·) & β’ π = (Unitβπ) β β’ (π β Ξ£π β π (πβπ) = if(π = 1 , (Οβπ), 0)) | ||
Theorem | dchrsum 26539* | An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character π is 0 if π is non-principal and Ο(π) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ 1 = (0gβπΊ) & β’ (π β π β π·) & β’ π΅ = (Baseβπ) β β’ (π β Ξ£π β π΅ (πβπ) = if(π = 1 , (Οβπ), 0)) | ||
Theorem | sumdchr2 26540* | Lemma for sumdchr 26542. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) & β’ π = (β€/nβ€βπ) & β’ 1 = (1rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β β) & β’ (π β π΄ β π΅) β β’ (π β Ξ£π₯ β π· (π₯βπ΄) = if(π΄ = 1 , (β―βπ·), 0)) | ||
Theorem | dchrhash 26541 | There are exactly Ο(π) Dirichlet characters modulo π. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) β β’ (π β β β (β―βπ·) = (Οβπ)) | ||
Theorem | sumdchr 26542* | An orthogonality relation for Dirichlet characters: the sum of π₯(π΄) for fixed π΄ and all π₯ is 0 if π΄ = 1 and Ο(π) otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) & β’ π = (β€/nβ€βπ) & β’ 1 = (1rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β β) & β’ (π β π΄ β π΅) β β’ (π β Ξ£π₯ β π· (π₯βπ΄) = if(π΄ = 1 , (Οβπ), 0)) | ||
Theorem | dchr2sum 26543* | An orthogonality relation for Dirichlet characters: the sum of π(π) Β· βπ(π) over all π is nonzero only when π = π. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ (π β π β π·) & β’ (π β π β π·) β β’ (π β Ξ£π β π΅ ((πβπ) Β· (ββ(πβπ))) = if(π = π, (Οβπ), 0)) | ||
Theorem | sum2dchr 26544* | An orthogonality relation for Dirichlet characters: the sum of π₯(π΄) for fixed π΄ and all π₯ is 0 if π΄ = 1 and Ο(π) otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π· = (BaseβπΊ) & β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ π = (Unitβπ) & β’ (π β π β β) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π) β β’ (π β Ξ£π₯ β π· ((π₯βπ΄) Β· (ββ(π₯βπΆ))) = if(π΄ = πΆ, (Οβπ), 0)) | ||
Theorem | bcctr 26545 | Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ (π β β0 β ((2 Β· π)Cπ) = ((!β(2 Β· π)) / ((!βπ) Β· (!βπ)))) | ||
Theorem | pcbcctr 26546* | Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ ((π β β β§ π β β) β (π pCnt ((2 Β· π)Cπ)) = Ξ£π β (1...(2 Β· π))((ββ((2 Β· π) / (πβπ))) β (2 Β· (ββ(π / (πβπ)))))) | ||
Theorem | bcmono 26547 | The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.) |
β’ ((π β β0 β§ π΅ β (β€β₯βπ΄) β§ π΅ β€ (π / 2)) β (πCπ΄) β€ (πCπ΅)) | ||
Theorem | bcmax 26548 | The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.) |
β’ ((π β β0 β§ πΎ β β€) β ((2 Β· π)CπΎ) β€ ((2 Β· π)Cπ)) | ||
Theorem | bcp1ctr 26549 | Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.) |
β’ (π β β0 β ((2 Β· (π + 1))C(π + 1)) = (((2 Β· π)Cπ) Β· (2 Β· (((2 Β· π) + 1) / (π + 1))))) | ||
Theorem | bclbnd 26550 | A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) |
β’ (π β (β€β₯β4) β ((4βπ) / π) < ((2 Β· π)Cπ)) | ||
Theorem | efexple 26551 | Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) |
β’ (((π΄ β β β§ 1 < π΄) β§ π β β€ β§ π΅ β β+) β ((π΄βπ) β€ π΅ β π β€ (ββ((logβπ΅) / (logβπ΄))))) | ||
Theorem | bpos1lem 26552* | Lemma for bpos1 26553. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ (βπ β β (π < π β§ π β€ (2 Β· π)) β π) & β’ (π β (β€β₯βπ) β π) & β’ π β β & β’ π΄ β β0 & β’ (π΄ Β· 2) = π΅ & β’ π΄ < π & β’ (π < π΅ β¨ π = π΅) β β’ (π β (β€β₯βπ΄) β π) | ||
Theorem | bpos1 26553* | Bertrand's postulate, checked numerically for π β€ 64, using the prime sequence 2, 3, 5, 7, 13, 23, 43, 83. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.) |
β’ ((π β β β§ π β€ ;64) β βπ β β (π < π β§ π β€ (2 Β· π))) | ||
Theorem | bposlem1 26554 | An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.) |
β’ ((π β β β§ π β β) β (πβ(π pCnt ((2 Β· π)Cπ))) β€ (2 Β· π)) | ||
Theorem | bposlem2 26555 | There are no odd primes in the range (2π / 3, π] dividing the π-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β 2 < π) & β’ (π β ((2 Β· π) / 3) < π) & β’ (π β π β€ π) β β’ (π β (π pCnt ((2 Β· π)Cπ)) = 0) | ||
Theorem | bposlem3 26556* | Lemma for bpos 26563. Since the binomial coefficient does not have any primes in the range (2π / 3, π] or (2π, +β) by bposlem2 26555 and prmfac1 16532, respectively, and it does not have any in the range (π, 2π] by hypothesis, the product of the primes up through 2π / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ (π β π β (β€β₯β5)) & β’ (π β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) & β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1)) & β’ πΎ = (ββ((2 Β· π) / 3)) β β’ (π β (seq1( Β· , πΉ)βπΎ) = ((2 Β· π)Cπ)) | ||
Theorem | bposlem4 26557* | Lemma for bpos 26563. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ (π β π β (β€β₯β5)) & β’ (π β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) & β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1)) & β’ πΎ = (ββ((2 Β· π) / 3)) & β’ π = (ββ(ββ(2 Β· π))) β β’ (π β π β (3...πΎ)) | ||
Theorem | bposlem5 26558* | Lemma for bpos 26563. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.) |
β’ (π β π β (β€β₯β5)) & β’ (π β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) & β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1)) & β’ πΎ = (ββ((2 Β· π) / 3)) & β’ π = (ββ(ββ(2 Β· π))) β β’ (π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)βπ(((ββ(2 Β· π)) / 3) + 2))) | ||
Theorem | bposlem6 26559* | Lemma for bpos 26563. By using the various bounds at our disposal, arrive at an inequality that is false for π large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.) |
β’ (π β π β (β€β₯β5)) & β’ (π β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) & β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1)) & β’ πΎ = (ββ((2 Β· π) / 3)) & β’ π = (ββ(ββ(2 Β· π))) β β’ (π β ((4βπ) / π) < (((2 Β· π)βπ(((ββ(2 Β· π)) / 3) + 2)) Β· (2βπ(((4 Β· π) / 3) β 5)))) | ||
Theorem | bposlem7 26560* | Lemma for bpos 26563. The function πΉ is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ πΉ = (π β β β¦ ((((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) + ((logβ2) / (ββ(2 Β· π))))) & β’ πΊ = (π₯ β β+ β¦ ((logβπ₯) / π₯)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (eβ2) β€ π΄) & β’ (π β (eβ2) β€ π΅) β β’ (π β (π΄ < π΅ β (πΉβπ΅) < (πΉβπ΄))) | ||
Theorem | bposlem8 26561 | Lemma for bpos 26563. Evaluate πΉ(64) and show it is less than log2. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ πΉ = (π β β β¦ ((((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) + ((logβ2) / (ββ(2 Β· π))))) & β’ πΊ = (π₯ β β+ β¦ ((logβπ₯) / π₯)) β β’ ((πΉβ;64) β β β§ (πΉβ;64) < (logβ2)) | ||
Theorem | bposlem9 26562* | Lemma for bpos 26563. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.) |
β’ πΉ = (π β β β¦ ((((ββ2) Β· (πΊβ(ββπ))) + ((9 / 4) Β· (πΊβ(π / 2)))) + ((logβ2) / (ββ(2 Β· π))))) & β’ πΊ = (π₯ β β+ β¦ ((logβπ₯) / π₯)) & β’ (π β π β β) & β’ (π β ;64 < π) & β’ (π β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) β β’ (π β π) | ||
Theorem | bpos 26563* | Bertrand's postulate: there is a prime between π and 2π for every positive integer π. 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.) |
β’ (π β β β βπ β β (π < π β§ π β€ (2 Β· π))) | ||
If the congruence ((π₯β2) mod π) = (π mod π) has a solution we say that π is a quadratic residue mod π. If the congruence has no solution we say that π is a quadratic nonresidue mod π, see definition in [ApostolNT] p. 178. The Legendre symbol (π /L π) is defined in a way that its value is 1 if π is a quadratic residue mod π and -1 if π is a quadratic nonresidue mod π (and 0 if π divides π), see lgsqr 26621. Originally, the Legendre symbol (π /L π) was defined for odd primes π only (and arbitrary integers π) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 26565 for the "Legendre symbol" /L is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol". | ||
Syntax | clgs 26564 | Extend class notation with the Legendre symbol function. |
class /L | ||
Definition | df-lgs 26565* | Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ /L = (π β β€, π β β€ β¦ if(π = 0, if((πβ2) = 1, 1, 0), (if((π < 0 β§ π < 0), -1, 1) Β· (seq1( Β· , (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π, 0, if((π mod 8) β {1, 7}, 1, -1)), ((((πβ((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)))β(absβπ))))) | ||
Theorem | zabsle1 26566 | {-1, 0, 1} is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.) |
β’ (π β β€ β (π β {-1, 0, 1} β (absβπ) β€ 1)) | ||
Theorem | lgslem1 26567 | When π is coprime to the prime π, πβ((π β 1) / 2) is equivalent mod π to 1 or -1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π β (β β {2}) β§ Β¬ π β₯ π΄) β (((π΄β((π β 1) / 2)) + 1) mod π) β {0, 2}) | ||
Theorem | lgslem2 26568 | The set π of all integers with absolute value at most 1 contains {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ π = {π₯ β β€ β£ (absβπ₯) β€ 1} β β’ (-1 β π β§ 0 β π β§ 1 β π) | ||
Theorem | lgslem3 26569* | The set π of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ π = {π₯ β β€ β£ (absβπ₯) β€ 1} β β’ ((π΄ β π β§ π΅ β π) β (π΄ Β· π΅) β π) | ||
Theorem | lgslem4 26570* | Lemma for lgsfcl2 26573. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.) |
β’ π = {π₯ β β€ β£ (absβπ₯) β€ 1} β β’ ((π΄ β β€ β§ π β (β β {2})) β ((((π΄β((π β 1) / 2)) + 1) mod π) β 1) β π) | ||
Theorem | lgsval 26571* | Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) = if(π = 0, if((π΄β2) = 1, 1, 0), (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· , πΉ)β(absβπ))))) | ||
Theorem | lgsfval 26572* | Value of the function πΉ which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) β β’ (π β β β (πΉβπ) = if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) | ||
Theorem | lgsfcl2 26573* | The function πΉ is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 26566). (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) & β’ π = {π₯ β β€ β£ (absβπ₯) β€ 1} β β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆπ) | ||
Theorem | lgscllem 26574* | The Legendre symbol is an element of π. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) & β’ π = {π₯ β β€ β£ (absβπ₯) β€ 1} β β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β π) | ||
Theorem | lgsfcl 26575* | Closure of the function πΉ which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) | ||
Theorem | lgsfle1 26576* | The function πΉ has magnitude less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) β β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β β) β (absβ(πΉβπ)) β€ 1) | ||
Theorem | lgsval2lem 26577* | Lemma for lgsval2 26583. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) | ||
Theorem | lgsval4lem 26578* | Lemma for lgsval4 26587. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))) | ||
Theorem | lgscl2 26579* | The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ π = {π₯ β β€ β£ (absβπ₯) β€ 1} β β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β π) | ||
Theorem | lgs0 26580 | The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (π΄ β β€ β (π΄ /L 0) = if((π΄β2) = 1, 1, 0)) | ||
Theorem | lgscl 26581 | The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β β€) | ||
Theorem | lgsle1 26582 | The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 26581 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π β β€) β (absβ(π΄ /L π)) β€ 1) | ||
Theorem | lgsval2 26583 | 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.) |
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) | ||
Theorem | lgs2 26584 | The Legendre symbol at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (π΄ β β€ β (π΄ /L 2) = if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1))) | ||
Theorem | lgsval3 26585 | The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π β (β β {2})) β (π΄ /L π) = ((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) | ||
Theorem | lgsvalmod 26586 | The Legendre symbol is equivalent to πβ((π β 1) / 2), mod π. This theorem is also called "Euler's criterion", see theorem 9.2 in [ApostolNT] p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr 26621. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π β (β β {2})) β ((π΄ /L π) mod π) = ((π΄β((π β 1) / 2)) mod π)) | ||
Theorem | lgsval4 26587* | Restate lgsval 26571 for nonzero π, where the function πΉ 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.) |
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· , πΉ)β(absβπ)))) | ||
Theorem | lgsfcl3 26588* | Closure of the function πΉ which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) | ||
Theorem | lgsval4a 26589* | Same as lgsval4 26587 for positive π. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) β β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = (seq1( Β· , πΉ)βπ)) | ||
Theorem | lgscl1 26590 | The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.) |
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β {-1, 0, 1}) | ||
Theorem | lgsneg 26591 | 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.) |
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L -π) = (if(π΄ < 0, -1, 1) Β· (π΄ /L π))) | ||
Theorem | lgsneg1 26592 | The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β0 β§ π β β€) β (π΄ /L -π) = (π΄ /L π)) | ||
Theorem | lgsmod 26593 | The Legendre (Jacobi) symbol is preserved under reduction mod π when π is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π β β β§ Β¬ 2 β₯ π) β ((π΄ mod π) /L π) = (π΄ /L π)) | ||
Theorem | lgsdilem 26594 | Lemma for lgsdi 26604 and lgsdir 26602: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ π β β€) β§ (π΄ β 0 β§ π΅ β 0)) β if((π < 0 β§ (π΄ Β· π΅) < 0), -1, 1) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· if((π < 0 β§ π΅ < 0), -1, 1))) | ||
Theorem | lgsdir2lem1 26595 | Lemma for lgsdir2 26600. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (((1 mod 8) = 1 β§ (-1 mod 8) = 7) β§ ((3 mod 8) = 3 β§ (-3 mod 8) = 5)) | ||
Theorem | lgsdir2lem2 26596 | Lemma for lgsdir2 26600. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (πΎ β β€ β§ 2 β₯ (πΎ + 1) β§ ((π΄ β β€ β§ Β¬ 2 β₯ π΄) β ((π΄ mod 8) β (0...πΎ) β (π΄ mod 8) β π))) & β’ π = (πΎ + 1) & β’ π = (π + 1) & β’ π β π β β’ (π β β€ β§ 2 β₯ (π + 1) β§ ((π΄ β β€ β§ Β¬ 2 β₯ π΄) β ((π΄ mod 8) β (0...π) β (π΄ mod 8) β π))) | ||
Theorem | lgsdir2lem3 26597 | Lemma for lgsdir2 26600. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ Β¬ 2 β₯ π΄) β (π΄ mod 8) β ({1, 7} βͺ {3, 5})) | ||
Theorem | lgsdir2lem4 26598 | Lemma for lgsdir2 26600. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (((π΄ β β€ β§ π΅ β β€) β§ (π΄ mod 8) β {1, 7}) β (((π΄ Β· π΅) mod 8) β {1, 7} β (π΅ mod 8) β {1, 7})) | ||
Theorem | lgsdir2lem5 26599 | Lemma for lgsdir2 26600. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (((π΄ β β€ β§ π΅ β β€) β§ ((π΄ mod 8) β {3, 5} β§ (π΅ mod 8) β {3, 5})) β ((π΄ Β· π΅) mod 8) β {1, 7}) | ||
Theorem | lgsdir2 26600 | The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ Β· π΅) /L 2) = ((π΄ /L 2) Β· (π΅ /L 2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |