Type | Label | Description |
Statement |
|
Theorem | iprodap 11601* |
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 11602* |
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 11603* |
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 11604* |
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 11605* |
A non-triviality lemma for finite sequences. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ (π β π΄ β (π...π)) β β’ (π β βπ β π βπ¦(π¦ # 0 β§ seqπ( Β· , (π β π β¦ if(π β π΄, π΅, 1))) β π¦)) |
|
Theorem | prod0 11606 |
A product over the empty set is one. (Contributed by Scott Fenton,
5-Dec-2017.)
|
β’ βπ β β
π΄ = 1 |
|
Theorem | prod1dc 11607* |
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 11608* |
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 11609* |
Re-index a finite product using a bijection. (Contributed by Scott
Fenton, 7-Dec-2017.)
|
β’ (π = πΊ β π΅ = π·)
& β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄)
& β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ)
& β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ = βπ β πΆ π·) |
|
Theorem | prodssdc 11610* |
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 11611* |
Change the index set to a subset in a finite sum. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
β’ (π β π΄ β π΅)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ (π β βπ β π΅ DECID π β π΄)
& β’ ((π β§ π β (π΅ β π΄)) β πΆ = 1) & β’ (π β π΅ β Fin) β β’ (π β βπ β π΄ πΆ = βπ β π΅ πΆ) |
|
Theorem | fprodmul 11612* |
The product of two finite products. (Contributed by Scott Fenton,
14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β)
β β’ (π β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |
|
Theorem | prodsnf 11613* |
A product of a singleton is the term. A version of prodsn 11614 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ΅
& β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β βπ β {π}π΄ = π΅) |
|
Theorem | prodsn 11614* |
A product of a singleton is the term. (Contributed by Scott Fenton,
14-Dec-2017.)
|
β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β βπ β {π}π΄ = π΅) |
|
Theorem | fprod1 11615* |
A finite product of only one term is the term itself. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
β’ (π = π β π΄ = π΅) β β’ ((π β β€ β§ π΅ β β) β βπ β (π...π)π΄ = π΅) |
|
Theorem | climprod1 11616 |
The limit of a product over one. (Contributed by Scott Fenton,
15-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€)
β β’ (π β seqπ( Β· , (π Γ {1})) β 1) |
|
Theorem | fprodsplitdc 11617* |
Split a finite product into two parts. New proofs should use
fprodsplit 11618 which is the same but with one fewer
hypothesis.
(Contributed by Scott Fenton, 16-Dec-2017.)
(New usage is discouraged.)
|
β’ (π β (π΄ β© π΅) = β
) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ (π β βπ β π DECID π β π΄)
& β’ ((π β§ π β π) β πΆ β β)
β β’ (π β βπ β π πΆ = (βπ β π΄ πΆ Β· βπ β π΅ πΆ)) |
|
Theorem | fprodsplit 11618* |
Split a finite product into two parts. (Contributed by Scott Fenton,
16-Dec-2017.)
|
β’ (π β (π΄ β© π΅) = β
) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β)
β β’ (π β βπ β π πΆ = (βπ β π΄ πΆ Β· βπ β π΅ πΆ)) |
|
Theorem | fprodm1 11619* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = (βπ β (π...(π β 1))π΄ Β· π΅)) |
|
Theorem | fprod1p 11620* |
Separate out the first term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = (π΅ Β· βπ β ((π + 1)...π)π΄)) |
|
Theorem | fprodp1 11621* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β βπ β (π...(π + 1))π΄ = (βπ β (π...π)π΄ Β· π΅)) |
|
Theorem | fprodm1s 11622* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β)
β β’ (π β βπ β (π...π)π΄ = (βπ β (π...(π β 1))π΄ Β· β¦π / πβ¦π΄)) |
|
Theorem | fprodp1s 11623* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β)
β β’ (π β βπ β (π...(π + 1))π΄ = (βπ β (π...π)π΄ Β· β¦(π + 1) / πβ¦π΄)) |
|
Theorem | prodsns 11624* |
A product of the singleton is the term. (Contributed by Scott Fenton,
25-Dec-2017.)
|
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β βπ β {π}π΄ = β¦π / πβ¦π΄) |
|
Theorem | fprodunsn 11625* |
Multiply in an additional term in a finite product. See also
fprodsplitsn 11654 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 11626* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π)
& β’ (π β π΄ β β
)
β β’ (π β βπ β π΄ π΅ β π) |
|
Theorem | fprodcllem 11627* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.)
|
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π)
& β’ (π β 1 β π) β β’ (π β βπ β π΄ π΅ β π) |
|
Theorem | fprodcl 11628* |
Closure of a finite product of complex numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodrecl 11629* |
Closure of a finite product of real numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodzcl 11630* |
Closure of a finite product of integers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€)
β β’ (π β βπ β π΄ π΅ β β€) |
|
Theorem | fprodnncl 11631* |
Closure of a finite product of positive integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodrpcl 11632* |
Closure of a finite product of positive reals. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β
β+) β β’ (π β βπ β π΄ π΅ β
β+) |
|
Theorem | fprodnn0cl 11633* |
Closure of a finite product of nonnegative integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β
β0) β β’ (π β βπ β π΄ π΅ β
β0) |
|
Theorem | fprodcllemf 11634* |
Finite product closure lemma. A version of fprodcllem 11627 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π)
& β’ (π β 1 β π) β β’ (π β βπ β π΄ π΅ β π) |
|
Theorem | fprodreclf 11635* |
Closure of a finite product of real numbers. A version of fprodrecl 11629
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodfac 11636* |
Factorial using product notation. (Contributed by Scott Fenton,
15-Dec-2017.)
|
β’ (π΄ β β0 β
(!βπ΄) = βπ β (1...π΄)π) |
|
Theorem | fprodabs 11637* |
The absolute value of a finite product. (Contributed by Scott Fenton,
25-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ ((π β§ π β π) β π΄ β β)
β β’ (π β (absββπ β (π...π)π΄) = βπ β (π...π)(absβπ΄)) |
|
Theorem | fprodeq0 11638* |
Any finite product containing a zero term is itself zero. (Contributed
by Scott Fenton, 27-Dec-2017.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π = π) β π΄ = 0) β β’ ((π β§ πΎ β (β€β₯βπ)) β βπ β (π...πΎ)π΄ = 0) |
|
Theorem | fprodshft 11639* |
Shift the index of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (π β πΎ) β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = βπ β ((π + πΎ)...(π + πΎ))π΅) |
|
Theorem | fprodrev 11640* |
Reversal of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = (πΎ β π) β π΄ = π΅) β β’ (π β βπ β (π...π)π΄ = βπ β ((πΎ β π)...(πΎ β π))π΅) |
|
Theorem | fprodconst 11641* |
The product of constant terms (π is not free in π΅).
(Contributed by Scott Fenton, 12-Jan-2018.)
|
β’ ((π΄ β Fin β§ π΅ β β) β βπ β π΄ π΅ = (π΅β(β―βπ΄))) |
|
Theorem | fprodap0 11642* |
A finite product of nonzero terms is nonzero. (Contributed by Scott
Fenton, 15-Jan-2018.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β π΅ # 0) β β’ (π β βπ β π΄ π΅ # 0) |
|
Theorem | fprod2dlemstep 11643* |
Lemma for fprod2d 11644- induction step. (Contributed by Scott
Fenton,
30-Jan-2018.)
|
β’ (π§ = β¨π, πβ© β π· = πΆ)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β) & β’ (π β Β¬ π¦ β π₯)
& β’ (π β (π₯ βͺ {π¦}) β π΄)
& β’ (π β π₯ β Fin) & β’ (π β βπ β π₯ βπ β π΅ πΆ = βπ§ β βͺ
π β π₯ ({π} Γ π΅)π·) β β’ ((π β§ π) β βπ β (π₯ βͺ {π¦})βπ β π΅ πΆ = βπ§ β βͺ
π β (π₯ βͺ {π¦})({π} Γ π΅)π·) |
|
Theorem | fprod2d 11644* |
Write a double product as a product over a two-dimensional region.
Compare fsum2d 11456. (Contributed by Scott Fenton,
30-Jan-2018.)
|
β’ (π§ = β¨π, πβ© β π· = πΆ)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΆ = βπ§ β βͺ
π β π΄ ({π} Γ π΅)π·) |
|
Theorem | fprodxp 11645* |
Combine two products into a single product over the cartesian product.
(Contributed by Scott Fenton, 1-Feb-2018.)
|
β’ (π§ = β¨π, πβ© β π· = πΆ)
& β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΆ = βπ§ β (π΄ Γ π΅)π·) |
|
Theorem | fprodcnv 11646* |
Transform a product region using the converse operation. (Contributed
by Scott Fenton, 1-Feb-2018.)
|
β’ (π₯ = β¨π, πβ© β π΅ = π·)
& β’ (π¦ = β¨π, πβ© β πΆ = π·)
& β’ (π β π΄ β Fin) & β’ (π β Rel π΄)
& β’ ((π β§ π₯ β π΄) β π΅ β β)
β β’ (π β βπ₯ β π΄ π΅ = βπ¦ β β‘ π΄πΆ) |
|
Theorem | fprodcom2fi 11647* |
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 11648* |
Interchange product order. (Contributed by Scott Fenton,
2-Feb-2018.)
|
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β β)
β β’ (π β βπ β π΄ βπ β π΅ πΆ = βπ β π΅ βπ β π΄ πΆ) |
|
Theorem | fprod0diagfz 11649* |
Two ways to express "the product of π΄(π, π) over the triangular
region π β€ π, π β€ π, π + π β€ π. Compare
fisum0diag 11462. (Contributed by Scott Fenton, 2-Feb-2018.)
|
β’ ((π β§ (π β (0...π) β§ π β (0...(π β π)))) β π΄ β β) & β’ (π β π β β€)
β β’ (π β βπ β (0...π)βπ β (0...(π β π))π΄ = βπ β (0...π)βπ β (0...(π β π))π΄) |
|
Theorem | fprodrec 11650* |
The finite product of reciprocals is the reciprocal of the product.
(Contributed by Jim Kingdon, 28-Aug-2024.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β π΅ # 0) β β’ (π β βπ β π΄ (1 / π΅) = (1 / βπ β π΄ π΅)) |
|
Theorem | fproddivap 11651* |
The quotient of two finite products. (Contributed by Scott Fenton,
15-Jan-2018.)
|
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β πΆ # 0) β β’ (π β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |
|
Theorem | fproddivapf 11652* |
The quotient of two finite products. A version of fproddivap 11651 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β πΆ # 0) β β’ (π β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |
|
Theorem | fprodsplitf 11653* |
Split a finite product into two parts. A version of fprodsplit 11618 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β (π΄ β© π΅) = β
) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β)
β β’ (π β βπ β π πΆ = (βπ β π΄ πΆ Β· βπ β π΅ πΆ)) |
|
Theorem | fprodsplitsn 11654* |
Separate out a term in a finite product. See also fprodunsn 11625 which is
the same but with a distinct variable condition in place of
β²ππ. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
β’ β²ππ
& β’ β²ππ·
& β’ (π β π΄ β Fin) & β’ (π β π΅ β π)
& β’ (π β Β¬ π΅ β π΄)
& β’ ((π β§ π β π΄) β πΆ β β) & β’ (π = π΅ β πΆ = π·)
& β’ (π β π· β β)
β β’ (π β βπ β (π΄ βͺ {π΅})πΆ = (βπ β π΄ πΆ Β· π·)) |
|
Theorem | fprodsplit1f 11655* |
Separate out a term in a finite product. (Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β β²ππ·)
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄)
& β’ ((π β§ π = πΆ) β π΅ = π·) β β’ (π β βπ β π΄ π΅ = (π· Β· βπ β (π΄ β {πΆ})π΅)) |
|
Theorem | fprodclf 11656* |
Closure of a finite product of complex numbers. A version of fprodcl 11628
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β)
β β’ (π β βπ β π΄ π΅ β β) |
|
Theorem | fprodap0f 11657* |
A finite product of terms apart from zero is apart from zero. A version
of fprodap0 11642 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 11658* |
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 11659* |
Any finite product containing a zero term is itself zero. (Contributed
by Glauco Siliprandi, 5-Apr-2020.)
|
β’ β²ππ
& β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄)
& β’ ((π β§ π = πΆ) β π΅ = 0) β β’ (π β βπ β π΄ π΅ = 0) |
|
Theorem | fprodge1 11660* |
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 11661* |
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 11662* |
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 11663 |
Extend class notation to include the exponential function.
|
class exp |
|
Syntax | ceu 11664 |
Extend class notation to include Euler's constant e =
2.71828....
|
class e |
|
Syntax | csin 11665 |
Extend class notation to include the sine function.
|
class sin |
|
Syntax | ccos 11666 |
Extend class notation to include the cosine function.
|
class cos |
|
Syntax | ctan 11667 |
Extend class notation to include the tangent function.
|
class tan |
|
Syntax | cpi 11668 |
Extend class notation to include the constant pi, Ο
= 3.14159....
|
class Ο |
|
Definition | df-ef 11669* |
Define the exponential function. Its value at the complex number π΄
is (expβπ΄) and is called the "exponential
of π΄"; see
efval 11682. (Contributed by NM, 14-Mar-2005.)
|
β’ exp = (π₯ β β β¦ Ξ£π β β0
((π₯βπ) / (!βπ))) |
|
Definition | df-e 11670 |
Define Euler's constant e = 2.71828.... (Contributed
by NM,
14-Mar-2005.)
|
β’ e = (expβ1) |
|
Definition | df-sin 11671 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
β’ sin = (π₯ β β β¦ (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) / (2 Β· i))) |
|
Definition | df-cos 11672 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
β’ cos = (π₯ β β β¦ (((expβ(i
Β· π₯)) +
(expβ(-i Β· π₯))) / 2)) |
|
Definition | df-tan 11673 |
Define the tangent function. We define it this way for cmpt 4076,
which
requires the form (π₯ β π΄ β¦ π΅). (Contributed by Mario
Carneiro, 14-Mar-2014.)
|
β’ tan = (π₯ β (β‘cos β (β β {0})) β¦
((sinβπ₯) /
(cosβπ₯))) |
|
Definition | df-pi 11674 |
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 11675 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
β’ ((π΄ β β β§ πΎ β β0) β ((π΄βπΎ) / (!βπΎ)) β β) |
|
Theorem | reeftcl 11676 |
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 11677 |
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 11678* |
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 11679* |
Lemma for efcl 11685. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11554 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 11680* |
Lemma for efcl 11685. 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 11681* |
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 11682* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 ((π΄βπ) / (!βπ))) |
|
Theorem | esum 11683 |
Value of Euler's constant e = 2.71828.... (Contributed
by Steve
Rodriguez, 5-Mar-2006.)
|
β’ e = Ξ£π β β0 (1 /
(!βπ)) |
|
Theorem | eff 11684 |
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 11685 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
β’ (π΄ β β β (expβπ΄) β
β) |
|
Theorem | efval2 11686* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 (πΉβπ)) |
|
Theorem | efcvg 11687* |
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 11688* |
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 11689 |
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 11690 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
β’ (π β π΄ β β)
β β’ (π β (expβπ΄) β β) |
|
Theorem | ere 11691 |
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 11692 |
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 11693 |
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 |
|
Theorem | efcj 11694 |
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.)
|
β’ (π΄ β β β
(expβ(ββπ΄)) = (ββ(expβπ΄))) |
|
Theorem | efaddlem 11695* |
Lemma for efadd 11696 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ πΊ = (π β β0 β¦ ((π΅βπ) / (!βπ))) & β’ π» = (π β β0 β¦ (((π΄ + π΅)βπ) / (!βπ))) & β’ (π β π΄ β β) & β’ (π β π΅ β β)
β β’ (π β (expβ(π΄ + π΅)) = ((expβπ΄) Β· (expβπ΅))) |
|
Theorem | efadd 11696 |
Sum of exponents law for exponential function. (Contributed by NM,
10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β (expβ(π΄ + π΅)) = ((expβπ΄) Β· (expβπ΅))) |
|
Theorem | efcan 11697 |
Cancellation law for exponential function. Equation 27 of [Rudin] p. 164.
(Contributed by NM, 13-Jan-2006.)
|
β’ (π΄ β β β ((expβπ΄) Β· (expβ-π΄)) = 1) |
|
Theorem | efap0 11698 |
The exponential of a complex number is apart from zero. (Contributed by
Jim Kingdon, 12-Dec-2022.)
|
β’ (π΄ β β β (expβπ΄) # 0) |
|
Theorem | efne0 11699 |
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 11698 (which will be more useful in most
contexts).
(Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
β’ (π΄ β β β (expβπ΄) β 0) |
|
Theorem | efneg 11700 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
β’ (π΄ β β β (expβ-π΄) = (1 / (expβπ΄))) |