Home | Metamath
Proof Explorer Theorem List (p. 139 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uzrdgxfr 13801* | Transfer the value of the recursive sequence builder from one base to another. (Contributed by Mario Carneiro, 1-Apr-2014.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) & β’ π» = (rec((π₯ β V β¦ (π₯ + 1)), π΅) βΎ Ο) & β’ π΄ β β€ & β’ π΅ β β€ β β’ (π β Ο β (πΊβπ) = ((π»βπ) + (π΄ β π΅))) | ||
Theorem | fzennn 13802 | The cardinality of a finite set of sequential integers. (See om2uz0i 13781 for a description of the hypothesis.) (Contributed by Mario Carneiro, 12-Feb-2013.) (Revised by Mario Carneiro, 7-Mar-2014.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β β’ (π β β0 β (1...π) β (β‘πΊβπ)) | ||
Theorem | fzen2 13803 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Mario Carneiro, 13-Feb-2014.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β β’ (π β (β€β₯βπ) β (π...π) β (β‘πΊβ((π + 1) β π))) | ||
Theorem | cardfz 13804 | The cardinality of a finite set of sequential integers. (See om2uz0i 13781 for a description of the hypothesis.) (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β β’ (π β β0 β (cardβ(1...π)) = (β‘πΊβπ)) | ||
Theorem | hashgf1o 13805 | πΊ maps Ο one-to-one onto β0. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 13-Sep-2013.) |
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β β’ πΊ:Οβ1-1-ontoββ0 | ||
Theorem | fzfi 13806 | A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) |
β’ (π...π) β Fin | ||
Theorem | fzfid 13807 | Commonly used special case of fzfi 13806. (Contributed by Mario Carneiro, 25-May-2014.) |
β’ (π β (π...π) β Fin) | ||
Theorem | fzofi 13808 | Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ (π..^π) β Fin | ||
Theorem | fsequb 13809* | The values of a finite real sequence have an upper bound. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
β’ (βπ β (π...π)(πΉβπ) β β β βπ₯ β β βπ β (π...π)(πΉβπ) < π₯) | ||
Theorem | fsequb2 13810* | The values of a finite real sequence have an upper bound. (Contributed by NM, 20-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
β’ (πΉ:(π...π)βΆβ β βπ₯ β β βπ¦ β ran πΉ π¦ β€ π₯) | ||
Theorem | fseqsupcl 13811 | The values of a finite real sequence have a supremum. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((π β (β€β₯βπ) β§ πΉ:(π...π)βΆβ) β sup(ran πΉ, β, < ) β β) | ||
Theorem | fseqsupubi 13812 | The values of a finite real sequence are bounded by their supremum. (Contributed by NM, 20-Sep-2005.) |
β’ ((πΎ β (π...π) β§ πΉ:(π...π)βΆβ) β (πΉβπΎ) β€ sup(ran πΉ, β, < )) | ||
Theorem | nn0ennn 13813 | The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.) |
β’ β0 β β | ||
Theorem | nnenom 13814 | The set of positive integers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers). (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ β β Ο | ||
Theorem | nnct 13815 | β is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
β’ β βΌ Ο | ||
Theorem | uzindi 13816* | Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
β’ (π β π΄ β π) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π) β§ βπ¦(π β (πΏ..^π ) β π)) β π) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π¦ β π = π) & β’ (π₯ = π΄ β π = π) β β’ (π β π) | ||
Theorem | axdc4uzlem 13817* | Lemma for axdc4uz 13818. (Contributed by Mario Carneiro, 8-Jan-2014.) (Revised by Mario Carneiro, 26-Dec-2014.) |
β’ π β β€ & β’ π = (β€β₯βπ) & β’ π΄ β V & β’ πΊ = (rec((π¦ β V β¦ (π¦ + 1)), π) βΎ Ο) & β’ π» = (π β Ο, π₯ β π΄ β¦ ((πΊβπ)πΉπ₯)) β β’ ((πΆ β π΄ β§ πΉ:(π Γ π΄)βΆ(π« π΄ β {β })) β βπ(π:πβΆπ΄ β§ (πβπ) = πΆ β§ βπ β π (πβ(π + 1)) β (ππΉ(πβπ)))) | ||
Theorem | axdc4uz 13818* | A version of axdc4 10326 that works on an upper set of integers instead of Ο. (Contributed by Mario Carneiro, 8-Jan-2014.) |
β’ π β β€ & β’ π = (β€β₯βπ) β β’ ((π΄ β π β§ πΆ β π΄ β§ πΉ:(π Γ π΄)βΆ(π« π΄ β {β })) β βπ(π:πβΆπ΄ β§ (πβπ) = πΆ β§ βπ β π (πβ(π + 1)) β (ππΉ(πβπ)))) | ||
Theorem | ssnn0fi 13819* | A subset of the nonnegative integers is finite if and only if there is a nonnegative integer so that all integers greater than this integer are not contained in the subset. (Contributed by AV, 3-Oct-2019.) |
β’ (π β β0 β (π β Fin β βπ β β0 βπ₯ β β0 (π < π₯ β π₯ β π))) | ||
Theorem | rabssnn0fi 13820* | A subset of the nonnegative integers defined by a restricted class abstraction is finite if there is a nonnegative integer so that for all integers greater than this integer the condition of the class abstraction is not fulfilled. (Contributed by AV, 3-Oct-2019.) |
β’ ({π₯ β β0 β£ π} β Fin β βπ β β0 βπ₯ β β0 (π < π₯ β Β¬ π)) | ||
Theorem | uzsinds 13821* | Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ β (β€β₯βπ) β (βπ¦ β (π...(π₯ β 1))π β π)) β β’ (π β (β€β₯βπ) β π) | ||
Theorem | nnsinds 13822* | Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ β β β (βπ¦ β (1...(π₯ β 1))π β π)) β β’ (π β β β π) | ||
Theorem | nn0sinds 13823* | Strong (or "total") induction principle over the nonnegative integers. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ β β0 β (βπ¦ β (0...(π₯ β 1))π β π)) β β’ (π β β0 β π) | ||
Theorem | fsuppmapnn0fiublem 13824* | Lemma for fsuppmapnn0fiub 13825 and fsuppmapnn0fiubex 13826. (Contributed by AV, 2-Oct-2019.) |
β’ π = βͺ π β π (π supp π) & β’ π = sup(π, β, < ) β β’ ((π β (π βm β0) β§ π β Fin β§ π β π) β ((βπ β π π finSupp π β§ π β β ) β π β β0)) | ||
Theorem | fsuppmapnn0fiub 13825* | If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0 and ending with the supremum of the union of the support of these functions. (Contributed by AV, 2-Oct-2019.) (Proof shortened by JJ, 2-Aug-2021.) |
β’ π = βͺ π β π (π supp π) & β’ π = sup(π, β, < ) β β’ ((π β (π βm β0) β§ π β Fin β§ π β π) β ((βπ β π π finSupp π β§ π β β ) β βπ β π (π supp π) β (0...π))) | ||
Theorem | fsuppmapnn0fiubex 13826* | If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0. (Contributed by AV, 2-Oct-2019.) |
β’ ((π β (π βm β0) β§ π β Fin β§ π β π) β (βπ β π π finSupp π β βπ β β0 βπ β π (π supp π) β (0...π))) | ||
Theorem | fsuppmapnn0fiub0 13827* | If all functions of a finite set of functions over the nonnegative integers are finitely supported, then all these functions are zero for all integers greater than a fixed integer. (Contributed by AV, 3-Oct-2019.) |
β’ ((π β (π βm β0) β§ π β Fin β§ π β π) β (βπ β π π finSupp π β βπ β β0 βπ β π βπ₯ β β0 (π < π₯ β (πβπ₯) = π))) | ||
Theorem | suppssfz 13828* | Condition for a function over the nonnegative integers to have a support contained in a finite set of sequential integers. (Contributed by AV, 9-Oct-2019.) |
β’ (π β π β π) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β π β β0) & β’ (π β βπ₯ β β0 (π < π₯ β (πΉβπ₯) = π)) β β’ (π β (πΉ supp π) β (0...π)) | ||
Theorem | fsuppmapnn0ub 13829* | If a function over the nonnegative integers is finitely supported, then there is an upper bound for the arguments resulting in nonzero values. (Contributed by AV, 6-Oct-2019.) |
β’ ((πΉ β (π βm β0) β§ π β π) β (πΉ finSupp π β βπ β β0 βπ₯ β β0 (π < π₯ β (πΉβπ₯) = π))) | ||
Theorem | fsuppmapnn0fz 13830* | If a function over the nonnegative integers is finitely supported, then there is an upper bound for a finite set of sequential integers containing the support of the function. (Contributed by AV, 30-Sep-2019.) (Proof shortened by AV, 6-Oct-2019.) |
β’ ((πΉ β (π βm β0) β§ π β π) β (πΉ finSupp π β βπ β β0 (πΉ supp π) β (0...π))) | ||
Theorem | mptnn0fsupp 13831* | A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 23-Dec-2019.) |
β’ (π β 0 β π) & β’ ((π β§ π β β0) β πΆ β π΅) & β’ (π β βπ β β0 βπ₯ β β0 (π < π₯ β β¦π₯ / πβ¦πΆ = 0 )) β β’ (π β (π β β0 β¦ πΆ) finSupp 0 ) | ||
Theorem | mptnn0fsuppd 13832* | A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 2-Dec-2019.) (Revised by AV, 23-Dec-2019.) |
β’ (π β 0 β π) & β’ ((π β§ π β β0) β πΆ β π΅) & β’ (π = π₯ β πΆ = π·) & β’ (π β βπ β β0 βπ₯ β β0 (π < π₯ β π· = 0 )) β β’ (π β (π β β0 β¦ πΆ) finSupp 0 ) | ||
Theorem | mptnn0fsuppr 13833* | A finitely supported mapping from the nonnegative integers fulfills certain conditions. (Contributed by AV, 3-Nov-2019.) (Revised by AV, 23-Dec-2019.) |
β’ (π β 0 β π) & β’ ((π β§ π β β0) β πΆ β π΅) & β’ (π β (π β β0 β¦ πΆ) finSupp 0 ) β β’ (π β βπ β β0 βπ₯ β β0 (π < π₯ β β¦π₯ / πβ¦πΆ = 0 )) | ||
Theorem | f13idfv 13834 | A one-to-one function with the domain { 0, 1 ,2 } in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
β’ π΄ = (0...2) β β’ (πΉ:π΄β1-1βπ΅ β (πΉ:π΄βΆπ΅ β§ ((πΉβ0) β (πΉβ1) β§ (πΉβ0) β (πΉβ2) β§ (πΉβ1) β (πΉβ2)))) | ||
Syntax | cseq 13835 | Extend class notation with recursive sequence builder. |
class seqπ( + , πΉ) | ||
Definition | df-seq 13836* |
Define a general-purpose operation that builds a recursive sequence
(i.e., a function on an upper integer set such as β or β0)
whose value at an index is a function of its previous value and the
value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by seq1 13848
and seqp1 13850.
Typically, those are the main theorems that would be used in practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation +, an input sequence πΉ with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence seq1( + , πΉ) with values 1, 3/2, 7/4, 15/8,.., so that (seq1( + , πΉ)β1) = 1, (seq1( + , πΉ)β2) = 3/2, etc. In other words, seqπ( + , πΉ) transforms a sequence πΉ into an infinite series. seqπ( + , πΉ) β 2 means "the sum of F(n) from n = M to infinity is 2". Since limits are unique (climuni 15369), by climdm 15371 the "sum of F(n) from n = 1 to infinity" can be expressed as ( β βseq1( + , πΉ)) (provided the sequence converges) and evaluates to 2 in this example. Internally, the rec function generates as its values a set of ordered pairs starting at β¨π, (πΉβπ)β©, with the first member of each pair incremented by one in each successive value. So, the range of rec is exactly the sequence we want, and we just extract the range (restricted to omega) and throw away the domain. This definition has its roots in a series of theorems from om2uz0i 13781 through om2uzf1oi 13787, originally proved by Raph Levien for use with df-exp 13897 and later generalized for arbitrary recursive sequences. Definition df-sum 15506 extracts the summation values from partial (finite) and complete (infinite) series. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 4-Sep-2013.) |
β’ seqπ( + , πΉ) = (rec((π₯ β V, π¦ β V β¦ β¨(π₯ + 1), (π¦ + (πΉβ(π₯ + 1)))β©), β¨π, (πΉβπ)β©) β Ο) | ||
Theorem | seqex 13837 | Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ seqπ( + , πΉ) β V | ||
Theorem | seqeq1 13838 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ (π = π β seqπ( + , πΉ) = seqπ( + , πΉ)) | ||
Theorem | seqeq2 13839 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ ( + = π β seqπ( + , πΉ) = seqπ(π, πΉ)) | ||
Theorem | seqeq3 13840 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ (πΉ = πΊ β seqπ( + , πΉ) = seqπ( + , πΊ)) | ||
Theorem | seqeq1d 13841 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π΄ = π΅) β β’ (π β seqπ΄( + , πΉ) = seqπ΅( + , πΉ)) | ||
Theorem | seqeq2d 13842 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π΄ = π΅) β β’ (π β seqπ(π΄, πΉ) = seqπ(π΅, πΉ)) | ||
Theorem | seqeq3d 13843 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π΄ = π΅) β β’ (π β seqπ( + , π΄) = seqπ( + , π΅)) | ||
Theorem | seqeq123d 13844 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π = π) & β’ (π β + = π) & β’ (π β πΉ = πΊ) β β’ (π β seqπ( + , πΉ) = seqπ(π, πΊ)) | ||
Theorem | nfseq 13845 | Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ β²π₯π & β’ β²π₯ + & β’ β²π₯πΉ β β’ β²π₯seqπ( + , πΉ) | ||
Theorem | seqval 13846* | Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ π = (rec((π₯ β V, π¦ β V β¦ β¨(π₯ + 1), (π₯(π§ β V, π€ β V β¦ (π€ + (πΉβ(π§ + 1))))π¦)β©), β¨π, (πΉβπ)β©) βΎ Ο) β β’ seqπ( + , πΉ) = ran π | ||
Theorem | seqfn 13847 | The sequence builder function is a function. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ (π β β€ β seqπ( + , πΉ) Fn (β€β₯βπ)) | ||
Theorem | seq1 13848 | Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ (π β β€ β (seqπ( + , πΉ)βπ) = (πΉβπ)) | ||
Theorem | seq1i 13849 | Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014.) |
β’ π β β€ & β’ (π β (πΉβπ) = π΄) β β’ (π β (seqπ( + , πΉ)βπ) = π΄) | ||
Theorem | seqp1 13850 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
β’ (π β (β€β₯βπ) β (seqπ( + , πΉ)β(π + 1)) = ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))) | ||
Theorem | seqexw 13851 | Weak version of seqex 13837 that holds without ax-rep 5241. A sequence builder exists when its binary operation input exists and its starting index is an integer. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ + β V & β’ π β β€ β β’ seqπ( + , πΉ) β V | ||
Theorem | seqp1d 13852 | Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by AV, 3-May-2024.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ πΎ = (π + 1) & β’ (π β (seqπ( + , πΉ)βπ) = π΄) & β’ (π β (πΉβπΎ) = π΅) β β’ (π β (seqπ( + , πΉ)βπΎ) = (π΄ + π΅)) | ||
Theorem | seqp1iOLD 13853 | Obsolete version of seqp1d 13852 as of 3-May-2024. Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (β€β₯βπ) & β’ π β π & β’ πΎ = (π + 1) & β’ (π β (seqπ( + , πΉ)βπ) = π΄) & β’ (π β (πΉβπΎ) = π΅) β β’ (π β (seqπ( + , πΉ)βπΎ) = (π΄ + π΅)) | ||
Theorem | seqm1 13854 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ ((π β β€ β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)β(π β 1)) + (πΉβπ))) | ||
Theorem | seqcl2 13855* | Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β (πΉβπ) β πΆ) & β’ ((π β§ (π₯ β πΆ β§ π¦ β π·)) β (π₯ + π¦) β πΆ) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β ((π + 1)...π)) β (πΉβπ₯) β π·) β β’ (π β (seqπ( + , πΉ)βπ) β πΆ) | ||
Theorem | seqf2 13856* | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β (πΉβπ) β πΆ) & β’ ((π β§ (π₯ β πΆ β§ π¦ β π·)) β (π₯ + π¦) β πΆ) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β (β€β₯β(π + 1))) β (πΉβπ₯) β π·) β β’ (π β seqπ( + , πΉ):πβΆπΆ) | ||
Theorem | seqcl 13857* | Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) β β’ (π β (seqπ( + , πΉ)βπ) β π) | ||
Theorem | seqf 13858* | Range of the recursive sequence builder (special case of seqf2 13856). (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) β β’ (π β seqπ( + , πΉ):πβΆπ) | ||
Theorem | seqfveq2 13859* | Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β (seqπ( + , πΉ)βπΎ) = (πΊβπΎ)) & β’ (π β π β (β€β₯βπΎ)) & β’ ((π β§ π β ((πΎ + 1)...π)) β (πΉβπ) = (πΊβπ)) β β’ (π β (seqπ( + , πΉ)βπ) = (seqπΎ( + , πΊ)βπ)) | ||
Theorem | seqfeq2 13860* | Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β (seqπ( + , πΉ)βπΎ) = (πΊβπΎ)) & β’ ((π β§ π β (β€β₯β(πΎ + 1))) β (πΉβπ) = (πΊβπ)) β β’ (π β (seqπ( + , πΉ) βΎ (β€β₯βπΎ)) = seqπΎ( + , πΊ)) | ||
Theorem | seqfveq 13861* | Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) = (πΊβπ)) β β’ (π β (seqπ( + , πΉ)βπ) = (seqπ( + , πΊ)βπ)) | ||
Theorem | seqfeq 13862* | Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β β€) & β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = (πΊβπ)) β β’ (π β seqπ( + , πΉ) = seqπ( + , πΊ)) | ||
Theorem | seqshft2 13863* | Shifting the index set of a sequence. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β πΎ β β€) & β’ ((π β§ π β (π...π)) β (πΉβπ) = (πΊβ(π + πΎ))) β β’ (π β (seqπ( + , πΉ)βπ) = (seq(π + πΎ)( + , πΊ)β(π + πΎ))) | ||
Theorem | seqres 13864 | Restricting its characteristic function to (β€β₯βπ) does not affect the seq function. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β β€ β seqπ( + , (πΉ βΎ (β€β₯βπ))) = seqπ( + , πΉ)) | ||
Theorem | serf 13865* | An infinite series of complex terms is a function from β to β. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β seqπ( + , πΉ):πβΆβ) | ||
Theorem | serfre 13866* | An infinite series of real numbers is a function from β to β. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β seqπ( + , πΉ):πβΆβ) | ||
Theorem | monoord 13867* | Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β€ (πΉβ(π + 1))) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | monoord2 13868* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | sermono 13869* | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-Jun-2013.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β π β (β€β₯βπΎ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β β) & β’ ((π β§ π₯ β ((πΎ + 1)...π)) β 0 β€ (πΉβπ₯)) β β’ (π β (seqπ( + , πΉ)βπΎ) β€ (seqπ( + , πΉ)βπ)) | ||
Theorem | seqsplit 13870* | Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π β (β€β₯βπΎ)) & β’ ((π β§ π₯ β (πΎ...π)) β (πΉβπ₯) β π) β β’ (π β (seqπΎ( + , πΉ)βπ) = ((seqπΎ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ))) | ||
Theorem | seq1p 13871* | Removing the first term from a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π β β€) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) β β’ (π β (seqπ( + , πΉ)βπ) = ((πΉβπ) + (seq(π + 1)( + , πΉ)βπ))) | ||
Theorem | seqcaopr3 13872* | Lemma for seqcaopr2 13873. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) & β’ ((π β§ π β (π...π)) β (πΊβπ) β π) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ)π(πΊβπ))) & β’ ((π β§ π β (π..^π)) β (((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ)) + ((πΉβ(π + 1))π(πΊβ(π + 1)))) = (((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))π((seqπ( + , πΊ)βπ) + (πΊβ(π + 1))))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ))) | ||
Theorem | seqcaopr2 13873* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β π) & β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ (π§ β π β§ π€ β π))) β ((π₯ππ§) + (π¦ππ€)) = ((π₯ + π¦)π(π§ + π€))) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) & β’ ((π β§ π β (π...π)) β (πΊβπ) β π) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ)π(πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ))) | ||
Theorem | seqcaopr 13874* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) & β’ ((π β§ π β (π...π)) β (πΊβπ) β π) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) + (seqπ( + , πΊ)βπ))) | ||
Theorem | seqf1olem2a 13875* | Lemma for seqf1o 13878. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΆ β π) & β’ (π β πΊ:π΄βΆπΆ) & β’ (π β πΎ β π΄) & β’ (π β (π...π) β π΄) β β’ (π β ((πΊβπΎ) + (seqπ( + , πΊ)βπ)) = ((seqπ( + , πΊ)βπ) + (πΊβπΎ))) | ||
Theorem | seqf1olem1 13876* | Lemma for seqf1o 13878. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΆ β π) & β’ (π β πΉ:(π...(π + 1))β1-1-ontoβ(π...(π + 1))) & β’ (π β πΊ:(π...(π + 1))βΆπΆ) & β’ π½ = (π β (π...π) β¦ (πΉβif(π < πΎ, π, (π + 1)))) & β’ πΎ = (β‘πΉβ(π + 1)) β β’ (π β π½:(π...π)β1-1-ontoβ(π...π)) | ||
Theorem | seqf1olem2 13877* | Lemma for seqf1o 13878. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΆ β π) & β’ (π β πΉ:(π...(π + 1))β1-1-ontoβ(π...(π + 1))) & β’ (π β πΊ:(π...(π + 1))βΆπΆ) & β’ π½ = (π β (π...π) β¦ (πΉβif(π < πΎ, π, (π + 1)))) & β’ πΎ = (β‘πΉβ(π + 1)) & β’ (π β βπβπ((π:(π...π)β1-1-ontoβ(π...π) β§ π:(π...π)βΆπΆ) β (seqπ( + , (π β π))βπ) = (seqπ( + , π)βπ))) β β’ (π β (seqπ( + , (πΊ β πΉ))β(π + 1)) = (seqπ( + , πΊ)β(π + 1))) | ||
Theorem | seqf1o 13878* | Rearrange a sum via an arbitrary bijection on (π...π). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΆ β π) & β’ (π β πΉ:(π...π)β1-1-ontoβ(π...π)) & β’ ((π β§ π₯ β (π...π)) β (πΊβπ₯) β πΆ) & β’ ((π β§ π β (π...π)) β (π»βπ) = (πΊβ(πΉβπ))) β β’ (π β (seqπ( + , π»)βπ) = (seqπ( + , πΊ)βπ)) | ||
Theorem | seradd 13879* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) + (seqπ( + , πΊ)βπ))) | ||
Theorem | sersub 13880* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) β (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ))) | ||
Theorem | seqid3 13881* | A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a + -idempotent sums (or "+'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) |
β’ (π β (π + π) = π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) = π) β β’ (π β (seqπ( + , πΉ)βπ) = π) | ||
Theorem | seqid 13882* | Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for +) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ π₯ β π) β (π + π₯) = π₯) & β’ (π β π β π) & β’ (π β π β (β€β₯βπ)) & β’ (π β (πΉβπ) β π) & β’ ((π β§ π₯ β (π...(π β 1))) β (πΉβπ₯) = π) β β’ (π β (seqπ( + , πΉ) βΎ (β€β₯βπ)) = seqπ( + , πΉ)) | ||
Theorem | seqid2 13883* | The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for +) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ π₯ β π) β (π₯ + π) = π₯) & β’ (π β πΎ β (β€β₯βπ)) & β’ (π β π β (β€β₯βπΎ)) & β’ (π β (seqπ( + , πΉ)βπΎ) β π) & β’ ((π β§ π₯ β ((πΎ + 1)...π)) β (πΉβπ₯) = π) β β’ (π β (seqπ( + , πΉ)βπΎ) = (seqπ( + , πΉ)βπ)) | ||
Theorem | seqhomo 13884* | Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π»β(π₯ + π¦)) = ((π»βπ₯)π(π»βπ¦))) & β’ ((π β§ π₯ β (π...π)) β (π»β(πΉβπ₯)) = (πΊβπ₯)) β β’ (π β (π»β(seqπ( + , πΉ)βπ)) = (seqπ(π, πΊ)βπ)) | ||
Theorem | seqz 13885* | If the operation + has an absorbing element π (a.k.a. zero element), then any sequence containing a π evaluates to π. (Contributed by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ ((π β§ π₯ β π) β (π + π₯) = π) & β’ ((π β§ π₯ β π) β (π₯ + π) = π) & β’ (π β πΎ β (π...π)) & β’ (π β π β π) & β’ (π β (πΉβπΎ) = π) β β’ (π β (seqπ( + , πΉ)βπ) = π) | ||
Theorem | seqfeq4 13886* | Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) = (π₯ππ¦)) β β’ (π β (seqπ( + , πΉ)βπ) = (seqπ(π, πΉ)βπ)) | ||
Theorem | seqfeq3 13887* | Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) |
β’ (π β π β β€) & β’ ((π β§ π₯ β (β€β₯βπ)) β (πΉβπ₯) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) = (π₯ππ¦)) β β’ (π β seqπ( + , πΉ) = seqπ(π, πΉ)) | ||
Theorem | seqdistr 13888* | The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΆπ(π₯ + π¦)) = ((πΆππ₯) + (πΆππ¦))) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΊβπ₯) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) = (πΆπ(πΊβπ₯))) β β’ (π β (seqπ( + , πΉ)βπ) = (πΆπ(seqπ( + , πΊ)βπ))) | ||
Theorem | ser0 13889 | The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013.) (Revised by Mario Carneiro, 15-Dec-2014.) |
β’ π = (β€β₯βπ) β β’ (π β π β (seqπ( + , (π Γ {0}))βπ) = 0) | ||
Theorem | ser0f 13890 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β seqπ( + , (π Γ {0})) = (π Γ {0})) | ||
Theorem | serge0 13891* | A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β 0 β€ (πΉβπ)) β β’ (π β 0 β€ (seqπ( + , πΉ)βπ)) | ||
Theorem | serle 13892* | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (πΉβπ) β€ (πΊβπ)) β β’ (π β (seqπ( + , πΉ)βπ) β€ (seqπ( + , πΊ)βπ)) | ||
Theorem | ser1const 13893 | Value of the partial series sum of a constant function. (Contributed by NM, 8-Aug-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
β’ ((π΄ β β β§ π β β) β (seq1( + , (β Γ {π΄}))βπ) = (π Β· π΄)) | ||
Theorem | seqof 13894* | Distribute function operation through a sequence. Note that πΊ(π§) is an implicit function on π§. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ (π β π΄ β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) = (π§ β π΄ β¦ (πΊβπ₯))) β β’ (π β (seqπ( βf + , πΉ)βπ) = (π§ β π΄ β¦ (seqπ( + , πΊ)βπ))) | ||
Theorem | seqof2 13895* | Distribute function operation through a sequence. Maps-to notation version of seqof 13894. (Contributed by Mario Carneiro, 7-Jul-2017.) |
β’ (π β π΄ β π) & β’ (π β π β (β€β₯βπ)) & β’ (π β (π...π) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π§ β π΄)) β π β π) β β’ (π β (seqπ( βf + , (π₯ β π΅ β¦ (π§ β π΄ β¦ π)))βπ) = (π§ β π΄ β¦ (seqπ( + , (π₯ β π΅ β¦ π))βπ))) | ||
Syntax | cexp 13896 | Extend class notation to include exponentiation of a complex number to an integer power. |
class β | ||
Definition | df-exp 13897* |
Define exponentiation to nonnegative integer powers. For example,
(5β2) = 25 (ex-exp 29180). Terminology: In general,
"exponentiation" is the operation of raising a
"base" π₯ to the power
of the "exponent" π¦, resulting in the "power"
(π₯βπ¦), also
called "x to the power of y". In this case, "integer
exponentiation" is
the operation of raising a complex "base" π₯ to the
power of an
integer π¦, resulting in the "integer
power" (π₯βπ¦).
This definition is not meant to be used directly; instead, exp0 13900 and expp1 13903 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0β0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134 (0exp0e1 13901). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3β-2) = (1 / 9) (ex-exp 29180). The case π₯ = 0, π¦ < 0 gives the value (1 / 0), so we will avoid this case in our theorems. For a definition of exponentiation including complex exponents see df-cxp 25835 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 25944. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.) |
β’ β = (π₯ β β, π¦ β β€ β¦ if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β Γ {π₯}))βπ¦), (1 / (seq1( Β· , (β Γ {π₯}))β-π¦))))) | ||
Theorem | expval 13898 | Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π β β€) β (π΄βπ) = if(π = 0, 1, if(0 < π, (seq1( Β· , (β Γ {π΄}))βπ), (1 / (seq1( Β· , (β Γ {π΄}))β-π))))) | ||
Theorem | expnnval 13899 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π β β) β (π΄βπ) = (seq1( Β· , (β Γ {π΄}))βπ)) | ||
Theorem | exp0 13900 | Value of a complex number raised to the 0th power. Note that under our definition, 0β0 = 1 (0exp0e1 13901) , following the convention used by Gleason. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
β’ (π΄ β β β (π΄β0) = 1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |