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