Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | clim2prod 11301* |
The limit of an infinite product with an initial segment added.
(Contributed by Scott Fenton, 18-Dec-2017.)
|
|
|
Theorem | clim2divap 11302* |
The limit of an infinite product with an initial segment removed.
(Contributed by Scott Fenton, 20-Dec-2017.)
|
#
|
|
Theorem | prod3fmul 11303* |
The product of two infinite products. (Contributed by Scott Fenton,
18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
|
|
|
Theorem | prodf1 11304 |
The value of the partial products in a one-valued infinite product.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
|
|
Theorem | prodf1f 11305 |
A one-valued infinite product is equal to the constant one function.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
|
|
Theorem | prodfclim1 11306 |
The constant one product converges to one. (Contributed by Scott
Fenton, 5-Dec-2017.)
|
|
|
Theorem | prodfap0 11307* |
The product of finitely many terms apart from zero is apart from zero.
(Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon,
23-Mar-2024.)
|
# # |
|
Theorem | prodfrecap 11308* |
The reciprocal of a finite product. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
#
|
|
Theorem | prodfdivap 11309* |
The quotient of two products. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
#
|
|
4.8.10.2 Non-trivial convergence
|
|
Theorem | ntrivcvgap 11310* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
#
|
|
Theorem | ntrivcvgap0 11311* |
A product that converges to a value apart from zero converges
non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|
#
#
|
|
4.8.10.3 Complex products
|
|
Syntax | cprod 11312 |
Extend class notation to include complex products.
|
|
|
Definition | df-proddc 11313* |
Define the product of a series with an index set of integers .
This definition takes most of the aspects of df-sumdc 11116 and adapts them
for multiplication instead of addition. However, we insist that in the
infinite case, there is a nonzero tail of the sequence. This ensures
that the convergence criteria match those of infinite sums.
(Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon,
21-Mar-2024.)
|
DECID
#
|
|
Theorem | prodeq1f 11314 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
|
|
Theorem | prodeq1 11315* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
|
|
Theorem | nfcprod1 11316* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
|
|
Theorem | nfcprod 11317* |
Bound-variable hypothesis builder for product: if is (effectively)
not free in
and , it is not free
in .
(Contributed by Scott Fenton, 1-Dec-2017.)
|
|
|
Theorem | prodeq2w 11318* |
Equality theorem for product, when the class expressions and
are equal everywhere. Proved using only Extensionality. (Contributed
by Scott Fenton, 4-Dec-2017.)
|
|
|
Theorem | prodeq2 11319* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | cbvprod 11320* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | cbvprodv 11321* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | cbvprodi 11322* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq1i 11323* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq2i 11324* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq12i 11325* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq1d 11326* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq2d 11327* |
Equality deduction for product. Note that unlike prodeq2dv 11328,
may occur in . (Contributed by Scott Fenton, 4-Dec-2017.)
|
|
|
Theorem | prodeq2dv 11328* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq2sdv 11329* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | 2cprodeq2dv 11330* |
Equality deduction for double product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq12dv 11331* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq12rdv 11332* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodrbdclem 11333* |
Lemma for prodrbdc 11336. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 4-Apr-2024.)
|
DECID
|
|
Theorem | fproddccvg 11334* |
The sequence of partial products of a finite product converges to
the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
|
DECID |
|
Theorem | prodrbdclem2 11335* |
Lemma for prodrbdc 11336. (Contributed by Scott Fenton,
4-Dec-2017.)
|
DECID
DECID
|
|
Theorem | prodrbdc 11336* |
Rebase the starting point of a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
DECID
DECID
|
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11337 |
Extend class notation to include the exponential function.
|
|
|
Syntax | ceu 11338 |
Extend class notation to include Euler's constant = 2.71828....
|
|
|
Syntax | csin 11339 |
Extend class notation to include the sine function.
|
|
|
Syntax | ccos 11340 |
Extend class notation to include the cosine function.
|
|
|
Syntax | ctan 11341 |
Extend class notation to include the tangent function.
|
|
|
Syntax | cpi 11342 |
Extend class notation to include the constant pi, = 3.14159....
|
|
|
Definition | df-ef 11343* |
Define the exponential function. Its value at the complex number
is and is called the "exponential of "; see
efval 11356. (Contributed by NM, 14-Mar-2005.)
|
|
|
Definition | df-e 11344 |
Define Euler's constant = 2.71828.... (Contributed by NM,
14-Mar-2005.)
|
|
|
Definition | df-sin 11345 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
|
|
Definition | df-cos 11346 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
|
|
Definition | df-tan 11347 |
Define the tangent function. We define it this way for cmpt 3984,
which
requires the form .
(Contributed by Mario
Carneiro, 14-Mar-2014.)
|
|
|
Definition | df-pi 11348 |
Define the constant pi, = 3.14159..., which is the smallest
positive number whose sine is zero. Definition of in [Gleason]
p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV,
14-Sep-2020.)
|
inf |
|
Theorem | eftcl 11349 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
|
|
Theorem | reeftcl 11350 |
The terms of the series expansion of the exponential function at a real
number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|
|
|
Theorem | eftabs 11351 |
The absolute value of a term in the series expansion of the exponential
function. (Contributed by Paul Chapman, 23-Nov-2007.)
|
|
|
Theorem | eftvalcn 11352* |
The value of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
|
|
Theorem | efcllemp 11353* |
Lemma for efcl 11359. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11295 is used to show convergence.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
|
|
Theorem | efcllem 11354* |
Lemma for efcl 11359. The series that defines the exponential
function
converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
|
|
Theorem | ef0lem 11355* |
The series defining the exponential function converges in the (trivial)
case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | efval 11356* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | esum 11357 |
Value of Euler's constant = 2.71828.... (Contributed by Steve
Rodriguez, 5-Mar-2006.)
|
|
|
Theorem | eff 11358 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
|
|
Theorem | efcl 11359 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | efval2 11360* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|
|
|
Theorem | efcvg 11361* |
The series that defines the exponential function converges to it.
(Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
|
|
Theorem | efcvgfsum 11362* |
Exponential function convergence in terms of a sequence of partial
finite sums. (Contributed by NM, 10-Jan-2006.) (Revised by Mario
Carneiro, 28-Apr-2014.)
|
|
|
Theorem | reefcl 11363 |
The exponential function is real if its argument is real. (Contributed
by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | reefcld 11364 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | ere 11365 |
Euler's constant =
2.71828... is a real number. (Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
|
|
Theorem | ege2le3 11366 |
Euler's constant =
2.71828... is bounded by 2 and 3.
(Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
|
|
Theorem | ef0 11367 |
Value of the exponential function at 0. Equation 2 of [Gleason] p. 308.
(Contributed by Steve Rodriguez, 27-Jun-2006.) (Revised by Mario
Carneiro, 28-Apr-2014.)
|
|
|
Theorem | efcj 11368 |
The exponential of a complex conjugate. Equation 3 of [Gleason] p. 308.
(Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
|
|
Theorem | efaddlem 11369* |
Lemma for efadd 11370 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | efadd 11370 |
Sum of exponents law for exponential function. (Contributed by NM,
10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | efcan 11371 |
Cancellation law for exponential function. Equation 27 of [Rudin] p. 164.
(Contributed by NM, 13-Jan-2006.)
|
|
|
Theorem | efap0 11372 |
The exponential of a complex number is apart from zero. (Contributed by
Jim Kingdon, 12-Dec-2022.)
|
# |
|
Theorem | efne0 11373 |
The exponential of a complex number is nonzero. Corollary 15-4.3 of
[Gleason] p. 309. The same result also
holds with not equal replaced by
apart, as seen at efap0 11372 (which will be more useful in most
contexts).
(Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
|
|
Theorem | efneg 11374 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
|
|
Theorem | eff2 11375 |
The exponential function maps the complex numbers to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
|
|
Theorem | efsub 11376 |
Difference of exponents law for exponential function. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
|
|
Theorem | efexp 11377 |
The exponential of an integer power. Corollary 15-4.4 of [Gleason]
p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006.)
(Revised by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | efzval 11378 |
Value of the exponential function for integers. Special case of efval 11356.
Equation 30 of [Rudin] p. 164. (Contributed
by Steve Rodriguez,
15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | efgt0 11379 |
The exponential of a real number is greater than 0. (Contributed by Paul
Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | rpefcl 11380 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | rpefcld 11381 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | eftlcvg 11382* |
The tail series of the exponential function are convergent.
(Contributed by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | eftlcl 11383* |
Closure of the sum of an infinite tail of the series defining the
exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | reeftlcl 11384* |
Closure of the sum of an infinite tail of the series defining the
exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | eftlub 11385* |
An upper bound on the absolute value of the infinite tail of the series
expansion of the exponential function on the closed unit disk.
(Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario
Carneiro, 29-Apr-2014.)
|
|
|
Theorem | efsep 11386* |
Separate out the next term of the power series expansion of the
exponential function. The last hypothesis allows the separated terms to
be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.)
(Revised by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | effsumlt 11387* |
The partial sums of the series expansion of the exponential function at
a positive real number are bounded by the value of the function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
|
|
Theorem | eft0val 11388 |
The value of the first term of the series expansion of the exponential
function is 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by
Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | ef4p 11389* |
Separate out the first four terms of the infinite series expansion of
the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.)
(Revised by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | efgt1p2 11390 |
The exponential of a positive real number is greater than the sum of the
first three terms of the series expansion. (Contributed by Mario
Carneiro, 15-Sep-2014.)
|
|
|
Theorem | efgt1p 11391 |
The exponential of a positive real number is greater than 1 plus that
number. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by
Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | efgt1 11392 |
The exponential of a positive real number is greater than 1.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro,
30-Apr-2014.)
|
|
|
Theorem | efltim 11393 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
20-Dec-2022.)
|
|
|
Theorem | efler 11394 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 20-Dec-2022.)
|
|
|
Theorem | reef11 11395 |
The exponential function on real numbers is one-to-one. (Contributed by
NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.)
|
|
|
Theorem | reeff1 11396 |
The exponential function maps real arguments one-to-one to positive
reals. (Contributed by Steve Rodriguez, 25-Aug-2007.) (Revised by
Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | eflegeo 11397 |
The exponential function on the reals between 0 and 1 lies below the
comparable geometric series sum. (Contributed by Paul Chapman,
11-Sep-2007.)
|
|
|
Theorem | sinval 11398 |
Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised
by Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | cosval 11399 |
Value of the cosine function. (Contributed by NM, 14-Mar-2005.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | sinf 11400 |
Domain and codomain of the sine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
|