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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fzennn 13801 | The cardinality of a finite set of sequential integers. (See om2uz0i 13780 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 13802 | 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 13803 | The cardinality of a finite set of sequential integers. (See om2uz0i 13780 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 13804 | πΊ 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 13805 | A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) |
β’ (π...π) β Fin | ||
Theorem | fzfid 13806 | Commonly used special case of fzfi 13805. (Contributed by Mario Carneiro, 25-May-2014.) |
β’ (π β (π...π) β Fin) | ||
Theorem | fzofi 13807 | Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ (π..^π) β Fin | ||
Theorem | fsequb 13808* | 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 13809* | 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 13810 | 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 13811 | The values of a finite real sequence are bounded by their supremum. (Contributed by NM, 20-Sep-2005.) |
β’ ((πΎ β (π...π) β§ πΉ:(π...π)βΆβ) β (πΉβπΎ) β€ sup(ran πΉ, β, < )) | ||
Theorem | nn0ennn 13812 | The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.) |
β’ β0 β β | ||
Theorem | nnenom 13813 | 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 13814 | β is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
β’ β βΌ Ο | ||
Theorem | uzindi 13815* | Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
β’ (π β π΄ β π) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π) β§ βπ¦(π β (πΏ..^π ) β π)) β π) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π¦ β π = π) & β’ (π₯ = π΄ β π = π) β β’ (π β π) | ||
Theorem | axdc4uzlem 13816* | Lemma for axdc4uz 13817. (Contributed by Mario Carneiro, 8-Jan-2014.) (Revised by Mario Carneiro, 26-Dec-2014.) |
β’ π β β€ & β’ π = (β€β₯βπ) & β’ π΄ β V & β’ πΊ = (rec((π¦ β V β¦ (π¦ + 1)), π) βΎ Ο) & β’ π» = (π β Ο, π₯ β π΄ β¦ ((πΊβπ)πΉπ₯)) β β’ ((πΆ β π΄ β§ πΉ:(π Γ π΄)βΆ(π« π΄ β {β })) β βπ(π:πβΆπ΄ β§ (πβπ) = πΆ β§ βπ β π (πβ(π + 1)) β (ππΉ(πβπ)))) | ||
Theorem | axdc4uz 13817* | A version of axdc4 10325 that works on an upper set of integers instead of Ο. (Contributed by Mario Carneiro, 8-Jan-2014.) |
β’ π β β€ & β’ π = (β€β₯βπ) β β’ ((π΄ β π β§ πΆ β π΄ β§ πΉ:(π Γ π΄)βΆ(π« π΄ β {β })) β βπ(π:πβΆπ΄ β§ (πβπ) = πΆ β§ βπ β π (πβ(π + 1)) β (ππΉ(πβπ)))) | ||
Theorem | ssnn0fi 13818* | 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 13819* | 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 13820* | Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ β (β€β₯βπ) β (βπ¦ β (π...(π₯ β 1))π β π)) β β’ (π β (β€β₯βπ) β π) | ||
Theorem | nnsinds 13821* | Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ β β β (βπ¦ β (1...(π₯ β 1))π β π)) β β’ (π β β β π) | ||
Theorem | nn0sinds 13822* | Strong (or "total") induction principle over the nonnegative integers. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ β β0 β (βπ¦ β (0...(π₯ β 1))π β π)) β β’ (π β β0 β π) | ||
Theorem | fsuppmapnn0fiublem 13823* | Lemma for fsuppmapnn0fiub 13824 and fsuppmapnn0fiubex 13825. (Contributed by AV, 2-Oct-2019.) |
β’ π = βͺ π β π (π supp π) & β’ π = sup(π, β, < ) β β’ ((π β (π βm β0) β§ π β Fin β§ π β π) β ((βπ β π π finSupp π β§ π β β ) β π β β0)) | ||
Theorem | fsuppmapnn0fiub 13824* | 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 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. (Contributed by AV, 2-Oct-2019.) |
β’ ((π β (π βm β0) β§ π β Fin β§ π β π) β (βπ β π π finSupp π β βπ β β0 βπ β π (π supp π) β (0...π))) | ||
Theorem | fsuppmapnn0fiub0 13826* | 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 13827* | 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 13828* | 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 13829* | 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 13830* | 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 13831* | 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 13832* | 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 13833 | 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 13834 | Extend class notation with recursive sequence builder. |
class seqπ( + , πΉ) | ||
Definition | df-seq 13835* |
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 13847
and seqp1 13849.
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 15368), by climdm 15370 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 13780 through om2uzf1oi 13786, originally proved by Raph Levien for use with df-exp 13896 and later generalized for arbitrary recursive sequences. Definition df-sum 15505 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 13836 | Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ seqπ( + , πΉ) β V | ||
Theorem | seqeq1 13837 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ (π = π β seqπ( + , πΉ) = seqπ( + , πΉ)) | ||
Theorem | seqeq2 13838 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ ( + = π β seqπ( + , πΉ) = seqπ(π, πΉ)) | ||
Theorem | seqeq3 13839 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
β’ (πΉ = πΊ β seqπ( + , πΉ) = seqπ( + , πΊ)) | ||
Theorem | seqeq1d 13840 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π΄ = π΅) β β’ (π β seqπ΄( + , πΉ) = seqπ΅( + , πΉ)) | ||
Theorem | seqeq2d 13841 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π΄ = π΅) β β’ (π β seqπ(π΄, πΉ) = seqπ(π΅, πΉ)) | ||
Theorem | seqeq3d 13842 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π΄ = π΅) β β’ (π β seqπ( + , π΄) = seqπ( + , π΅)) | ||
Theorem | seqeq123d 13843 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
β’ (π β π = π) & β’ (π β + = π) & β’ (π β πΉ = πΊ) β β’ (π β seqπ( + , πΉ) = seqπ(π, πΊ)) | ||
Theorem | nfseq 13844 | Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ β²π₯π & β’ β²π₯ + & β’ β²π₯πΉ β β’ β²π₯seqπ( + , πΉ) | ||
Theorem | seqval 13845* | Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ π = (rec((π₯ β V, π¦ β V β¦ β¨(π₯ + 1), (π₯(π§ β V, π€ β V β¦ (π€ + (πΉβ(π§ + 1))))π¦)β©), β¨π, (πΉβπ)β©) βΎ Ο) β β’ seqπ( + , πΉ) = ran π | ||
Theorem | seqfn 13846 | 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 13847 | 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 13848 | Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014.) |
β’ π β β€ & β’ (π β (πΉβπ) = π΄) β β’ (π β (seqπ( + , πΉ)βπ) = π΄) | ||
Theorem | seqp1 13849 | 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 13850 | Weak version of seqex 13836 that holds without ax-rep 5240. 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 13851 | 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 13852 | Obsolete version of seqp1d 13851 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 13853 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ ((π β β€ β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)β(π β 1)) + (πΉβπ))) | ||
Theorem | seqcl2 13854* | 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 13855* | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β (πΉβπ) β πΆ) & β’ ((π β§ (π₯ β πΆ β§ π¦ β π·)) β (π₯ + π¦) β πΆ) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β (β€β₯β(π + 1))) β (πΉβπ₯) β π·) β β’ (π β seqπ( + , πΉ):πβΆπΆ) | ||
Theorem | seqcl 13856* | Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) β β’ (π β (seqπ( + , πΉ)βπ) β π) | ||
Theorem | seqf 13857* | Range of the recursive sequence builder (special case of seqf2 13855). (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) β β’ (π β seqπ( + , πΉ):πβΆπ) | ||
Theorem | seqfveq2 13858* | Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β (seqπ( + , πΉ)βπΎ) = (πΊβπΎ)) & β’ (π β π β (β€β₯βπΎ)) & β’ ((π β§ π β ((πΎ + 1)...π)) β (πΉβπ) = (πΊβπ)) β β’ (π β (seqπ( + , πΉ)βπ) = (seqπΎ( + , πΊ)βπ)) | ||
Theorem | seqfeq2 13859* | Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β (seqπ( + , πΉ)βπΎ) = (πΊβπΎ)) & β’ ((π β§ π β (β€β₯β(πΎ + 1))) β (πΉβπ) = (πΊβπ)) β β’ (π β (seqπ( + , πΉ) βΎ (β€β₯βπΎ)) = seqπΎ( + , πΊ)) | ||
Theorem | seqfveq 13860* | Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) = (πΊβπ)) β β’ (π β (seqπ( + , πΉ)βπ) = (seqπ( + , πΊ)βπ)) | ||
Theorem | seqfeq 13861* | Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β β€) & β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = (πΊβπ)) β β’ (π β seqπ( + , πΉ) = seqπ( + , πΊ)) | ||
Theorem | seqshft2 13862* | 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 13863 | 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 13864* | 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 13865* | 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 13866* | 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 13867* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | sermono 13868* | 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 13869* | 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 13870* | 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 13871* | Lemma for seqcaopr2 13872. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) & β’ ((π β§ π β (π...π)) β (πΊβπ) β π) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ)π(πΊβπ))) & β’ ((π β§ π β (π..^π)) β (((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ)) + ((πΉβ(π + 1))π(πΊβ(π + 1)))) = (((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))π((seqπ( + , πΊ)βπ) + (πΊβ(π + 1))))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ))) | ||
Theorem | seqcaopr2 13872* | 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 13873* | 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 13874* | Lemma for seqf1o 13877. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΆ β π) & β’ (π β πΊ:π΄βΆπΆ) & β’ (π β πΎ β π΄) & β’ (π β (π...π) β π΄) β β’ (π β ((πΊβπΎ) + (seqπ( + , πΊ)βπ)) = ((seqπ( + , πΊ)βπ) + (πΊβπΎ))) | ||
Theorem | seqf1olem1 13875* | Lemma for seqf1o 13877. (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 13876* | Lemma for seqf1o 13877. (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 13877* | 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 13878* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) + (seqπ( + , πΊ)βπ))) | ||
Theorem | sersub 13879* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) β (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ))) | ||
Theorem | seqid3 13880* | 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 13881* | 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 13882* | 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 13883* | Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π»β(π₯ + π¦)) = ((π»βπ₯)π(π»βπ¦))) & β’ ((π β§ π₯ β (π...π)) β (π»β(πΉβπ₯)) = (πΊβπ₯)) β β’ (π β (π»β(seqπ( + , πΉ)βπ)) = (seqπ(π, πΊ)βπ)) | ||
Theorem | seqz 13884* | 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 13885* | 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 13886* | 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 13887* | The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΆπ(π₯ + π¦)) = ((πΆππ₯) + (πΆππ¦))) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΊβπ₯) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) = (πΆπ(πΊβπ₯))) β β’ (π β (seqπ( + , πΉ)βπ) = (πΆπ(seqπ( + , πΊ)βπ))) | ||
Theorem | ser0 13888 | 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 13889 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β seqπ( + , (π Γ {0})) = (π Γ {0})) | ||
Theorem | serge0 13890* | 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 13891* | 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 13892 | 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 13893* | 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 13894* | Distribute function operation through a sequence. Maps-to notation version of seqof 13893. (Contributed by Mario Carneiro, 7-Jul-2017.) |
β’ (π β π΄ β π) & β’ (π β π β (β€β₯βπ)) & β’ (π β (π...π) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π§ β π΄)) β π β π) β β’ (π β (seqπ( βf + , (π₯ β π΅ β¦ (π§ β π΄ β¦ π)))βπ) = (π§ β π΄ β¦ (seqπ( + , (π₯ β π΅ β¦ π))βπ))) | ||
Syntax | cexp 13895 | Extend class notation to include exponentiation of a complex number to an integer power. |
class β | ||
Definition | df-exp 13896* |
Define exponentiation to nonnegative integer powers. For example,
(5β2) = 25 (ex-exp 29192). 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 13899 and expp1 13902 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 13900). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3β-2) = (1 / 9) (ex-exp 29192). 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 13897 | 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 13898 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π β β) β (π΄βπ) = (seq1( Β· , (β Γ {π΄}))βπ)) | ||
Theorem | exp0 13899 | Value of a complex number raised to the 0th power. Note that under our definition, 0β0 = 1 (0exp0e1 13900) , 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) | ||
Theorem | 0exp0e1 13900 | The zeroth power of zero equals one. See comment of exp0 13899. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (0β0) = 1 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |