Theorem List for Intuitionistic Logic Explorer - 11501-11600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | prodfap0 11501* |
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 11502* |
The reciprocal of a finite product. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
#
|
|
Theorem | prodfdivap 11503* |
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 11504* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
#
|
|
Theorem | ntrivcvgap0 11505* |
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 11506 |
Extend class notation to include complex products.
|
|
|
Definition | df-proddc 11507* |
Define the product of a series with an index set of integers .
This definition takes most of the aspects of df-sumdc 11310 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 11508 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
|
|
Theorem | prodeq1 11509* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
|
|
Theorem | nfcprod1 11510* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
|
|
Theorem | nfcprod 11511* |
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 11512* |
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 11513* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | cbvprod 11514* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | cbvprodv 11515* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | cbvprodi 11516* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq1i 11517* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq2i 11518* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq12i 11519* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq1d 11520* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq2d 11521* |
Equality deduction for product. Note that unlike prodeq2dv 11522,
may occur in . (Contributed by Scott Fenton, 4-Dec-2017.)
|
|
|
Theorem | prodeq2dv 11522* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq2sdv 11523* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | 2cprodeq2dv 11524* |
Equality deduction for double product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq12dv 11525* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodeq12rdv 11526* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
|
|
Theorem | prodrbdclem 11527* |
Lemma for prodrbdc 11530. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 4-Apr-2024.)
|
DECID
|
|
Theorem | fproddccvg 11528* |
The sequence of partial products of a finite product converges to
the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
|
DECID |
|
Theorem | prodrbdclem2 11529* |
Lemma for prodrbdc 11530. (Contributed by Scott Fenton,
4-Dec-2017.)
|
DECID
DECID
|
|
Theorem | prodrbdc 11530* |
Rebase the starting point of a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
DECID
DECID
|
|
Theorem | prodmodclem3 11531* |
Lemma for prodmodc 11534. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
♯
♯
|
|
Theorem | prodmodclem2a 11532* |
Lemma for prodmodc 11534. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
♯
♯
DECID ♯
|
|
Theorem | prodmodclem2 11533* |
Lemma for prodmodc 11534. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 13-Apr-2024.)
|
♯
DECID #
|
|
Theorem | prodmodc 11534* |
A product has at most one limit. (Contributed by Scott Fenton,
4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)
|
♯
DECID
#
|
|
Theorem | zproddc 11535* |
Series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
#
DECID
|
|
Theorem | iprodap 11536* |
Series product with an upper integer index set (i.e. an infinite
product.) (Contributed by Scott Fenton, 5-Dec-2017.)
|
#
|
|
Theorem | zprodap0 11537* |
Nonzero series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 6-Dec-2017.)
|
#
DECID
|
|
Theorem | iprodap0 11538* |
Nonzero series product with an upper integer index set (i.e. an
infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
|
#
|
|
4.8.10.4 Finite products
|
|
Theorem | fprodseq 11539* |
The value of a product over a nonempty finite set. (Contributed by
Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
|
|
|
Theorem | fprodntrivap 11540* |
A non-triviality lemma for finite sequences. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
#
|
|
Theorem | prod0 11541 |
A product over the empty set is one. (Contributed by Scott Fenton,
5-Dec-2017.)
|
|
|
Theorem | prod1dc 11542* |
Any product of one over a valid set is one. (Contributed by Scott
Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
|
DECID |
|
Theorem | prodfct 11543* |
A lemma to facilitate conversions from the function form to the
class-variable form of a product. (Contributed by Scott Fenton,
7-Dec-2017.)
|
|
|
Theorem | fprodf1o 11544* |
Re-index a finite product using a bijection. (Contributed by Scott
Fenton, 7-Dec-2017.)
|
|
|
Theorem | prodssdc 11545* |
Change the index set to a subset in an upper integer product.
(Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon,
6-Aug-2024.)
|
# DECID
DECID
|
|
Theorem | fprodssdc 11546* |
Change the index set to a subset in a finite sum. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
DECID
|
|
Theorem | fprodmul 11547* |
The product of two finite products. (Contributed by Scott Fenton,
14-Dec-2017.)
|
|
|
Theorem | prodsnf 11548* |
A product of a singleton is the term. A version of prodsn 11549 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | prodsn 11549* |
A product of a singleton is the term. (Contributed by Scott Fenton,
14-Dec-2017.)
|
|
|
Theorem | fprod1 11550* |
A finite product of only one term is the term itself. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
|
|
Theorem | climprod1 11551 |
The limit of a product over one. (Contributed by Scott Fenton,
15-Dec-2017.)
|
|
|
Theorem | fprodsplitdc 11552* |
Split a finite product into two parts. New proofs should use
fprodsplit 11553 which is the same but with one fewer
hypothesis.
(Contributed by Scott Fenton, 16-Dec-2017.)
(New usage is discouraged.)
|
DECID
|
|
Theorem | fprodsplit 11553* |
Split a finite product into two parts. (Contributed by Scott Fenton,
16-Dec-2017.)
|
|
|
Theorem | fprodm1 11554* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
|
|
Theorem | fprod1p 11555* |
Separate out the first term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
|
|
Theorem | fprodp1 11556* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
|
|
Theorem | fprodm1s 11557* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
|
|
Theorem | fprodp1s 11558* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
|
|
Theorem | prodsns 11559* |
A product of the singleton is the term. (Contributed by Scott Fenton,
25-Dec-2017.)
|
|
|
Theorem | fprodunsn 11560* |
Multiply in an additional term in a finite product. See also
fprodsplitsn 11589 which is the same but with a hypothesis in
place of the distinct variable condition between and .
(Contributed by Jim Kingdon, 16-Aug-2024.)
|
|
|
Theorem | fprodcl2lem 11561* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|
|
|
Theorem | fprodcllem 11562* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.)
|
|
|
Theorem | fprodcl 11563* |
Closure of a finite product of complex numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
|
|
Theorem | fprodrecl 11564* |
Closure of a finite product of real numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
|
|
Theorem | fprodzcl 11565* |
Closure of a finite product of integers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
|
|
Theorem | fprodnncl 11566* |
Closure of a finite product of positive integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
|
|
Theorem | fprodrpcl 11567* |
Closure of a finite product of positive reals. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
|
|
Theorem | fprodnn0cl 11568* |
Closure of a finite product of nonnegative integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
|
|
Theorem | fprodcllemf 11569* |
Finite product closure lemma. A version of fprodcllem 11562 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodreclf 11570* |
Closure of a finite product of real numbers. A version of fprodrecl 11564
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodfac 11571* |
Factorial using product notation. (Contributed by Scott Fenton,
15-Dec-2017.)
|
|
|
Theorem | fprodabs 11572* |
The absolute value of a finite product. (Contributed by Scott Fenton,
25-Dec-2017.)
|
|
|
Theorem | fprodeq0 11573* |
Any finite product containing a zero term is itself zero. (Contributed
by Scott Fenton, 27-Dec-2017.)
|
|
|
Theorem | fprodshft 11574* |
Shift the index of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
|
|
Theorem | fprodrev 11575* |
Reversal of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
|
|
Theorem | fprodconst 11576* |
The product of constant terms ( is not free in ).
(Contributed by Scott Fenton, 12-Jan-2018.)
|
♯ |
|
Theorem | fprodap0 11577* |
A finite product of nonzero terms is nonzero. (Contributed by Scott
Fenton, 15-Jan-2018.)
|
# # |
|
Theorem | fprod2dlemstep 11578* |
Lemma for fprod2d 11579- induction step. (Contributed by Scott
Fenton,
30-Jan-2018.)
|
|
|
Theorem | fprod2d 11579* |
Write a double product as a product over a two-dimensional region.
Compare fsum2d 11391. (Contributed by Scott Fenton,
30-Jan-2018.)
|
|
|
Theorem | fprodxp 11580* |
Combine two products into a single product over the cartesian product.
(Contributed by Scott Fenton, 1-Feb-2018.)
|
|
|
Theorem | fprodcnv 11581* |
Transform a product region using the converse operation. (Contributed
by Scott Fenton, 1-Feb-2018.)
|
|
|
Theorem | fprodcom2fi 11582* |
Interchange order of multiplication. Note that and
are not necessarily constant expressions. (Contributed by
Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
|
|
|
Theorem | fprodcom 11583* |
Interchange product order. (Contributed by Scott Fenton,
2-Feb-2018.)
|
|
|
Theorem | fprod0diagfz 11584* |
Two ways to express "the product of over the
triangular
region , ,
. Compare
fisum0diag 11397. (Contributed by Scott Fenton, 2-Feb-2018.)
|
|
|
Theorem | fprodrec 11585* |
The finite product of reciprocals is the reciprocal of the product.
(Contributed by Jim Kingdon, 28-Aug-2024.)
|
#
|
|
Theorem | fproddivap 11586* |
The quotient of two finite products. (Contributed by Scott Fenton,
15-Jan-2018.)
|
# |
|
Theorem | fproddivapf 11587* |
The quotient of two finite products. A version of fproddivap 11586 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
#
|
|
Theorem | fprodsplitf 11588* |
Split a finite product into two parts. A version of fprodsplit 11553 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodsplitsn 11589* |
Separate out a term in a finite product. See also fprodunsn 11560 which is
the same but with a distinct variable condition in place of
. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
|
|
Theorem | fprodsplit1f 11590* |
Separate out a term in a finite product. (Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodclf 11591* |
Closure of a finite product of complex numbers. A version of fprodcl 11563
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodap0f 11592* |
A finite product of terms apart from zero is apart from zero. A version
of fprodap0 11577 using bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
(Revised by Jim Kingdon, 30-Aug-2024.)
|
# # |
|
Theorem | fprodge0 11593* |
If all the terms of a finite product are nonnegative, so is the product.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodeq0g 11594* |
Any finite product containing a zero term is itself zero. (Contributed
by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodge1 11595* |
If all of the terms of a finite product are greater than or equal to
, so is the
product. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
|
|
Theorem | fprodle 11596* |
If all the terms of two finite products are nonnegative and compare, so
do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | fprodmodd 11597* |
If all factors of two finite products are equal modulo , the
products are equal modulo . (Contributed by AV, 7-Jul-2021.)
|
|
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11598 |
Extend class notation to include the exponential function.
|
|
|
Syntax | ceu 11599 |
Extend class notation to include Euler's constant = 2.71828....
|
|
|
Syntax | csin 11600 |
Extend class notation to include the sine function.
|
|