Type | Label | Description |
Statement |
|
Theorem | prodrbdclem2 11601* |
Lemma for prodrbdc 11602. (Contributed by Scott Fenton,
4-Dec-2017.)
|
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π΄ β
(β€β₯βπ)) & β’ (π β π΄ β
(β€β₯βπ)) & β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΄)
& β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΄) β β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ) β πΆ β seqπ( Β· , πΉ) β πΆ)) |
|
Theorem | prodrbdc 11602* |
Rebase the starting point of a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π΄ β
(β€β₯βπ)) & β’ (π β π΄ β
(β€β₯βπ)) & β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΄)
& β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΄) β β’ (π β (seqπ( Β· , πΉ) β πΆ β seqπ( Β· , πΉ) β πΆ)) |
|
Theorem | prodmodclem3 11603* |
Lemma for prodmodc 11606. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 1)) & β’ π» = (π β β β¦ if(π β€ (β―βπ΄), β¦(πΎβπ) / πβ¦π΅, 1)) & β’ (π β (π β β β§ π β β)) & β’ (π β π:(1...π)β1-1-ontoβπ΄)
& β’ (π β πΎ:(1...π)β1-1-ontoβπ΄) β β’ (π β (seq1( Β· , πΊ)βπ) = (seq1( Β· , π»)βπ)) |
|
Theorem | prodmodclem2a 11604* |
Lemma for prodmodc 11606. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 1)) & β’ π» = (π β β β¦ if(π β€ (β―βπ΄), β¦(πΎβπ) / πβ¦π΅, 1)) & β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΄)
& β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π΄ β
(β€β₯βπ)) & β’ (π β π:(1...π)β1-1-ontoβπ΄)
& β’ (π β πΎ Isom < , <
((1...(β―βπ΄)),
π΄)) β β’ (π β seqπ( Β· , πΉ) β (seq1( Β· , πΊ)βπ)) |
|
Theorem | prodmodclem2 11605* |
Lemma for prodmodc 11606. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 13-Apr-2024.)
|
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 1)) β β’ ((π β§ βπ β β€ ((π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ (βπ β (β€β₯βπ)βπ¦(π¦ # 0 β§ seqπ( Β· , πΉ) β π¦) β§ seqπ( Β· , πΉ) β π₯))) β (βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π§ = (seq1( Β· , πΊ)βπ)) β π₯ = π§)) |
|
Theorem | prodmodc 11606* |
A product has at most one limit. (Contributed by Scott Fenton,
4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)
|
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 1)) β β’ (π β β*π₯(βπ β β€ ((π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ (βπ β (β€β₯βπ)βπ¦(π¦ # 0 β§ seqπ( Β· , πΉ) β π¦) β§ seqπ( Β· , πΉ) β π₯)) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( Β· , πΊ)βπ)))) |
|
Theorem | zproddc 11607* |
Series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β βπ β π βπ¦(π¦ # 0 β§ seqπ( Β· , πΉ) β π¦))
& β’ (π β π΄ β π)
& β’ (π β βπ β π DECID π β π΄)
& β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ = ( β βseqπ( Β· , πΉ))) |
|
Theorem | iprodap 11608* |
Series product with an upper integer index set (i.e. an infinite
product.) (Contributed by Scott Fenton, 5-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β βπ β π βπ¦(π¦ # 0 β§ seqπ( Β· , πΉ) β π¦))
& β’ ((π β§ π β π) β (πΉβπ) = π΅)
& β’ ((π β§ π β π) β π΅ β β)
β β’ (π β βπ β π π΅ = ( β βseqπ( Β· , πΉ))) |
|
Theorem | zprodap0 11609* |
Nonzero series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 6-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π # 0) & β’ (π β seqπ( Β· , πΉ) β π)
& β’ (π β βπ β π DECID π β π΄)
& β’ (π β π΄ β π)
& β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 1)) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ = π) |
|
Theorem | iprodap0 11610* |
Nonzero series product with an upper integer index set (i.e. an
infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π # 0) & β’ (π β seqπ( Β· , πΉ) β π)
& β’ ((π β§ π β π) β (πΉβπ) = π΅)
& β’ ((π β§ π β π) β π΅ β β)
β β’ (π β βπ β π π΅ = π) |
|
4.8.10.4 Finite products
|
|
Theorem | fprodseq 11611* |
The value of a product over a nonempty finite set. (Contributed by
Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
|
β’ (π = (πΉβπ) β π΅ = πΆ)
& β’ (π β π β β) & β’ (π β πΉ:(1...π)β1-1-ontoβπ΄)
& β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β (1...π)) β (πΊβπ) = πΆ) β β’ (π β βπ β π΄ π΅ = (seq1( Β· , (π β β β¦ if(π β€ π, (πΊβπ), 1)))βπ)) |
|
Theorem | fprodntrivap 11612* |
A non-triviality lemma for finite sequences. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ (π β π΄ β (π...π)) β β’ (π β βπ β π βπ¦(π¦ # 0 β§ seqπ( Β· , (π β π β¦ if(π β π΄, π΅, 1))) β π¦)) |
|
Theorem | prod0 11613 |
A product over the empty set is one. (Contributed by Scott Fenton,
5-Dec-2017.)
|
β’ βπ β β
π΄ = 1 |
|
Theorem | prod1dc 11614* |
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 π β π΄) β¨ π΄ β Fin) β βπ β π΄ 1 = 1) |
|
Theorem | prodfct 11615* |
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 11616* |
Re-index a finite product using a bijection. (Contributed by Scott
Fenton, 7-Dec-2017.)
|
β’ (π = πΊ β π΅ = π·)
& β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄)
& β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ)
& β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ = βπ β πΆ π·) |
|
Theorem | prodssdc 11617* |
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.)
|
β’ (π β π΄ β π΅)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ (π β βπ β (β€β₯βπ)βπ¦(π¦ # 0 β§ seqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))) β π¦))
& β’ (π β βπ β (β€β₯βπ)DECID π β π΄)
& β’ (π β π β β€) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 1) & β’ (π β π΅ β
(β€β₯βπ)) & β’ (π β βπ β
(β€β₯βπ)DECID π β π΅) β β’ (π β βπ β π΄ πΆ = βπ β π΅ πΆ) |
|
Theorem | fprodssdc 11618* |
Change the index set to a subset in a finite sum. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
β’ (π β π΄ β π΅)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ (π β βπ β π΅ DECID π β π΄)
& β’ ((π β§ π β (π΅ β π΄)) β πΆ = 1) & β’ (π β π΅ β Fin) β β’ (π β βπ β π΄ πΆ = βπ β π΅ πΆ) |
|
Theorem | fprodmul 11619* |
The product of two finite products. (Contributed by Scott Fenton,
14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β)
β β’ (π β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |
|
Theorem | prodsnf 11620* |
A product of a singleton is the term. A version of prodsn 11621 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ΅
& β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β βπ β {π}π΄ = π΅) |
|
Theorem | prodsn 11621* |
A product of a singleton is the term. (Contributed by Scott Fenton,
14-Dec-2017.)
|
β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β βπ β {π}π΄ = π΅) |
|
Theorem | fprod1 11622* |
A finite product of only one term is the term itself. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
β’ (π = π β π΄ = π΅) β β’ ((π β β€ β§ π΅ β β) β βπ β (π...π)π΄ = π΅) |
|
Theorem | climprod1 11623 |
The limit of a product over one. (Contributed by Scott Fenton,
15-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€)
β β’ (π β seqπ( Β· , (π Γ {1})) β 1) |
|
Theorem | fprodsplitdc 11624* |
Split a finite product into two parts. New proofs should use
fprodsplit 11625 which is the same but with one fewer
hypothesis.
(Contributed by Scott Fenton, 16-Dec-2017.)
(New usage is discouraged.)
|
β’ (π β (π΄ β© π΅) = β
) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ (π β βπ β π DECID π β π΄)
& β’ ((π β§ π β π) β πΆ β β)
β β’ (π β βπ β π πΆ = (βπ β π΄ πΆ Β· βπ β π΅ πΆ)) |
|
Theorem | fprodsplit 11625* |
Split a finite product into two parts. (Contributed by Scott Fenton,
16-Dec-2017.)
|
β’ (π β (π΄ β© π΅) = β
) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β)
β β’ (π β βπ β π πΆ = (βπ β π΄ πΆ Β· βπ β π΅ πΆ)) |
|
Theorem | fprodm1 11626* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = (βπ β (π...(π β 1))π΄ Β· π΅)) |
|
Theorem | fprod1p 11627* |
Separate out the first term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = (π΅ Β· βπ β ((π + 1)...π)π΄)) |
|
Theorem | fprodp1 11628* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β βπ β (π...(π + 1))π΄ = (βπ β (π...π)π΄ Β· π΅)) |
|
Theorem | fprodm1s 11629* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β)
β β’ (π β βπ β (π...π)π΄ = (βπ β (π...(π β 1))π΄ Β· β¦π / πβ¦π΄)) |
|
Theorem | fprodp1s 11630* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β)
β β’ (π β βπ β (π...(π + 1))π΄ = (βπ β (π...π)π΄ Β· β¦(π + 1) / πβ¦π΄)) |
|
Theorem | prodsns 11631* |
A product of the singleton is the term. (Contributed by Scott Fenton,
25-Dec-2017.)
|
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β βπ β {π}π΄ = β¦π / πβ¦π΄) |
|
Theorem | fprodunsn 11632* |
Multiply in an additional term in a finite product. See also
fprodsplitsn 11661 which is the same but with a β²ππ hypothesis in
place of the distinct variable condition between π and π.
(Contributed by Jim Kingdon, 16-Aug-2024.)
|
β’ β²ππ·
& β’ (π β π΄ β Fin) & β’ (π β π΅ β π)
& β’ (π β Β¬ π΅ β π΄)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ (π β π· β β) & β’ (π = π΅ β πΆ = π·) β β’ (π β βπ β (π΄ βͺ {π΅})πΆ = (βπ β π΄ πΆ Β· π·)) |
|
Theorem | fprodcl2lem 11633* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π)
& β’ (π β π΄ β β
)
β β’ (π β βπ β π΄ π΅ β π) |
|
Theorem | fprodcllem 11634* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.)
|
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π)
& β’ (π β 1 β π) β β’ (π β βπ β π΄ π΅ β π) |
|
Theorem | fprodcl 11635* |
Closure of a finite product of complex numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodrecl 11636* |
Closure of a finite product of real numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodzcl 11637* |
Closure of a finite product of integers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€)
β β’ (π β βπ β π΄ π΅ β β€) |
|
Theorem | fprodnncl 11638* |
Closure of a finite product of positive integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodrpcl 11639* |
Closure of a finite product of positive reals. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β
β+) β β’ (π β βπ β π΄ π΅ β
β+) |
|
Theorem | fprodnn0cl 11640* |
Closure of a finite product of nonnegative integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β
β0) β β’ (π β βπ β π΄ π΅ β
β0) |
|
Theorem | fprodcllemf 11641* |
Finite product closure lemma. A version of fprodcllem 11634 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π)
& β’ (π β 1 β π) β β’ (π β βπ β π΄ π΅ β π) |
|
Theorem | fprodreclf 11642* |
Closure of a finite product of real numbers. A version of fprodrecl 11636
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodfac 11643* |
Factorial using product notation. (Contributed by Scott Fenton,
15-Dec-2017.)
|
β’ (π΄ β β0 β
(!βπ΄) = βπ β (1...π΄)π) |
|
Theorem | fprodabs 11644* |
The absolute value of a finite product. (Contributed by Scott Fenton,
25-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ ((π β§ π β π) β π΄ β β)
β β’ (π β (absββπ β (π...π)π΄) = βπ β (π...π)(absβπ΄)) |
|
Theorem | fprodeq0 11645* |
Any finite product containing a zero term is itself zero. (Contributed
by Scott Fenton, 27-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π = π) β π΄ = 0) β β’ ((π β§ πΎ β (β€β₯βπ)) β βπ β (π...πΎ)π΄ = 0) |
|
Theorem | fprodshft 11646* |
Shift the index of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (π β πΎ) β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = βπ β ((π + πΎ)...(π + πΎ))π΅) |
|
Theorem | fprodrev 11647* |
Reversal of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (πΎ β π) β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = βπ β ((πΎ β π)...(πΎ β π))π΅) |
|
Theorem | fprodconst 11648* |
The product of constant terms (π is not free in π΅).
(Contributed by Scott Fenton, 12-Jan-2018.)
|
β’ ((π΄ β Fin β§ π΅ β β) β βπ β π΄ π΅ = (π΅β(β―βπ΄))) |
|
Theorem | fprodap0 11649* |
A finite product of nonzero terms is nonzero. (Contributed by Scott
Fenton, 15-Jan-2018.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β π΅ # 0) β β’ (π β βπ β π΄ π΅ # 0) |
|
Theorem | fprod2dlemstep 11650* |
Lemma for fprod2d 11651- induction step. (Contributed by Scott
Fenton,
30-Jan-2018.)
|
β’ (π§ = β¨π, πβ© β π· = πΆ)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) & β’ (π β Β¬ π¦ β π₯)
& β’ (π β (π₯ βͺ {π¦}) β π΄)
& β’ (π β π₯ β Fin) & β’ (π β βπ β π₯ βπ β π΅ πΆ = βπ§ β βͺ
π β π₯ ({π} Γ π΅)π·) β β’ ((π β§ π) β βπ β (π₯ βͺ {π¦})βπ β π΅ πΆ = βπ§ β βͺ
π β (π₯ βͺ {π¦})({π} Γ π΅)π·) |
|
Theorem | fprod2d 11651* |
Write a double product as a product over a two-dimensional region.
Compare fsum2d 11463. (Contributed by Scott Fenton,
30-Jan-2018.)
|
β’ (π§ = β¨π, πβ© β π· = πΆ)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΆ = βπ§ β βͺ
π β π΄ ({π} Γ π΅)π·) |
|
Theorem | fprodxp 11652* |
Combine two products into a single product over the cartesian product.
(Contributed by Scott Fenton, 1-Feb-2018.)
|
β’ (π§ = β¨π, πβ© β π· = πΆ)
& β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΆ = βπ§ β (π΄ Γ π΅)π·) |
|
Theorem | fprodcnv 11653* |
Transform a product region using the converse operation. (Contributed
by Scott Fenton, 1-Feb-2018.)
|
β’ (π₯ = β¨π, πβ© β π΅ = π·)
& β’ (π¦ = β¨π, πβ© β πΆ = π·)
& β’ (π β π΄ β Fin) & β’ (π β Rel π΄)
& β’ ((π β§ π₯ β π΄) β π΅ β β)
β β’ (π β βπ₯ β π΄ π΅ = βπ¦ β β‘ π΄πΆ) |
|
Theorem | fprodcom2fi 11654* |
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.)
|
β’ (π β π΄ β Fin) & β’ (π β πΆ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ π β πΆ) β π· β Fin) & β’ (π β ((π β π΄ β§ π β π΅) β (π β πΆ β§ π β π·))) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΈ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΈ = βπ β πΆ βπ β π· πΈ) |
|
Theorem | fprodcom 11655* |
Interchange product order. (Contributed by Scott Fenton,
2-Feb-2018.)
|
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΆ = βπ β π΅ βπ β π΄ πΆ) |
|
Theorem | fprod0diagfz 11656* |
Two ways to express "the product of π΄(π, π) over the triangular
region π β€ π, π β€ π, π + π β€ π. Compare
fisum0diag 11469. (Contributed by Scott Fenton, 2-Feb-2018.)
|
β’ ((π β§ (π β (0...π) β§ π β (0...(π β π)))) β π΄ β β) & β’ (π β π β β€)
β β’ (π β βπ β (0...π)βπ β (0...(π β π))π΄ = βπ β (0...π)βπ β (0...(π β π))π΄) |
|
Theorem | fprodrec 11657* |
The finite product of reciprocals is the reciprocal of the product.
(Contributed by Jim Kingdon, 28-Aug-2024.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β π΅ # 0) β β’ (π β βπ β π΄ (1 / π΅) = (1 / βπ β π΄ π΅)) |
|
Theorem | fproddivap 11658* |
The quotient of two finite products. (Contributed by Scott Fenton,
15-Jan-2018.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β πΆ # 0) β β’ (π β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |
|
Theorem | fproddivapf 11659* |
The quotient of two finite products. A version of fproddivap 11658 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β πΆ # 0) β β’ (π β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |
|
Theorem | fprodsplitf 11660* |
Split a finite product into two parts. A version of fprodsplit 11625 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β (π΄ β© π΅) = β
) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β)
β β’ (π β βπ β π πΆ = (βπ β π΄ πΆ Β· βπ β π΅ πΆ)) |
|
Theorem | fprodsplitsn 11661* |
Separate out a term in a finite product. See also fprodunsn 11632 which is
the same but with a distinct variable condition in place of
β²ππ. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
β’ β²ππ
& β’ β²ππ·
& β’ (π β π΄ β Fin) & β’ (π β π΅ β π)
& β’ (π β Β¬ π΅ β π΄)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ (π = π΅ β πΆ = π·)
& β’ (π β π· β β)
β β’ (π β βπ β (π΄ βͺ {π΅})πΆ = (βπ β π΄ πΆ Β· π·)) |
|
Theorem | fprodsplit1f 11662* |
Separate out a term in a finite product. (Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β β²ππ·)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄)
& β’ ((π β§ π = πΆ) β π΅ = π·) β β’ (π β βπ β π΄ π΅ = (π· Β· βπ β (π΄ β {πΆ})π΅)) |
|
Theorem | fprodclf 11663* |
Closure of a finite product of complex numbers. A version of fprodcl 11635
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodap0f 11664* |
A finite product of terms apart from zero is apart from zero. A version
of fprodap0 11649 using bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
(Revised by Jim Kingdon, 30-Aug-2024.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β π΅ # 0) β β’ (π β βπ β π΄ π΅ # 0) |
|
Theorem | fprodge0 11665* |
If all the terms of a finite product are nonnegative, so is the product.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) β β’ (π β 0 β€ βπ β π΄ π΅) |
|
Theorem | fprodeq0g 11666* |
Any finite product containing a zero term is itself zero. (Contributed
by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄)
& β’ ((π β§ π = πΆ) β π΅ = 0) β β’ (π β βπ β π΄ π΅ = 0) |
|
Theorem | fprodge1 11667* |
If all of the terms of a finite product are greater than or equal to
1, so is the product. (Contributed by Glauco
Siliprandi,
5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 1 β€ π΅) β β’ (π β 1 β€ βπ β π΄ π΅) |
|
Theorem | fprodle 11668* |
If all the terms of two finite products are nonnegative and compare, so
do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β€ πΆ) β β’ (π β βπ β π΄ π΅ β€ βπ β π΄ πΆ) |
|
Theorem | fprodmodd 11669* |
If all factors of two finite products are equal modulo π, the
products are equal modulo π. (Contributed by AV, 7-Jul-2021.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) & β’ ((π β§ π β π΄) β πΆ β β€) & β’ (π β π β β) & β’ ((π β§ π β π΄) β (π΅ mod π) = (πΆ mod π)) β β’ (π β (βπ β π΄ π΅ mod π) = (βπ β π΄ πΆ mod π)) |
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11670 |
Extend class notation to include the exponential function.
|
class exp |
|
Syntax | ceu 11671 |
Extend class notation to include Euler's constant e =
2.71828....
|
class e |
|
Syntax | csin 11672 |
Extend class notation to include the sine function.
|
class sin |
|
Syntax | ccos 11673 |
Extend class notation to include the cosine function.
|
class cos |
|
Syntax | ctan 11674 |
Extend class notation to include the tangent function.
|
class tan |
|
Syntax | cpi 11675 |
Extend class notation to include the constant pi, Ο
= 3.14159....
|
class Ο |
|
Definition | df-ef 11676* |
Define the exponential function. Its value at the complex number π΄
is (expβπ΄) and is called the "exponential
of π΄"; see
efval 11689. (Contributed by NM, 14-Mar-2005.)
|
β’ exp = (π₯ β β β¦ Ξ£π β β0
((π₯βπ) / (!βπ))) |
|
Definition | df-e 11677 |
Define Euler's constant e = 2.71828.... (Contributed
by NM,
14-Mar-2005.)
|
β’ e = (expβ1) |
|
Definition | df-sin 11678 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
β’ sin = (π₯ β β β¦ (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) / (2 Β· i))) |
|
Definition | df-cos 11679 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
β’ cos = (π₯ β β β¦ (((expβ(i
Β· π₯)) +
(expβ(-i Β· π₯))) / 2)) |
|
Definition | df-tan 11680 |
Define the tangent function. We define it this way for cmpt 4079,
which
requires the form (π₯ β π΄ β¦ π΅). (Contributed by Mario
Carneiro, 14-Mar-2014.)
|
β’ tan = (π₯ β (β‘cos β (β β {0})) β¦
((sinβπ₯) /
(cosβπ₯))) |
|
Definition | df-pi 11681 |
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((β+ β© (β‘sin β {0})), β, <
) |
|
Theorem | eftcl 11682 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
β’ ((π΄ β β β§ πΎ β β0) β ((π΄βπΎ) / (!βπΎ)) β β) |
|
Theorem | reeftcl 11683 |
The terms of the series expansion of the exponential function at a real
number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|
β’ ((π΄ β β β§ πΎ β β0) β ((π΄βπΎ) / (!βπΎ)) β β) |
|
Theorem | eftabs 11684 |
The absolute value of a term in the series expansion of the exponential
function. (Contributed by Paul Chapman, 23-Nov-2007.)
|
β’ ((π΄ β β β§ πΎ β β0) β
(absβ((π΄βπΎ) / (!βπΎ))) = (((absβπ΄)βπΎ) / (!βπΎ))) |
|
Theorem | eftvalcn 11685* |
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.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ ((π΄ β β β§ π β β0) β (πΉβπ) = ((π΄βπ) / (!βπ))) |
|
Theorem | efcllemp 11686* |
Lemma for efcl 11692. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11561 is used to show convergence.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ (π β π΄ β β) & β’ (π β πΎ β β) & β’ (π β (2 Β·
(absβπ΄)) < πΎ)
β β’ (π β seq0( + , πΉ) β dom β ) |
|
Theorem | efcllem 11687* |
Lemma for efcl 11692. The series that defines the exponential
function
converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β seq0( + , πΉ) β dom β
) |
|
Theorem | ef0lem 11688* |
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.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ = 0 β seq0( + , πΉ) β 1) |
|
Theorem | efval 11689* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 ((π΄βπ) / (!βπ))) |
|
Theorem | esum 11690 |
Value of Euler's constant e = 2.71828.... (Contributed
by Steve
Rodriguez, 5-Mar-2006.)
|
β’ e = Ξ£π β β0 (1 /
(!βπ)) |
|
Theorem | eff 11691 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
β’ exp:ββΆβ |
|
Theorem | efcl 11692 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
β’ (π΄ β β β (expβπ΄) β
β) |
|
Theorem | efval2 11693* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 (πΉβπ)) |
|
Theorem | efcvg 11694* |
The series that defines the exponential function converges to it.
(Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β seq0( + , πΉ) β (expβπ΄)) |
|
Theorem | efcvgfsum 11695* |
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.)
|
β’ πΉ = (π β β0 β¦
Ξ£π β (0...π)((π΄βπ) / (!βπ))) β β’ (π΄ β β β πΉ β (expβπ΄)) |
|
Theorem | reefcl 11696 |
The exponential function is real if its argument is real. (Contributed
by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
β’ (π΄ β β β (expβπ΄) β
β) |
|
Theorem | reefcld 11697 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
β’ (π β π΄ β β)
β β’ (π β (expβπ΄) β β) |
|
Theorem | ere 11698 |
Euler's constant e = 2.71828... is a real number.
(Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
β’ e β β |
|
Theorem | ege2le3 11699 |
Euler's constant e = 2.71828... is bounded by 2 and 3.
(Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
β’ πΉ = (π β β β¦ (2 Β· ((1 /
2)βπ))) & β’ πΊ = (π β β0 β¦ (1 /
(!βπ))) β β’ (2 β€ e β§ e β€
3) |
|
Theorem | ef0 11700 |
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.)
|
β’ (expβ0) = 1 |