HomeTheorem List (p. 252 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 252 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lgseisenlem2 25101* |
Lemma for lgseisen 25104. The function  is an injection (and hence
a bijection by the pigeonhole principle). (Contributed by Mario
Carneiro, 17-Jun-2015.)
|
      
![\](setminus.gif "\"){kind=small}           
   
     
| ||
| Theorem | lgseisenlem3 25102* | Lemma for lgseisen 25104. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.) |
ℤ/nℤ  mulGrp   RHom  g
 | ||
| Theorem | lgseisenlem4 25103* |
Lemma for lgseisen 25104. 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.)
|
ℤ/nℤ mulGrp RHom
| ||
| Theorem | lgseisen 25104* |
Eisenstein's lemma, an expression for  when  are
distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.)
|
|
| ||
| Theorem | lgsquadlem1 25105* |
Lemma for lgsquad 25108. Count the members of with odd coordinates.
(Contributed by Mario Carneiro, 19-Jun-2015.)
|
    ![/\](wedge.gif "/\"){kind=small}
        | ||
| Theorem | lgsquadlem2 25106* |
Lemma for lgsquad 25108. Count the members of with even coordinates,
and combine with lgsquadlem1 25105 to get the total count of lattice
points
in (up to
parity). (Contributed by Mario Carneiro,
18-Jun-2015.)
|
|
| ||
| Theorem | lgsquadlem3 25107* | Lemma for lgsquad 25108. (Contributed by Mario Carneiro, 18-Jun-2015.) |
|
| ||
| Theorem | lgsquad 25108 |
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 and is the parity of
. 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.)
|
|
| ||
| Theorem | lgsquad2lem1 25109 | Lemma for lgsquad2 25111. (Contributed by Mario Carneiro, 19-Jun-2015.) |
  
| ||
| Theorem | lgsquad2lem2 25110* | Lemma for lgsquad2 25111. (Contributed by Mario Carneiro, 19-Jun-2015.) |
   
| ||
| Theorem | lgsquad2 25111 | Extend lgsquad 25108 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.) |
|
| ||
| Theorem | lgsquad3 25112 | Extend lgsquad2 25111 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.) |
|
| ||
| Theorem | m1lgs 25113 |
The first supplement to the law of quadratic reciprocity. Negative one is
a square mod an odd prime iff  (mod  ). See first
case of theorem 9.4 in [ApostolNT] p.
181. (Contributed by Mario
Carneiro, 19-Jun-2015.)
|
|
| ||
| Theorem | 2lgslem1a1 25114* | Lemma 1 for 2lgslem1a 25116. (Contributed by AV, 16-Jun-2021.) |
| ||
| Theorem | 2lgslem1a2 25115 | Lemma 2 for 2lgslem1a 25116. (Contributed by AV, 18-Jun-2021.) |
 | ||
| Theorem | 2lgslem1a 25116* | Lemma 1 for 2lgslem1 25119. (Contributed by AV, 18-Jun-2021.) |
| ||
| Theorem | 2lgslem1b 25117* | Lemma 2 for 2lgslem1 25119. (Contributed by AV, 18-Jun-2021.) |
 
| ||
| Theorem | 2lgslem1c 25118 | Lemma 3 for 2lgslem1 25119. (Contributed by AV, 19-Jun-2021.) |
| ||
| Theorem | 2lgslem1 25119* | Lemma 1 for 2lgs 25132. (Contributed by AV, 19-Jun-2021.) |
|
| ||
| Theorem | 2lgslem2 25120 | Lemma 2 for 2lgs 25132. (Contributed by AV, 20-Jun-2021.) |
|
| ||
| Theorem | 2lgslem3a 25121 | Lemma for 2lgslem3a1 25125. (Contributed by AV, 14-Jul-2021.) |
   | ||
| Theorem | 2lgslem3b 25122 | Lemma for 2lgslem3b1 25126. (Contributed by AV, 16-Jul-2021.) |
 | ||
| Theorem | 2lgslem3c 25123 | Lemma for 2lgslem3c1 25127. (Contributed by AV, 16-Jul-2021.) |
 | ||
| Theorem | 2lgslem3d 25124 | Lemma for 2lgslem3d1 25128. (Contributed by AV, 16-Jul-2021.) |
 | ||
| Theorem | 2lgslem3a1 25125 | Lemma 1 for 2lgslem3 25129. (Contributed by AV, 15-Jul-2021.) |
 | ||
| Theorem | 2lgslem3b1 25126 | Lemma 2 for 2lgslem3 25129. (Contributed by AV, 16-Jul-2021.) |
|
| ||
| Theorem | 2lgslem3c1 25127 | Lemma 3 for 2lgslem3 25129. (Contributed by AV, 16-Jul-2021.) |
|
| ||
| Theorem | 2lgslem3d1 25128 | Lemma 4 for 2lgslem3 25129. (Contributed by AV, 15-Jul-2021.) |
|
| ||
| Theorem | 2lgslem3 25129 | Lemma 3 for 2lgs 25132. (Contributed by AV, 16-Jul-2021.) |
 | ||
| Theorem | 2lgs2 25130 |
The Legendre symbol for
at is . (Contributed by AV,
20-Jun-2021.)
|
| | ||
| Theorem | 2lgslem4 25131 |
Lemma 4 for 2lgs 25132: special case of 2lgs 25132
for . (Contributed
by AV, 20-Jun-2021.)
|
| | ||
| Theorem | 2lgs 25132 |
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
 (mod ), see
first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies
our definition of (lgs2 25039) to some degree, by demanding
that reciprocity extend to the case . (Proposed
by Mario
Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.)
|
| | ||
| Theorem | 2lgsoddprmlem1 25133 | Lemma 1 for 2lgsoddprm 25141. (Contributed by AV, 19-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem2 25134 | Lemma 2 for 2lgsoddprm 25141. (Contributed by AV, 19-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem3a 25135 | Lemma 1 for 2lgsoddprmlem3 25139. (Contributed by AV, 20-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem3b 25136 | Lemma 2 for 2lgsoddprmlem3 25139. (Contributed by AV, 20-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem3c 25137 | Lemma 3 for 2lgsoddprmlem3 25139. (Contributed by AV, 20-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem3d 25138 | Lemma 4 for 2lgsoddprmlem3 25139. (Contributed by AV, 20-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem3 25139 | Lemma 3 for 2lgsoddprm 25141. (Contributed by AV, 20-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprmlem4 25140 | Lemma 4 for 2lgsoddprm 25141. (Contributed by AV, 20-Jul-2021.) |
|
| ||
| Theorem | 2lgsoddprm 25141 |
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
at an odd prime is minus one to the power of the
square of the odd prime minus one divided by eight ( =
-1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.)
|
|
| ||
| Theorem | 2sqlem1 25142* | Lemma for 2sq 25155. (Contributed by Mario Carneiro, 19-Jun-2015.) |
 
  ![]](rbrack.gif "]"){kind=small} 
| ||
| Theorem | 2sqlem2 25143* | Lemma for 2sq 25155. (Contributed by Mario Carneiro, 19-Jun-2015.) |
|
| ||
| Theorem | mul2sq 25144 | 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.) |
|
| ||
| Theorem | 2sqlem3 25145 | Lemma for 2sqlem5 25147. (Contributed by Mario Carneiro, 20-Jun-2015.) |
 
| ||
| Theorem | 2sqlem4 25146 | Lemma for 2sqlem5 25147. (Contributed by Mario Carneiro, 20-Jun-2015.) |
|
| ||
| Theorem | 2sqlem5 25147 | Lemma for 2sq 25155. 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.) |
|
| ||
| Theorem | 2sqlem6 25148* | Lemma for 2sq 25155. 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.) |
 | ||
| Theorem | 2sqlem7 25149* | Lemma for 2sq 25155. (Contributed by Mario Carneiro, 19-Jun-2015.) |
  | ||
| Theorem | 2sqlem8a 25150* | Lemma for 2sqlem8 25151. (Contributed by Mario Carneiro, 4-Jun-2016.) |
 
| ||
| Theorem | 2sqlem8 25151* | Lemma for 2sq 25155. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ||
| Theorem | 2sqlem9 25152* | Lemma for 2sq 25155. (Contributed by Mario Carneiro, 19-Jun-2015.) |
|
| ||
| Theorem | 2sqlem10 25153* | Lemma for 2sq 25155. 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.) |
|
| ||
| Theorem | 2sqlem11 25154* | Lemma for 2sq 25155. (Contributed by Mario Carneiro, 19-Jun-2015.) |
|
| ||
| Theorem | 2sq 25155* |
All primes of the form are sums of two squares. This is
Metamath 100 proof #20. (Contributed by Mario Carneiro,
20-Jun-2015.)
|
|
| ||
| Theorem | 2sqblem 25156 | The converse to 2sq 25155. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ||
| Theorem | 2sqb 25157* | The converse to 2sq 25155. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ||
| Theorem | chebbnd1lem1 25158 |
Lemma for chebbnd1 25161: show a lower bound on π at even
integers using similar techniques to those used to prove bpos 25018. (Note
that the expression is actually equal to , but proving
that is not necessary for the proof, and it's too much work.) The key
to the proof is bposlem1 25009, which shows that each term in the expansion
 
 is at most
, so
that the sum really only has nonzero elements up to , and
since each term is at most , after taking logs we get
the
inequality π 
, and bclbnd 25005 finishes the proof.
(Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario
Carneiro, 15-Apr-2016.)
|
| π | ||
| Theorem | chebbnd1lem2 25159 |
Lemma for chebbnd1 25161: Show that does not change too
much between
and . (Contributed by Mario
Carneiro, 22-Sep-2014.)
|
| ||
| Theorem | chebbnd1lem3 25160 |
Lemma for chebbnd1 25161: get a lower bound on
π that is independent of .
(Contributed by Mario Carneiro, 21-Sep-2014.)
|
π
| ||
| Theorem | chebbnd1 25161 |
The Chebyshev bound: The function π is eventually
lower
bounded by a positive constant times . Alternatively
stated, the function π is eventually
bounded. (Contributed by Mario Carneiro, 22-Sep-2014.)
|
 π  | ||
| Theorem | chtppilimlem1 25162 | Lemma for chtppilim 25164. (Contributed by Mario Carneiro, 22-Sep-2014.) |
 π π  | ||
| Theorem | chtppilimlem2 25163* | Lemma for chtppilim 25164. (Contributed by Mario Carneiro, 22-Sep-2014.) |
|
π | ||
| Theorem | chtppilim 25164 |
The function
is asymptotic to π, so it
is sufficient to prove   to establish
the PNT.
(Contributed by Mario Carneiro, 22-Sep-2014.)
|
|
π | ||
| Theorem | chto1ub 25165 |
The function
is upper bounded by a linear term. Corollary of
chtub 24937. (Contributed by Mario Carneiro,
22-Sep-2014.)
|
| | ||
| Theorem | chebbnd2 25166 |
The Chebyshev bound, part 2: The function π is eventually
upper bounded by a positive constant times .
Alternatively stated, the function π is
eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.)
|
|
π
| ||
| Theorem | chto1lb 25167 |
The function
is lower bounded by a linear term. Corollary of
chebbnd1 25161. (Contributed by Mario Carneiro,
8-Apr-2016.)
|
|
| ||
| Theorem | chpchtlim 25168 |
The ψ and functions are asymptotic to each other, so is
sufficient to prove either or
ψ to establish the PNT. (Contributed by Mario
Carneiro, 8-Apr-2016.)
|
|
ψ | ||
| Theorem | chpo1ub 25169 | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.) |
| ψ | ||
| Theorem | chpo1ubb 25170* | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.) |
 ψ
| ||
| Theorem | vmadivsum 25171* |
The sum of the von Mangoldt function over  is asymptotic to
. Equation 9.2.13 of [Shapiro], p. 331. (Contributed
by Mario Carneiro, 16-Apr-2016.)
|
| Λ | ||
| Theorem | vmadivsumb 25172* | Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.) |
| Λ | ||
| Theorem | rplogsumlem1 25173* | Lemma for rplogsum 25216. (Contributed by Mario Carneiro, 2-May-2016.) |
|
| ||
| Theorem | rplogsumlem2 25174* | Lemma for rplogsum 25216. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.) |
|
Λ | ||
| Theorem | dchrisum0lem1a 25175 | Lemma for dchrisum0lem1 25205. (Contributed by Mario Carneiro, 7-Jun-2016.) |
|
| ||
| Theorem | rpvmasumlem 25176* |
Lemma for rpvmasum 25215. Calculate the "trivial case"
estimate
 Λ , where
is the principal Dirichlet character. Equation 9.4.7 of
[Shapiro], p. 376. (Contributed by
Mario Carneiro, 2-May-2016.)
|
 ℤ/nℤ RHom DChr  
Λ | ||
| Theorem | dchrisumlema 25177* | Lemma for dchrisum 25181. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
ℤ/nℤ RHom DChr
 ![]_](_urbrack.gif "]_"){kind=small}
| ||
| Theorem | dchrisumlem1 25178* | Lemma for dchrisum 25181. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
ℤ/nℤ RHom DChr
..^ ..^
..^
| ||
| Theorem | dchrisumlem2 25179* | Lemma for dchrisum 25181. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
ℤ/nℤ RHom DChr
..^ ..^
 | ||
| Theorem | dchrisumlem3 25180* | Lemma for dchrisum 25181. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
ℤ/nℤ RHom DChr
..^ ..^
| ||
| Theorem | dchrisum 25181* |
If is a positive decreasing
function approaching zero, then the infinite sum
is convergent, with the
partial sum
within  of the
limit  .
Lemma 9.4.1 of [Shapiro], p. 377.
(Contributed by
Mario Carneiro, 2-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrmusumlema 25182* |
Lemma for dchrmusum 25213 and dchrisumn0 25210. Apply dchrisum 25181 for the
function . (Contributed by Mario Carneiro,
4-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrmusum2 25183* |
The sum of the Möbius function multiplied by a non-principal
Dirichlet character, divided by , is bounded, provided that
. Lemma 9.4.2 of [Shapiro], p. 380. (Contributed by
Mario Carneiro, 4-May-2016.)
|
ℤ/nℤ RHom DChr
 
| ||
| Theorem | dchrvmasumlem1 25184* | An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 3-May-2016.) |
| ℤ/nℤ RHom DChr Λ
| ||
| Theorem | dchrvmasum2lem 25185* |
Give an expression for remarkably
similar to
Λ given in
dchrvmasumlem1 25184. Part of Lemma 9.4.3 of [Shapiro], p. 380.
(Contributed by Mario Carneiro, 4-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrvmasum2if 25186* | Combine the results of dchrvmasumlem1 25184 and dchrvmasum2lem 25185 inside a conditional. (Contributed by Mario Carneiro, 4-May-2016.) |
| ℤ/nℤ RHom DChr Λ
| ||
| Theorem | dchrvmasumlem2 25187* | Lemma for dchrvmasum 25214. (Contributed by Mario Carneiro, 4-May-2016.) |
ℤ/nℤ RHom DChr
| ||
| Theorem | dchrvmasumlem3 25188* | Lemma for dchrvmasum 25214. (Contributed by Mario Carneiro, 3-May-2016.) |
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrvmasumlema 25189* |
Lemma for dchrvmasum 25214 and dchrvmasumif 25192. Apply dchrisum 25181 for
the function , which is
decreasing above
(or above 3, the nearest integer bound). (Contributed by Mario
Carneiro, 5-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrvmasumiflem1 25190* | Lemma for dchrvmasumif 25192. (Contributed by Mario Carneiro, 5-May-2016.) |
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrvmasumiflem2 25191* | Lemma for dchrvmasum 25214. (Contributed by Mario Carneiro, 5-May-2016.) |
| ℤ/nℤ RHom DChr
Λ | ||
| Theorem | dchrvmasumif 25192* |
An asymptotic approximation for the sum of Λ
conditional on the value of the infinite sum . (We will later
show that the case is impossible, and hence
establish
dchrvmasum 25214.) (Contributed by Mario Carneiro,
5-May-2016.)
|
| ℤ/nℤ RHom DChr
Λ | ||
| Theorem | dchrvmaeq0 25193* |
The set  is the
collection of all non-principal Dirichlet
characters such that the sum is equal
to zero. (Contributed by Mario Carneiro, 5-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrisum0fval 25194* |
Value of the function , the divisor sum of a Dirichlet
character. (Contributed by Mario Carneiro, 5-May-2016.)
|
ℤ/nℤ RHom DChr  
| ||
| Theorem | dchrisum0fmul 25195* |
The function , the
divisor sum of a Dirichlet character, is
a multiplicative function (but not completely multiplicative).
Equation 9.4.27 of [Shapiro], p.
382. (Contributed by Mario
Carneiro, 5-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrisum0ff 25196* |
The function is a
real function. (Contributed by Mario
Carneiro, 5-May-2016.)
|
ℤ/nℤ RHom DChr
 | ||
| Theorem | dchrisum0flblem1 25197* | Lemma for dchrisum0flb 25199. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.) |
ℤ/nℤ RHom DChr
 | ||
| Theorem | dchrisum0flblem2 25198* | Lemma for dchrisum0flb 25199. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.) |
| ℤ/nℤ RHom DChr
..^
| ||
| Theorem | dchrisum0flb 25199* | The divisor sum of a real Dirichlet character, is lower bounded by zero everywhere and one at the squares. Equation 9.4.29 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
| ℤ/nℤ RHom DChr
| ||
| Theorem | dchrisum0fno1 25200* |
The sum
is divergent (i.e. not
eventually bounded). Equation 9.4.30 of [Shapiro], p. 383.
(Contributed by Mario Carneiro, 5-May-2016.)
|
| ℤ/nℤ RHom DChr
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |