Home | Intuitionistic Logic Explorer Theorem List (p. 99 of 119) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | frec2uzf1od 9801* | (see frec2uz0d 9794) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.) |
frec | ||
Theorem | frec2uzisod 9802* | (see frec2uz0d 9794) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.) |
frec | ||
Theorem | frecuzrdgrrn 9803* | The function (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of . (Contributed by Jim Kingdon, 28-Mar-2022.) |
frec frec | ||
Theorem | frec2uzrdg 9804* | A helper lemma for the value of a recursive definition generator on upper integers (typically either or ) with characteristic function and initial value . This lemma shows that evaluating at an element of gives an ordered pair whose first element is the index (translated from to ). See comment in frec2uz0d 9794 which describes and the index translation. (Contributed by Jim Kingdon, 24-May-2020.) |
frec frec | ||
Theorem | frecuzrdgrcl 9805* | The function (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 1-Apr-2022.) |
frec frec | ||
Theorem | frecuzrdglem 9806* | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.) |
frec frec | ||
Theorem | frecuzrdgtcl 9807* | The recursive definition generator on upper integers is a function. See comment in frec2uz0d 9794 for the description of as the mapping from to . (Contributed by Jim Kingdon, 26-May-2020.) |
frec frec | ||
Theorem | frecuzrdg0 9808* | Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 9794 for the description of as the mapping from to . (Contributed by Jim Kingdon, 27-May-2020.) |
frec frec | ||
Theorem | frecuzrdgsuc 9809* | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 9794 for the description of as the mapping from to . (Contributed by Jim Kingdon, 28-May-2020.) |
frec frec | ||
Theorem | frecuzrdgrclt 9810* | The function (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of . Similar to frecuzrdgrcl 9805 except that and need not be the same. (Contributed by Jim Kingdon, 22-Apr-2022.) |
frec | ||
Theorem | frecuzrdgg 9811* | Lemma for other theorems involving the the recursive definition generator on upper integers. Evaluating at a natural number gives an ordered pair whose first element is the mapping of that natural number via . (Contributed by Jim Kingdon, 23-Apr-2022.) |
frec frec | ||
Theorem | frecuzrdgdomlem 9812* | The domain of the result of the recursive definition generator on upper integers. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec frec | ||
Theorem | frecuzrdgdom 9813* | The domain of the result of the recursive definition generator on upper integers. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec | ||
Theorem | frecuzrdgfunlem 9814* | The recursive definition generator on upper integers produces a a function. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec frec | ||
Theorem | frecuzrdgfun 9815* | The recursive definition generator on upper integers produces a a function. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec | ||
Theorem | frecuzrdgtclt 9816* | The recursive definition generator on upper integers is a function. (Contributed by Jim Kingdon, 22-Apr-2022.) |
frec | ||
Theorem | frecuzrdg0t 9817* | Initial value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 28-Apr-2022.) |
frec | ||
Theorem | frecuzrdgsuctlem 9818* | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 9794 for the description of as the mapping from to . (Contributed by Jim Kingdon, 29-Apr-2022.) |
frec frec | ||
Theorem | frecuzrdgsuct 9819* | Successor value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 29-Apr-2022.) |
frec | ||
Theorem | uzenom 9820 | An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.) |
Theorem | frecfzennn 9821 | The cardinality of a finite set of sequential integers. (See frec2uz0d 9794 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.) |
frec | ||
Theorem | frecfzen2 9822 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.) |
frec | ||
Theorem | frechashgf1o 9823 | maps one-to-one onto . (Contributed by Jim Kingdon, 19-May-2020.) |
frec | ||
Theorem | frec2uzled 9824* | The mapping (see frec2uz0d 9794) preserves order. (Contributed by Jim Kingdon, 24-Feb-2022.) |
frec | ||
Theorem | fzfig 9825 | A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.) |
Theorem | fzfigd 9826 | Deduction form of fzfig 9825. (Contributed by Jim Kingdon, 21-May-2020.) |
Theorem | fzofig 9827 | Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.) |
..^ | ||
Theorem | nn0ennn 9828 | The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.) |
Theorem | nnenom 9829 | 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 9830 | is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
Theorem | fnn0nninf 9831* | A function from into ℕ_{∞}. (Contributed by Jim Kingdon, 16-Jul-2022.) |
frec ℕ_{∞} | ||
Theorem | fxnn0nninf 9832* | A function from NN0* into ℕ_{∞}. (Contributed by Jim Kingdon, 16-Jul-2022.) |
frec NN0*ℕ_{∞} | ||
Theorem | 0tonninf 9833* | The mapping of zero into ℕ_{∞} is the sequence of all zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
Theorem | 1tonninf 9834* | The mapping of one into ℕ_{∞} is a sequence which is a one followed by zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
Theorem | inftonninf 9835* | The mapping of into ℕ_{∞} is the sequence of all ones. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
Theorem | uzsinds 9836* | Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.) |
Theorem | nnsinds 9837* | Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.) |
Theorem | nn0sinds 9838* | Strong (or "total") induction principle over the nonnegative integers. (Contributed by Scott Fenton, 16-May-2014.) |
Syntax | cseq4 9839 | Extend class notation with four-argument recursive sequence builder. |
Syntax | cseq 9840 | Extend class notation with three-argument recursive sequence builder. |
Definition | df-iseq 9841* |
Define a general-purpose operation that builds a recursive sequence
(i.e., a function on an upper integer set such as or )
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 iseq1 9863 and iseqp1 9870.
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 with values 1, 3/2, 7/4, 15/8,.., so that , 3/2, etc. In other words, transforms a sequence into an infinite series. Internally, the frec 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 frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.) Use df-seq3 9842 or dfseq3-2 9843 instead. (New usage is discouraged.) |
frec | ||
Definition | df-seq3 9842 | Define a three-argument version of . By theorems such as iseqsst 9874, it should be capable of doing pretty much everything that the four-argument version can, and may eventually replace the four-argument version entirely. (Contributed by Jim Kingdon, 3-Oct-2022.) |
Theorem | dfseq3-2 9843* |
Define a general-purpose operation that builds a recursive sequence
(i.e., a function on an upper integer set such as or )
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 seqf 9868,
seq3-1 9865 and
seq3p1 9872. 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 with values 1, 3/2, 7/4, 15/8,.., so that , 3/2, etc. In other words, transforms a sequence into an infinite series. Internally, the frec 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 frec is exactly the sequence we want, and we just extract the range and throw away the domain. Eventually, this will be the definition of , replacing df-iseq 9841 and df-seq3 9842. (Contributed by NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
Theorem | iseqex 9844 |
Existence of the sequence builder operation.
New proofs should use seqex 9845 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 20-Aug-2021.) (New usage is discouraged.) |
Theorem | seqex 9845 | Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
Theorem | iseqeq1 9846 |
Equality theorem for the sequence builder operation.
New proofs should use seqeq1 9849 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 30-May-2020.) (New usage is discouraged.) |
Theorem | iseqeq2 9847 |
Equality theorem for the sequence builder operation.
New proofs should use seqeq2 9850 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 30-May-2020.) (New usage is discouraged.) |
Theorem | iseqeq3 9848 |
Equality theorem for the sequence builder operation.
New proofs should use seqeq3 9851 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 30-May-2020.) (New usage is discouraged.) |
Theorem | seqeq1 9849 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
Theorem | seqeq2 9850 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
Theorem | seqeq3 9851 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
Theorem | seqeq1d 9852 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
Theorem | seqeq2d 9853 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
Theorem | seqeq3d 9854 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
Theorem | seqeq123d 9855 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
Theorem | nfiseq 9856 |
Hypothesis builder for the sequence builder operation.
New proofs should use nfseq 9857 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 30-May-2020.) (New usage is discouraged.) |
Theorem | nfseq 9857 | Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | iseqovex 9858* | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
Theorem | iseqval 9859* |
Value of the sequence builder function.
There should be no need for new usages of this theorem because once we have proved theorems seqf 9868, seq3-1 9865 and seq3p1 9872 future development can be done in terms of those. (Contributed by Jim Kingdon, 30-May-2020.) (New usage is discouraged.) |
frec | ||
Theorem | iseqvalcbv 9860* | Changing the bound variables in an expression which appears in some related proofs. (Contributed by Jim Kingdon, 28-Apr-2022.) |
frec frec | ||
Theorem | iseqvalt 9861* |
Value of the sequence builder function.
There should be no need for new usages of this theorem because once we have proved theorems seqf 9868, seq3-1 9865 and seq3p1 9872 future development can be done in terms of those. (Contributed by Jim Kingdon, 27-Apr-2022.) (New usage is discouraged.) |
frec | ||
Theorem | seq3val 9862* | Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 9868, seq3-1 9865 and seq3p1 9872, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
Theorem | iseq1 9863* |
Value of the sequence builder function at its initial value.
New proofs should use seq3-1 9865 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 31-May-2020.) (New usage is discouraged.) |
Theorem | iseq1t 9864* |
Value of the sequence builder function at its initial value.
New proofs should use seq3-1 9865 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 31-May-2020.) (New usage is discouraged.) |
Theorem | seq3-1 9865* | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.) |
Theorem | iseqfcl 9866* | Range of the recursive sequence builder. New proofs should use seqf 9868 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 11-Apr-2022.) (New usage is discouraged.) |
Theorem | iseqfclt 9867* |
Range of the recursive sequence builder.
New proofs should use seqf 9868 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 26-Apr-2022.) (New usage is discouraged.) |
Theorem | seqf 9868* | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) |
Theorem | iseqcl 9869* |
Closure property of the recursive sequence builder.
New proofs should use seqf 9868 or seq3clss 9875 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 1-Jun-2020.) (New usage is discouraged.) |
Theorem | iseqp1 9870* |
Value of the sequence builder function at a successor.
New proofs should use seq3p1 9872 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 31-May-2020.) (New usage is discouraged.) |
Theorem | iseqp1t 9871* |
Value of the sequence builder function at a successor.
New proofs should use seq3p1 9872 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 30-Apr-2022.) (New usage is discouraged.) |
Theorem | seq3p1 9872* | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 30-Apr-2022.) |
Theorem | iseqoveq 9873* |
Equality theorem for the sequence builder operation. This is similar to
iseqeq2 9847 but and only have to agree on elements of .
We intend to replace it with seqfeq3 from the Metamath Proof Explorer, which is why new usages are discouraged. (Contributed by Jim Kingdon, 21-Apr-2022.) (New usage is discouraged.) |
Theorem | iseqsst 9874* |
Specifying a larger universe for . As long as and
are closed over , then any class which contains can be used
as the last argument to .
Together with df-seq3 9842 it can be used to convert between the df-iseq 9841 syntax and the df-seq3 9842 syntax (in many cases iseqseq3 9890 is an even more convenient way to do this). (Contributed by Jim Kingdon, 28-Apr-2022.) |
Theorem | seq3clss 9875* | Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.) |
Theorem | iseqm1 9876* | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) Use seq3m1 9877 instead. (New usage is discouraged.) |
Theorem | seq3m1 9877* | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.) |
Theorem | iseqfveq2 9878* | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) Use seq3fveq2 9880 instead. (New usage is discouraged.) |
Theorem | iseqfeq2 9879* | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) Use seq3feq2 9881 instead. (New usage is discouraged.) |
Theorem | seq3fveq2 9880* | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
Theorem | seq3feq2 9881* | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
Theorem | iseqfveq 9882* | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) Use seq3fveq 9883 instead. (New usage is discouraged.) |
Theorem | seq3fveq 9883* | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) |
Theorem | iseqfeq 9884* |
Equality of sequences.
New proofs should use seq3feq 9885 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 15-Aug-2021.) (New usage is discouraged.) |
Theorem | seq3feq 9885* | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | iseqshft2 9886* |
Shifting the index set of a sequence.
New proofs should use seq3shft2 9887 instead (together with iseqsst 9874 or iseqseq3 9890 if need be). (Contributed by Jim Kingdon, 15-Aug-2021.) (New usage is discouraged.) |
Theorem | seq3shft2 9887* | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 17-Oct-2022.) |
Theorem | serf 9888* | An infinite series of complex terms is a function from to . (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
Theorem | serfre 9889* | An infinite series of real numbers is a function from to . (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
Theorem | iseqseq3 9890* | Equality of and . (Contributed by Jim Kingdon, 4-Oct-2022.) |
Theorem | iserf 9891* | An infinite series of complex terms is a function from to . (Contributed by Jim Kingdon, 15-Aug-2021.) Use serf 9888 instead. (New usage is discouraged.) |
Theorem | monoord 9892* | Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
Theorem | monoord2 9893* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.) |
Theorem | isermono 9894* | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) |
Theorem | seq3split 9895* | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.) |
Theorem | iseqsplit 9896* | Split a sequence into two sequences. New proofs should use seq3split 9895 instead. (Contributed by Jim Kingdon, 16-Aug-2021.) (New usage is discouraged.) |
Theorem | seq3-1p 9897* | Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.) |
Theorem | iseqcaopr3 9898* | Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.) |
..^ | ||
Theorem | iseqcaopr2 9899* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) |
Theorem | iseqcaopr 9900* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Jim Kingdon, 17-Aug-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |