Home | Metamath
Proof Explorer Theorem List (p. 267 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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lgsdirprm 26601 | The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β ((π΄ Β· π΅) /L π) = ((π΄ /L π) Β· (π΅ /L π))) | ||
Theorem | lgsdir 26602 | The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that π΄ and π΅ are odd positive integers). Together with lgsqr 26621 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.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ π β β€) β§ (π΄ β 0 β§ π΅ β 0)) β ((π΄ Β· π΅) /L π) = ((π΄ /L π) Β· (π΅ /L π))) | ||
Theorem | lgsdilem2 26603* | Lemma for lgsdi 26604. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ (π β π΄ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β 0) & β’ (π β π β 0) & β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) β β’ (π β (seq1( Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)β(absβ(π Β· π)))) | ||
Theorem | lgsdi 26604 | The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that π and π are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.) |
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π΄ /L (π Β· π)) = ((π΄ /L π) Β· (π΄ /L π))) | ||
Theorem | lgsne0 26605 | The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.) |
β’ ((π΄ β β€ β§ π β β€) β ((π΄ /L π) β 0 β (π΄ gcd π) = 1)) | ||
Theorem | lgsabs1 26606 | The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.) |
β’ ((π΄ β β€ β§ π β β€) β ((absβ(π΄ /L π)) = 1 β (π΄ gcd π) = 1)) | ||
Theorem | lgssq 26607 | The Legendre symbol at a square is equal to 1. Together with lgsmod 26593 this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.) (Revised by AV, 20-Jul-2021.) |
β’ (((π΄ β β€ β§ π΄ β 0) β§ π β β€ β§ (π΄ gcd π) = 1) β ((π΄β2) /L π) = 1) | ||
Theorem | lgssq2 26608 | The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄ gcd π) = 1) β (π΄ /L (πβ2)) = 1) | ||
Theorem | lgsprme0 26609 | The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in [ApostolNT] p. 179. (Contributed by AV, 20-Jul-2021.) |
β’ ((π΄ β β€ β§ π β β) β ((π΄ /L π) = 0 β (π΄ mod π) = 0)) | ||
Theorem | 1lgs 26610 | The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ (π β β€ β (1 /L π) = 1) | ||
Theorem | lgs1 26611 | The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ (π΄ β β€ β (π΄ /L 1) = 1) | ||
Theorem | lgsmodeq 26612 | The Legendre (Jacobi) symbol is preserved under reduction mod π when π is odd. Theorem 9.9(c) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ (π β β β§ Β¬ 2 β₯ π)) β ((π΄ mod π) = (π΅ mod π) β (π΄ /L π) = (π΅ /L π))) | ||
Theorem | lgsmulsqcoprm 26613 | The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.) |
β’ (((π΄ β β€ β§ π΄ β 0) β§ (π΅ β β€ β§ π΅ β 0) β§ (π β β€ β§ (π΄ gcd π) = 1)) β (((π΄β2) Β· π΅) /L π) = (π΅ /L π)) | ||
Theorem | lgsdirnn0 26614 | Variation on lgsdir 26602 valid for all π΄, π΅ but only for positive π. (The exact location of the failure of this law is for π΄ = 0, π΅ < 0, π = -1 in which case (0 /L -1) = 1 but (π΅ /L -1) = -1.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β ((π΄ Β· π΅) /L π) = ((π΄ /L π) Β· (π΅ /L π))) | ||
Theorem | lgsdinn0 26615 | Variation on lgsdi 26604 valid for all π, π but only for positive π΄. (The exact location of the failure of this law is for π΄ = -1, π = 0, and some π in which case (-1 /L 0) = 1 but (-1 /L π) = -1 when -1 is not a quadratic residue mod π.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ ((π΄ β β0 β§ π β β€ β§ π β β€) β (π΄ /L (π Β· π)) = ((π΄ /L π) Β· (π΄ /L π))) | ||
Theorem | lgsqrlem1 26616 | Lemma for lgsqr 26621. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (β€/nβ€βπ) & β’ π = (Poly1βπ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ) & β’ π = (eval1βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ) & β’ β = (-gβπ) & β’ 1 = (1rβπ) & β’ π = ((((π β 1) / 2) β π) β 1 ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β (β β {2})) & β’ (π β π΄ β β€) & β’ (π β ((π΄β((π β 1) / 2)) mod π) = (1 mod π)) β β’ (π β ((πβπ)β(πΏβπ΄)) = (0gβπ)) | ||
Theorem | lgsqrlem2 26617* | Lemma for lgsqr 26621. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (β€/nβ€βπ) & β’ π = (Poly1βπ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ) & β’ π = (eval1βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ) & β’ β = (-gβπ) & β’ 1 = (1rβπ) & β’ π = ((((π β 1) / 2) β π) β 1 ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β (β β {2})) & β’ πΊ = (π¦ β (1...((π β 1) / 2)) β¦ (πΏβ(π¦β2))) β β’ (π β πΊ:(1...((π β 1) / 2))β1-1β(β‘(πβπ) β {(0gβπ)})) | ||
Theorem | lgsqrlem3 26618* | Lemma for lgsqr 26621. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (β€/nβ€βπ) & β’ π = (Poly1βπ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ) & β’ π = (eval1βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ) & β’ β = (-gβπ) & β’ 1 = (1rβπ) & β’ π = ((((π β 1) / 2) β π) β 1 ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β (β β {2})) & β’ πΊ = (π¦ β (1...((π β 1) / 2)) β¦ (πΏβ(π¦β2))) & β’ (π β π΄ β β€) & β’ (π β (π΄ /L π) = 1) β β’ (π β (πΏβπ΄) β (β‘(πβπ) β {(0gβπ)})) | ||
Theorem | lgsqrlem4 26619* | Lemma for lgsqr 26621. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (β€/nβ€βπ) & β’ π = (Poly1βπ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ) & β’ π = (eval1βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ) & β’ β = (-gβπ) & β’ 1 = (1rβπ) & β’ π = ((((π β 1) / 2) β π) β 1 ) & β’ πΏ = (β€RHomβπ) & β’ (π β π β (β β {2})) & β’ πΊ = (π¦ β (1...((π β 1) / 2)) β¦ (πΏβ(π¦β2))) & β’ (π β π΄ β β€) & β’ (π β (π΄ /L π) = 1) β β’ (π β βπ₯ β β€ π β₯ ((π₯β2) β π΄)) | ||
Theorem | lgsqrlem5 26620* | Lemma for lgsqr 26621. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ ((π΄ β β€ β§ π β (β β {2}) β§ (π΄ /L π) = 1) β βπ₯ β β€ π β₯ ((π₯β2) β π΄)) | ||
Theorem | lgsqr 26621* | 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 26605) and the number is a quadratic residue mod π (it is -1 for nonresidues by the process of elimination from lgsabs1 26606). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ ((π΄ β β€ β§ π β (β β {2})) β ((π΄ /L π) = 1 β (Β¬ π β₯ π΄ β§ βπ₯ β β€ π β₯ ((π₯β2) β π΄)))) | ||
Theorem | lgsqrmod 26622* | If the Legendre symbol of an integer for an odd prime is 1, then the number is a quadratic residue mod π. (Contributed by AV, 20-Aug-2021.) |
β’ ((π΄ β β€ β§ π β (β β {2})) β ((π΄ /L π) = 1 β βπ₯ β β€ ((π₯β2) mod π) = (π΄ mod π))) | ||
Theorem | lgsqrmodndvds 26623* | If the Legendre symbol of an integer π΄ for an odd prime is 1, then the number is a quadratic residue mod π with a solution π₯ of the congruence (π₯β2)β‘π΄ (mod π) which is not divisible by the prime. (Contributed by AV, 20-Aug-2021.) (Proof shortened by AV, 18-Mar-2022.) |
β’ ((π΄ β β€ β§ π β (β β {2})) β ((π΄ /L π) = 1 β βπ₯ β β€ (((π₯β2) mod π) = (π΄ mod π) β§ Β¬ π β₯ π₯))) | ||
Theorem | lgsdchrval 26624* | The Legendre symbol function π(π) = (π /L π), where π is an odd positive number, is a Dirichlet character modulo π. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ πΏ = (β€RHomβπ) & β’ π = (π¦ β π΅ β¦ (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π)))) β β’ (((π β β β§ Β¬ 2 β₯ π) β§ π΄ β β€) β (πβ(πΏβπ΄)) = (π΄ /L π)) | ||
Theorem | lgsdchr 26625* | The Legendre symbol function π(π) = (π /L π), where π is an odd positive number, is a real Dirichlet character modulo π. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ πΊ = (DChrβπ) & β’ π = (β€/nβ€βπ) & β’ π· = (BaseβπΊ) & β’ π΅ = (Baseβπ) & β’ πΏ = (β€RHomβπ) & β’ π = (π¦ β π΅ β¦ (β©ββπ β β€ (π¦ = (πΏβπ) β§ β = (π /L π)))) β β’ ((π β β β§ Β¬ 2 β₯ π) β (π β π· β§ π:π΅βΆβ)) | ||
Gauss' Lemma is valid for any integer not dividing the given prime number. In the following, only the special case for 2 (not dividing any odd prime) is proven, see gausslemma2d 26644. The general case is still to prove. | ||
Theorem | gausslemma2dlem0a 26626 | Auxiliary lemma 1 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) β β’ (π β π β β) | ||
Theorem | gausslemma2dlem0b 26627 | Auxiliary lemma 2 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) β β’ (π β π» β β) | ||
Theorem | gausslemma2dlem0c 26628 | Auxiliary lemma 3 for gausslemma2d 26644. (Contributed by AV, 13-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) β β’ (π β ((!βπ») gcd π) = 1) | ||
Theorem | gausslemma2dlem0d 26629 | Auxiliary lemma 4 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π = (ββ(π / 4)) β β’ (π β π β β0) | ||
Theorem | gausslemma2dlem0e 26630 | Auxiliary lemma 5 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π = (ββ(π / 4)) β β’ (π β (π Β· 2) < (π / 2)) | ||
Theorem | gausslemma2dlem0f 26631 | Auxiliary lemma 6 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π = (ββ(π / 4)) & β’ π» = ((π β 1) / 2) β β’ (π β (π + 1) β€ π») | ||
Theorem | gausslemma2dlem0g 26632 | Auxiliary lemma 7 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π = (ββ(π / 4)) & β’ π» = ((π β 1) / 2) β β’ (π β π β€ π») | ||
Theorem | gausslemma2dlem0h 26633 | Auxiliary lemma 8 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π = (ββ(π / 4)) & β’ π» = ((π β 1) / 2) & β’ π = (π» β π) β β’ (π β π β β0) | ||
Theorem | gausslemma2dlem0i 26634 | Auxiliary lemma 9 for gausslemma2d 26644. (Contributed by AV, 14-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π = (ββ(π / 4)) & β’ π» = ((π β 1) / 2) & β’ π = (π» β π) β β’ (π β (((2 /L π) mod π) = ((-1βπ) mod π) β (2 /L π) = (-1βπ))) | ||
Theorem | gausslemma2dlem1a 26635* | Lemma for gausslemma2dlem1 26636. (Contributed by AV, 1-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) β β’ (π β ran π = (1...π»)) | ||
Theorem | gausslemma2dlem1 26636* | Lemma 1 for gausslemma2d 26644. (Contributed by AV, 5-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) β β’ (π β (!βπ») = βπ β (1...π»)(π βπ)) | ||
Theorem | gausslemma2dlem2 26637* | Lemma 2 for gausslemma2d 26644. (Contributed by AV, 4-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) β β’ (π β βπ β (1...π)(π βπ) = (π Β· 2)) | ||
Theorem | gausslemma2dlem3 26638* | Lemma 3 for gausslemma2d 26644. (Contributed by AV, 4-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) β β’ (π β βπ β ((π + 1)...π»)(π βπ) = (π β (π Β· 2))) | ||
Theorem | gausslemma2dlem4 26639* | Lemma 4 for gausslemma2d 26644. (Contributed by AV, 16-Jun-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) β β’ (π β (!βπ») = (βπ β (1...π)(π βπ) Β· βπ β ((π + 1)...π»)(π βπ))) | ||
Theorem | gausslemma2dlem5a 26640* | Lemma for gausslemma2dlem5 26641. (Contributed by AV, 8-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) β β’ (π β (βπ β ((π + 1)...π»)(π βπ) mod π) = (βπ β ((π + 1)...π»)(-1 Β· (π Β· 2)) mod π)) | ||
Theorem | gausslemma2dlem5 26641* | Lemma 5 for gausslemma2d 26644. (Contributed by AV, 9-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) & β’ π = (π» β π) β β’ (π β (βπ β ((π + 1)...π»)(π βπ) mod π) = (((-1βπ) Β· βπ β ((π + 1)...π»)(π Β· 2)) mod π)) | ||
Theorem | gausslemma2dlem6 26642* | Lemma 6 for gausslemma2d 26644. (Contributed by AV, 16-Jun-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) & β’ π = (π» β π) β β’ (π β ((!βπ») mod π) = ((((-1βπ) Β· (2βπ»)) Β· (!βπ»)) mod π)) | ||
Theorem | gausslemma2dlem7 26643* | Lemma 7 for gausslemma2d 26644. (Contributed by AV, 13-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) & β’ π = (π» β π) β β’ (π β (((-1βπ) Β· (2βπ»)) mod π) = 1) | ||
Theorem | gausslemma2d 26644* | Gauss' Lemma (see also theorem 9.6 in [ApostolNT] p. 182) for integer 2: Let p be an odd prime. Let S = {2, 4, 6, ..., p - 1}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021.) |
β’ (π β π β (β β {2})) & β’ π» = ((π β 1) / 2) & β’ π = (π₯ β (1...π») β¦ if((π₯ Β· 2) < (π / 2), (π₯ Β· 2), (π β (π₯ Β· 2)))) & β’ π = (ββ(π / 4)) & β’ π = (π» β π) β β’ (π β (2 /L π) = (-1βπ)) | ||
Theorem | lgseisenlem1 26645* | Lemma for lgseisen 26649. If π (π’) = (π Β· π’) mod π and π(π’) = (-1βπ (π’)) Β· π (π’), then for any even 1 β€ π’ β€ π β 1, π(π’) is also an even integer 1 β€ π(π’) β€ π β 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that π(π₯ / 2) = (-1βπ (π₯ / 2)) Β· π (π₯ / 2) / 2 is an integer between 1 and (π β 1) / 2. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π Β· (2 Β· π₯)) mod π) & β’ π = (π₯ β (1...((π β 1) / 2)) β¦ ((((-1βπ ) Β· π ) mod π) / 2)) β β’ (π β π:(1...((π β 1) / 2))βΆ(1...((π β 1) / 2))) | ||
Theorem | lgseisenlem2 26646* | Lemma for lgseisen 26649. The function π is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π Β· (2 Β· π₯)) mod π) & β’ π = (π₯ β (1...((π β 1) / 2)) β¦ ((((-1βπ ) Β· π ) mod π) / 2)) & β’ π = ((π Β· (2 Β· π¦)) mod π) β β’ (π β π:(1...((π β 1) / 2))β1-1-ontoβ(1...((π β 1) / 2))) | ||
Theorem | lgseisenlem3 26647* | Lemma for lgseisen 26649. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π Β· (2 Β· π₯)) mod π) & β’ π = (π₯ β (1...((π β 1) / 2)) β¦ ((((-1βπ ) Β· π ) mod π) / 2)) & β’ π = ((π Β· (2 Β· π¦)) mod π) & β’ π = (β€/nβ€βπ) & β’ πΊ = (mulGrpβπ) & β’ πΏ = (β€RHomβπ) β β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ ) Β· π)))) = (1rβπ)) | ||
Theorem | lgseisenlem4 26648* | Lemma for lgseisen 26649. The function π is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π Β· (2 Β· π₯)) mod π) & β’ π = (π₯ β (1...((π β 1) / 2)) β¦ ((((-1βπ ) Β· π ) mod π) / 2)) & β’ π = ((π Β· (2 Β· π¦)) mod π) & β’ π = (β€/nβ€βπ) & β’ πΊ = (mulGrpβπ) & β’ πΏ = (β€RHomβπ) β β’ (π β ((πβ((π β 1) / 2)) mod π) = ((-1βΞ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯)))) mod π)) | ||
Theorem | lgseisen 26649* | Eisenstein's lemma, an expression for (π /L π) when π, π are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) β β’ (π β (π /L π) = (-1βΞ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯))))) | ||
Theorem | lgsquadlem1 26650* | Lemma for lgsquad 26653. Count the members of π with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π β 1) / 2) & β’ π = ((π β 1) / 2) & β’ π = {β¨π₯, π¦β© β£ ((π₯ β (1...π) β§ π¦ β (1...π)) β§ (π¦ Β· π) < (π₯ Β· π))} β β’ (π β (-1βΞ£π’ β (((ββ(π / 2)) + 1)...π)(ββ((π / π) Β· (2 Β· π’)))) = (-1β(β―β{π§ β π β£ Β¬ 2 β₯ (1st βπ§)}))) | ||
Theorem | lgsquadlem2 26651* | Lemma for lgsquad 26653. Count the members of π with even coordinates, and combine with lgsquadlem1 26650 to get the total count of lattice points in π (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π β 1) / 2) & β’ π = ((π β 1) / 2) & β’ π = {β¨π₯, π¦β© β£ ((π₯ β (1...π) β§ π¦ β (1...π)) β§ (π¦ Β· π) < (π₯ Β· π))} β β’ (π β (π /L π) = (-1β(β―βπ))) | ||
Theorem | lgsquadlem3 26652* | Lemma for lgsquad 26653. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π β π β (β β {2})) & β’ (π β π β (β β {2})) & β’ (π β π β π) & β’ π = ((π β 1) / 2) & β’ π = ((π β 1) / 2) & β’ π = {β¨π₯, π¦β© β£ ((π₯ β (1...π) β§ π¦ β (1...π)) β§ (π¦ Β· π) < (π₯ Β· π))} β β’ (π β ((π /L π) Β· (π /L π)) = (-1β(π Β· π))) | ||
Theorem | lgsquad 26653 | The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] p. 185. If π and π are distinct odd primes, then the product of the Legendre symbols (π /L π) and (π /L π) is the parity of ((π β 1) / 2) Β· ((π β 1) / 2). This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity. This is Metamath 100 proof #7. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ ((π β (β β {2}) β§ π β (β β {2}) β§ π β π) β ((π /L π) Β· (π /L π)) = (-1β(((π β 1) / 2) Β· ((π β 1) / 2)))) | ||
Theorem | lgsquad2lem1 26654 | Lemma for lgsquad2 26656. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) & β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) & β’ (π β (π gcd π) = 1) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄ Β· π΅) = π) & β’ (π β ((π΄ /L π) Β· (π /L π΄)) = (-1β(((π΄ β 1) / 2) Β· ((π β 1) / 2)))) & β’ (π β ((π΅ /L π) Β· (π /L π΅)) = (-1β(((π΅ β 1) / 2) Β· ((π β 1) / 2)))) β β’ (π β ((π /L π) Β· (π /L π)) = (-1β(((π β 1) / 2) Β· ((π β 1) / 2)))) | ||
Theorem | lgsquad2lem2 26655* | Lemma for lgsquad2 26656. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) & β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) & β’ (π β (π gcd π) = 1) & β’ ((π β§ (π β (β β {2}) β§ (π gcd π) = 1)) β ((π /L π) Β· (π /L π)) = (-1β(((π β 1) / 2) Β· ((π β 1) / 2)))) & β’ (π β βπ₯ β (1...π)((π₯ gcd (2 Β· π)) = 1 β ((π₯ /L π) Β· (π /L π₯)) = (-1β(((π₯ β 1) / 2) Β· ((π β 1) / 2))))) β β’ (π β ((π /L π) Β· (π /L π)) = (-1β(((π β 1) / 2) Β· ((π β 1) / 2)))) | ||
Theorem | lgsquad2 26656 | Extend lgsquad 26653 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) & β’ (π β π β β) & β’ (π β Β¬ 2 β₯ π) & β’ (π β (π gcd π) = 1) β β’ (π β ((π /L π) Β· (π /L π)) = (-1β(((π β 1) / 2) Β· ((π β 1) / 2)))) | ||
Theorem | lgsquad3 26657 | Extend lgsquad2 26656 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (((π β β β§ Β¬ 2 β₯ π) β§ (π β β β§ Β¬ 2 β₯ π)) β (π /L π) = ((-1β(((π β 1) / 2) Β· ((π β 1) / 2))) Β· (π /L π))) | ||
Theorem | m1lgs 26658 | The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime π iff πβ‘1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (π β (β β {2}) β ((-1 /L π) = 1 β (π mod 4) = 1)) | ||
Theorem | 2lgslem1a1 26659* | Lemma 1 for 2lgslem1a 26661. (Contributed by AV, 16-Jun-2021.) |
β’ ((π β β β§ Β¬ 2 β₯ π) β βπ β (1...((π β 1) / 2))(π Β· 2) = ((π Β· 2) mod π)) | ||
Theorem | 2lgslem1a2 26660 | Lemma 2 for 2lgslem1a 26661. (Contributed by AV, 18-Jun-2021.) |
β’ ((π β β€ β§ πΌ β β€) β ((ββ(π / 4)) < πΌ β (π / 2) < (πΌ Β· 2))) | ||
Theorem | 2lgslem1a 26661* | Lemma 1 for 2lgslem1 26664. (Contributed by AV, 18-Jun-2021.) |
β’ ((π β β β§ Β¬ 2 β₯ π) β {π₯ β β€ β£ βπ β (1...((π β 1) / 2))(π₯ = (π Β· 2) β§ (π / 2) < (π₯ mod π))} = {π₯ β β€ β£ βπ β (((ββ(π / 4)) + 1)...((π β 1) / 2))π₯ = (π Β· 2)}) | ||
Theorem | 2lgslem1b 26662* | Lemma 2 for 2lgslem1 26664. (Contributed by AV, 18-Jun-2021.) |
β’ πΌ = (π΄...π΅) & β’ πΉ = (π β πΌ β¦ (π Β· 2)) β β’ πΉ:πΌβ1-1-ontoβ{π₯ β β€ β£ βπ β πΌ π₯ = (π Β· 2)} | ||
Theorem | 2lgslem1c 26663 | Lemma 3 for 2lgslem1 26664. (Contributed by AV, 19-Jun-2021.) |
β’ ((π β β β§ Β¬ 2 β₯ π) β (ββ(π / 4)) β€ ((π β 1) / 2)) | ||
Theorem | 2lgslem1 26664* | Lemma 1 for 2lgs 26677. (Contributed by AV, 19-Jun-2021.) |
β’ ((π β β β§ Β¬ 2 β₯ π) β (β―β{π₯ β β€ β£ βπ β (1...((π β 1) / 2))(π₯ = (π Β· 2) β§ (π / 2) < (π₯ mod π))}) = (((π β 1) / 2) β (ββ(π / 4)))) | ||
Theorem | 2lgslem2 26665 | Lemma 2 for 2lgs 26677. (Contributed by AV, 20-Jun-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((π β β β§ Β¬ 2 β₯ π) β π β β€) | ||
Theorem | 2lgslem3a 26666 | Lemma for 2lgslem3a1 26670. (Contributed by AV, 14-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((πΎ β β0 β§ π = ((8 Β· πΎ) + 1)) β π = (2 Β· πΎ)) | ||
Theorem | 2lgslem3b 26667 | Lemma for 2lgslem3b1 26671. (Contributed by AV, 16-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((πΎ β β0 β§ π = ((8 Β· πΎ) + 3)) β π = ((2 Β· πΎ) + 1)) | ||
Theorem | 2lgslem3c 26668 | Lemma for 2lgslem3c1 26672. (Contributed by AV, 16-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((πΎ β β0 β§ π = ((8 Β· πΎ) + 5)) β π = ((2 Β· πΎ) + 1)) | ||
Theorem | 2lgslem3d 26669 | Lemma for 2lgslem3d1 26673. (Contributed by AV, 16-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((πΎ β β0 β§ π = ((8 Β· πΎ) + 7)) β π = ((2 Β· πΎ) + 2)) | ||
Theorem | 2lgslem3a1 26670 | Lemma 1 for 2lgslem3 26674. (Contributed by AV, 15-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((π β β β§ (π mod 8) = 1) β (π mod 2) = 0) | ||
Theorem | 2lgslem3b1 26671 | Lemma 2 for 2lgslem3 26674. (Contributed by AV, 16-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((π β β β§ (π mod 8) = 3) β (π mod 2) = 1) | ||
Theorem | 2lgslem3c1 26672 | Lemma 3 for 2lgslem3 26674. (Contributed by AV, 16-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((π β β β§ (π mod 8) = 5) β (π mod 2) = 1) | ||
Theorem | 2lgslem3d1 26673 | Lemma 4 for 2lgslem3 26674. (Contributed by AV, 15-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((π β β β§ (π mod 8) = 7) β (π mod 2) = 0) | ||
Theorem | 2lgslem3 26674 | Lemma 3 for 2lgs 26677. (Contributed by AV, 16-Jul-2021.) |
β’ π = (((π β 1) / 2) β (ββ(π / 4))) β β’ ((π β β β§ Β¬ 2 β₯ π) β (π mod 2) = if((π mod 8) β {1, 7}, 0, 1)) | ||
Theorem | 2lgs2 26675 | The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.) |
β’ (2 /L 2) = 0 | ||
Theorem | 2lgslem4 26676 | Lemma 4 for 2lgs 26677: special case of 2lgs 26677 for π = 2. (Contributed by AV, 20-Jun-2021.) |
β’ ((2 /L 2) = 1 β (2 mod 8) β {1, 7}) | ||
Theorem | 2lgs 26677 | The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime π iff πβ‘Β±1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of (π /L 2) (lgs2 26584) to some degree, by demanding that reciprocity extend to the case π = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.) |
β’ (π β β β ((2 /L π) = 1 β (π mod 8) β {1, 7})) | ||
Theorem | 2lgsoddprmlem1 26678 | Lemma 1 for 2lgsoddprm 26686. (Contributed by AV, 19-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π = ((8 Β· π΄) + π΅)) β (((πβ2) β 1) / 8) = (((8 Β· (π΄β2)) + (2 Β· (π΄ Β· π΅))) + (((π΅β2) β 1) / 8))) | ||
Theorem | 2lgsoddprmlem2 26679 | Lemma 2 for 2lgsoddprm 26686. (Contributed by AV, 19-Jul-2021.) |
β’ ((π β β€ β§ Β¬ 2 β₯ π β§ π = (π mod 8)) β (2 β₯ (((πβ2) β 1) / 8) β 2 β₯ (((π β2) β 1) / 8))) | ||
Theorem | 2lgsoddprmlem3a 26680 | Lemma 1 for 2lgsoddprmlem3 26684. (Contributed by AV, 20-Jul-2021.) |
β’ (((1β2) β 1) / 8) = 0 | ||
Theorem | 2lgsoddprmlem3b 26681 | Lemma 2 for 2lgsoddprmlem3 26684. (Contributed by AV, 20-Jul-2021.) |
β’ (((3β2) β 1) / 8) = 1 | ||
Theorem | 2lgsoddprmlem3c 26682 | Lemma 3 for 2lgsoddprmlem3 26684. (Contributed by AV, 20-Jul-2021.) |
β’ (((5β2) β 1) / 8) = 3 | ||
Theorem | 2lgsoddprmlem3d 26683 | Lemma 4 for 2lgsoddprmlem3 26684. (Contributed by AV, 20-Jul-2021.) |
β’ (((7β2) β 1) / 8) = (2 Β· 3) | ||
Theorem | 2lgsoddprmlem3 26684 | Lemma 3 for 2lgsoddprm 26686. (Contributed by AV, 20-Jul-2021.) |
β’ ((π β β€ β§ Β¬ 2 β₯ π β§ π = (π mod 8)) β (2 β₯ (((π β2) β 1) / 8) β π β {1, 7})) | ||
Theorem | 2lgsoddprmlem4 26685 | Lemma 4 for 2lgsoddprm 26686. (Contributed by AV, 20-Jul-2021.) |
β’ ((π β β€ β§ Β¬ 2 β₯ π) β (2 β₯ (((πβ2) β 1) / 8) β (π mod 8) β {1, 7})) | ||
Theorem | 2lgsoddprm 26686 | The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in [ApostolNT] p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ((2 /L π) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.) |
β’ (π β (β β {2}) β (2 /L π) = (-1β(((πβ2) β 1) / 8))) | ||
Theorem | 2sqlem1 26687* | Lemma for 2sq 26700. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) β β’ (π΄ β π β βπ₯ β β€[i] π΄ = ((absβπ₯)β2)) | ||
Theorem | 2sqlem2 26688* | Lemma for 2sq 26700. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) β β’ (π΄ β π β βπ₯ β β€ βπ¦ β β€ π΄ = ((π₯β2) + (π¦β2))) | ||
Theorem | mul2sq 26689 | Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) β β’ ((π΄ β π β§ π΅ β π) β (π΄ Β· π΅) β π) | ||
Theorem | 2sqlem3 26690 | Lemma for 2sqlem5 26692. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β€) & β’ (π β π· β β€) & β’ (π β (π Β· π) = ((π΄β2) + (π΅β2))) & β’ (π β π = ((πΆβ2) + (π·β2))) & β’ (π β π β₯ ((πΆ Β· π΅) + (π΄ Β· π·))) β β’ (π β π β π) | ||
Theorem | 2sqlem4 26691 | Lemma for 2sqlem5 26692. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β€) & β’ (π β π· β β€) & β’ (π β (π Β· π) = ((π΄β2) + (π΅β2))) & β’ (π β π = ((πΆβ2) + (π·β2))) β β’ (π β π β π) | ||
Theorem | 2sqlem5 26692 | Lemma for 2sq 26700. If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) β π) & β’ (π β π β π) β β’ (π β π β π) | ||
Theorem | 2sqlem6 26693* | Lemma for 2sq 26700. If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β βπ β β (π β₯ π΅ β π β π)) & β’ (π β (π΄ Β· π΅) β π) β β’ (π β π΄ β π) | ||
Theorem | 2sqlem7 26694* | Lemma for 2sq 26700. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ π = {π§ β£ βπ₯ β β€ βπ¦ β β€ ((π₯ gcd π¦) = 1 β§ π§ = ((π₯β2) + (π¦β2)))} β β’ π β (π β© β) | ||
Theorem | 2sqlem8a 26695* | Lemma for 2sqlem8 26696. (Contributed by Mario Carneiro, 4-Jun-2016.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ π = {π§ β£ βπ₯ β β€ βπ¦ β β€ ((π₯ gcd π¦) = 1 β§ π§ = ((π₯β2) + (π¦β2)))} & β’ (π β βπ β (1...(π β 1))βπ β π (π β₯ π β π β π)) & β’ (π β π β₯ π) & β’ (π β π β β) & β’ (π β π β (β€β₯β2)) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β (π΄ gcd π΅) = 1) & β’ (π β π = ((π΄β2) + (π΅β2))) & β’ πΆ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ π· = (((π΅ + (π / 2)) mod π) β (π / 2)) β β’ (π β (πΆ gcd π·) β β) | ||
Theorem | 2sqlem8 26696* | Lemma for 2sq 26700. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ π = {π§ β£ βπ₯ β β€ βπ¦ β β€ ((π₯ gcd π¦) = 1 β§ π§ = ((π₯β2) + (π¦β2)))} & β’ (π β βπ β (1...(π β 1))βπ β π (π β₯ π β π β π)) & β’ (π β π β₯ π) & β’ (π β π β β) & β’ (π β π β (β€β₯β2)) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β (π΄ gcd π΅) = 1) & β’ (π β π = ((π΄β2) + (π΅β2))) & β’ πΆ = (((π΄ + (π / 2)) mod π) β (π / 2)) & β’ π· = (((π΅ + (π / 2)) mod π) β (π / 2)) & β’ πΈ = (πΆ / (πΆ gcd π·)) & β’ πΉ = (π· / (πΆ gcd π·)) β β’ (π β π β π) | ||
Theorem | 2sqlem9 26697* | Lemma for 2sq 26700. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ π = {π§ β£ βπ₯ β β€ βπ¦ β β€ ((π₯ gcd π¦) = 1 β§ π§ = ((π₯β2) + (π¦β2)))} & β’ (π β βπ β (1...(π β 1))βπ β π (π β₯ π β π β π)) & β’ (π β π β₯ π) & β’ (π β π β β) & β’ (π β π β π) β β’ (π β π β π) | ||
Theorem | 2sqlem10 26698* | Lemma for 2sq 26700. Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ π = {π§ β£ βπ₯ β β€ βπ¦ β β€ ((π₯ gcd π¦) = 1 β§ π§ = ((π₯β2) + (π¦β2)))} β β’ ((π΄ β π β§ π΅ β β β§ π΅ β₯ π΄) β π΅ β π) | ||
Theorem | 2sqlem11 26699* | Lemma for 2sq 26700. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ π = ran (π€ β β€[i] β¦ ((absβπ€)β2)) & β’ π = {π§ β£ βπ₯ β β€ βπ¦ β β€ ((π₯ gcd π¦) = 1 β§ π§ = ((π₯β2) + (π¦β2)))} β β’ ((π β β β§ (π mod 4) = 1) β π β π) | ||
Theorem | 2sq 26700* | All primes of the form 4π + 1 are sums of two squares. This is Metamath 100 proof #20. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ ((π β β β§ (π mod 4) = 1) β βπ₯ β β€ βπ¦ β β€ π = ((π₯β2) + (π¦β2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |