HomeTheorem List (p. 405 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. 405 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 | fourierdlem78 40401* |
 is continuous when
restricted on an interval not containing
 . (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
              ![[,]](_icc.gif "[,]"){kind=small}   
 
               
  
  
 | ||
| Theorem | fourierdlem79 40402* |
 projects every
interval of the partition induced by on
into a corresponding interval of the partition induced by  on
 ![]](rbrack.gif "]"){kind=small} .
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
         ![/\](wedge.gif "/\"){kind=small}  
..^     
..^
 
  
    
  ![(,]](_ioc.gif "(,]"){kind=small}  
  ..^
 ..^
 | ||
| Theorem | fourierdlem80 40403* |
The derivative of is
bounded on the given interval. (Contributed
by Glauco Siliprandi, 11-Dec-2019.)
|
..^ 
  ..^ 
..^
..^
..^
..^
  ..^
  | ||
| Theorem | fourierdlem81 40404* |
The integral of a piecewise continuous periodic function is
unchanged if the domain is shifted by its period . In this lemma,
is assumed to
be strictly positive. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
..^ 
..^
..^ 
lim ..^
lim
| ||
| Theorem | fourierdlem82 40405* | Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
lim lim
| ||
| Theorem | fourierdlem83 40406* |
The fourier partial sum for rewritten as an integral.
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
     
| ||
| Theorem | fourierdlem84 40407* |
If is piecewise
coninuous and is
continuous, then is
continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
..^
..^
..^
lim ..^
lim
..^
| ||
| Theorem | fourierdlem85 40408* |
Limit of the function
at the lower bounds of the partition
intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
..^
lim
..^
lim
..^ ..^
lim
..^
lim | ||
| Theorem | fourierdlem86 40409* |
Continuity of and its
limits with respect to the partition.
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
..^
..^
..^
lim ..^
lim
 ![]_](_urbrack.gif "]_"){kind=small}
..^
..^
lim
lim
| ||
| Theorem | fourierdlem87 40410* |
The integral of goes
uniformly ( with respect to ) to zero
if the measure of the domain of integration goes to zero. (Contributed
by Glauco Siliprandi, 11-Dec-2019.)
|
  
 
| ||
| Theorem | fourierdlem88 40411* |
Given a piecewise continuous function , a continuous function
and a
continuous function ,
the function is
integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
..^
lim
lim
..^
..^
lim ..^
lim
..^ ..^
lim lim | ||
| Theorem | fourierdlem89 40412* | Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^
..^
..^
lim
..^
 ..^
..^
..^
lim | ||
| Theorem | fourierdlem90 40413* | Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
..^
..^
..^
..^
..^
| ||
| Theorem | fourierdlem91 40414* | Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
..^
..^
..^
lim
..^
..^
..^
..^
lim
| ||
| Theorem | fourierdlem92 40415* |
The integral of a piecewise continuous periodic function is
unchanged if the domain is shifted by its period . (Contributed
by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
..^
lim ..^
lim
| ||
| Theorem | fourierdlem93 40416* |
Integral by substitution (the domain is shifted by ) for a
piecewise continuous function. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
lim
| ||
| Theorem | fourierdlem94 40417* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^
..^ lim   ..^ lim lim
lim
| ||
| Theorem | fourierdlem95 40418* | Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^
..^
..^
lim ..^
lim
..^
lim lim lim lim ![\](setminus.gif "\"){kind=small}
| ||
| Theorem | fourierdlem96 40419* |
limit for at the
lower bound of an interval for the moved
partition .
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
..^
..^
..^
lim ..^
..^
..^ ..^
lim | ||
| Theorem | fourierdlem97 40420* |
is continuous on the
intervals induced by the moved partition
. (Contributed
by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
| ||
| Theorem | fourierdlem98 40421* |
is continuous on the
intervals induced by the moved partition
. (Contributed
by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
| ||
| Theorem | fourierdlem99 40422* |
limit for at the
upper bound of an interval for the moved
partition .
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
..^
..^
..^
lim
| ||
| Theorem | fourierdlem100 40423* | A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
..^
..^
..^
lim ..^
lim
..^
..^
| ||
| Theorem | fourierdlem101 40424* | Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
..^
..^
..^
lim ..^
lim
| ||
| Theorem | fourierdlem102 40425* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
 
lim
lim
..^
lim
lim
| ||
| Theorem | fourierdlem103 40426* | The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^
..^
..^
..^
..^
..^
lim ..^
lim
lim
lim
lim
lim
 ..^
| ||
| Theorem | fourierdlem104 40427* | The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
..^
..^
..^
..^
..^
..^
lim ..^
lim
lim
lim
lim
lim
..^
| ||
| Theorem | fourierdlem105 40428* | A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
..^
..^
..^
lim ..^
lim | ||
| Theorem | fourierdlem106 40429* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
lim
lim
lim
lim
| ||
| Theorem | fourierdlem107 40430* |
The integral of a piecewise continuous periodic function is
unchanged if the domain is shifted by any positive value . This
lemma generalizes fourierdlem92 40415 where the integral was shifted by the
exact period. This lemma uses local definitions, so that the proof is
more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
lim
..^
..^
| ||
| Theorem | fourierdlem108 40431* |
The integral of a piecewise continuous periodic function is
unchanged if the domain is shifted by any positive value . This
lemma generalizes fourierdlem92 40415 where the integral was shifted by the
exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
lim | ||
| Theorem | fourierdlem109 40432* |
The integral of a piecewise continuous periodic function is
unchanged if the domain is shifted by any value . This lemma
generalizes fourierdlem92 40415 where the integral was shifted by
the exact
period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
lim
..^
..^
| ||
| Theorem | fourierdlem110 40433* |
The integral of a piecewise continuous periodic function is
unchanged if the domain is shifted by any value . This lemma
generalizes fourierdlem92 40415 where the integral was shifted by
the exact
period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
lim | ||
| Theorem | fourierdlem111 40434* |
The fourier partial sum for is the sum of two integrals, with the
same integrand involving and the Dirichlet Kernel , but on
two opposite intervals. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
..^
..^
..^
lim ..^
lim
..^
| ||
| Theorem | fourierdlem112 40435* |
Here abbreviations (local definitions) are introduced to prove the
fourier 40442 theorem. is the mth
partial sum of the fourier
series. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
..^
..^
..^
lim ..^
lim ..^
lim
lim
lim
lim
| ||
| Theorem | fourierdlem113 40436* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| lim lim
..^ ..^
..^ lim ..^ lim
| ||
| Theorem | fourierdlem114 40437* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
lim
lim
lim lim
..^
| ||
| Theorem | fourierdlem115 40438* | Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
lim
lim
lim lim
| ||
| Theorem | fourierd 40439* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 40443. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 40444 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 40449. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
lim
lim
lim lim
| ||
| Theorem | fourierclimd 40440* |
Fourier series convergence, for piecewise smooth functions. See
fourierd 40439 for the analogous equation. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
|
lim
lim
lim lim
| ||
| Theorem | fourierclim 40441* |
Fourier series convergence, for piecewise smooth functions. See
fourier 40442 for the analogous equation. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
|
lim
lim
lim lim
| ||
| Theorem | fourier 40442* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 40443. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 40444 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 40449. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
lim
lim
lim lim
| ||
| Theorem | fouriercnp 40443* |
If is continuous at
the point , then its
Fourier series at
, converges to
.
(Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
lim
lim
 
| ||
| Theorem | fourier2 40444* |
Fourier series convergence, for a piecewise smooth function. Here it is
also proven the existence of the left and right limits of at any
given point .
See fourierd 40439 for a comparison. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
lim
lim
lim lim
| ||
| Theorem | sqwvfoura 40445* |
Fourier coefficients for the square wave function. Since the square
function is an odd function, there is no contribution from the
coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
| ||
| Theorem | sqwvfourb 40446* |
Fourier series
coefficients for the square wave function.
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
 
| ||
| Theorem | fourierswlem 40447* |
The Fourier series for the square wave converges to , a
simpler expression for this special case. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
|
| ||
| Theorem | fouriersw 40448* |
Fourier series convergence, for the square wave function. Where
is discontinuous, the series converges to , the average value of
the left and the right limits. Notice that is an odd function and
its Fourier expansion has only sine terms (coefficients for cosine terms
are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
| ||
| Theorem | fouriercn 40449* |
If the derivative of
is continuous, then the Fourier series for
converges to
everywhere and the
hypothesis are simpler than
those for the more general case of a piecewise smooth function ( see
fourierd 40439 for a comparison). (Contributed by Glauco
Siliprandi,
11-Dec-2019.)
|
|
| ||
| Theorem | elaa2lem 40450* | Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 40451. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.) |
 Poly 
inf
coeff
coeff deg
 Polycoeff
| ||
| Theorem | elaa2 40451* |
Elementhood in the set of nonzero algebraic numbers: when is
nonzero, the polynomial can be chosen with a nonzero constant
term. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened
by AV, 1-Oct-2020.)
|
|
Polycoeff
| ||
| Theorem | etransclem1 40452* |
is a function.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem2 40453* |
Derivative of .
(Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
 | ||
| Theorem | etransclem3 40454 |
The given term is
an integer. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
| ||
| Theorem | etransclem4 40455* |
expressed as a finite
product. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
 | ||
| Theorem | etransclem5 40456* | A change of bound variable, often used in proofs for etransc 40500. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| | ||
| Theorem | etransclem6 40457* | A change of bound variable, often used in proofs for etransc 40500. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
|
| ||
| Theorem | etransclem7 40458* | The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
|
| ||
| Theorem | etransclem8 40459* |
is a function.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| | ||
| Theorem | etransclem9 40460 |
If divides but does not divide then
cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| | ||
| Theorem | etransclem10 40461 |
The given term is
an integer. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
|
| ||
| Theorem | etransclem11 40462* | A change of bound variable, often used in proofs for etransc 40500. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ||
| Theorem | etransclem12 40463* |
applied to . (Contributed by Glauco
Siliprandi,
5-Apr-2020.)
|
|
| ||
| Theorem | etransclem13 40464* |
applied to . (Contributed by Glauco
Siliprandi,
5-Apr-2020.)
|
| | ||
| Theorem | etransclem14 40465* |
Value of the term ,
when and
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem15 40466* |
Value of the term ,
when and
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem16 40467* |
Every element in the range of is a finite set. (Contributed by
Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem17 40468* |
The -th derivative of
. (Contributed by
Glauco Siliprandi,
5-Apr-2020.)
|
 ℂfld
↾t
| ||
| Theorem | etransclem18 40469* | The given function is integrable. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
ℂfld
↾t
 
| ||
| Theorem | etransclem19 40470* |
The -th derivative of
is 0 if is large enough.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem20 40471* |
is smooth.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t | ||
| Theorem | etransclem21 40472* |
The -th derivative of
applied to . (Contributed by
Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem22 40473* |
The -th derivative of
is continuous.
(Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem23 40474* | This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
|
| ||
| Theorem | etransclem24 40475* |
divides the I -th
derivative of applied
to . when
and is not equal to . This is the second part
of case 2 proven in [Juillerat] p. 13
. (Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem25 40476* |
factorial divides the
-th derivative of applied to
. (Contributed
by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem26 40477* |
Every term in the sum of the -th derivative of applied to
is an integer.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem27 40478* |
The -th derivative of
applied to is an integer.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem28 40479* |
factorial divides the -th derivative of
applied to .
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem29 40480* |
The -th derivative of
. (Contributed by
Glauco Siliprandi,
5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem30 40481* |
The -th derivative of
. (Contributed by
Glauco Siliprandi,
5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem31 40482* |
The -th derivative of
applied to . (Contributed by
Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem32 40483* | This is the proof for the last equation in the proof of the derivative calculated in [Juillerat] p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ℂfld
↾t
| ||
| Theorem | etransclem33 40484* |
is smooth.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t | ||
| Theorem | etransclem34 40485* |
The -th derivative of
is continuous.
(Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem35 40486* |
does not divide the
P-1 -th derivative of
applied to .
This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by
Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem36 40487* |
The -th derivative of
applied to is an integer.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t | ||
| Theorem | etransclem37 40488* |
factorial divides the -th derivative of
applied to .
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem38 40489* |
divides the I -th
derivative of applied
to . if it is
not the case that and
. This is case 1 and the
second part of case 2 proven in in [Juillerat] p. 13 . (Contributed by
Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem39 40490* |
is a function.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| | ||
| Theorem | etransclem40 40491* |
The -th derivative of
is continuous.
(Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t
| ||
| Theorem | etransclem41 40492* |
does not divide the
P-1 -th derivative of
applied to .
This is the first part of case 2: proven in in [Juillerat] p. 13 .
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
 | ||
| Theorem | etransclem42 40493* |
The -th derivative of
applied to is an integer.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| ℂfld
↾t | ||
| Theorem | etransclem43 40494* |
is a continuous
function. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
| ℂfld
↾t | ||
| Theorem | etransclem44 40495* | The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
 
| ||
| Theorem | etransclem45 40496* |
is an integer.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
| ||
| Theorem | etransclem46 40497* |
This is the proof for equation *(7) in [Juillerat] p. 12. The proven
equality will lead to a contradiction, because the left-hand side goes
to for large , but the right-hand side
is a nonzero integer.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
| Poly coeff deg
ℂfld
↾t
| ||
| Theorem | etransclem47 40498* |
is transcendental.
Section *5 of [Juillerat] p. 11 can be used
as a reference for this proof. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
| Poly coeff
deg
| ||
| Theorem | etransclem48 40499* |
is transcendental.
Section *5 of [Juillerat] p. 11 can be used
as a reference for this proof. In this lemma, a large enough prime
is chosen: it
will be used by subsequent lemmas. (Contributed by
Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.)
|
Poly coeff
deg inf
| ||
| Theorem | etransc 40500 |
is transcendental.
Section *5 of [Juillerat] p. 11 can be used
as a reference for this proof. (Contributed by Glauco Siliprandi,
5-Apr-2020.) (Proof shortened by AV, 28-Sep-2020.)
|
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |