Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
24-Nov-2022 | cvgratnnlembern 10878 | Lemma for cvgratnn 10886. Upper bound for a geometric progression of positive ratio less than one. (Contributed by Jim Kingdon, 24-Nov-2022.) |
23-Nov-2022 | cvgratnnlemfm 10884 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 23-Nov-2022.) |
23-Nov-2022 | cvgratnnlemsumlt 10883 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 23-Nov-2022.) |
21-Nov-2022 | cvgratnnlemrate 10885 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 21-Nov-2022.) |
21-Nov-2022 | cvgratnnlemabsle 10882 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 21-Nov-2022.) |
21-Nov-2022 | cvgratnnlemseq 10881 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 21-Nov-2022.) |
15-Nov-2022 | cvgratnnlemmn 10880 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 15-Nov-2022.) |
15-Nov-2022 | cvgratnnlemnexp 10879 | Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 15-Nov-2022.) |
12-Nov-2022 | cvgratnn 10886 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. Although this theorem is similar to cvgratz 10887 and cvgratgt0 10888, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 10703 is sensitive to how a sequence is indexed. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 12-Nov-2022.) |
12-Nov-2022 | fsum3cvg 10731 | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 12-Nov-2022.) |
DECID | ||
12-Nov-2022 | seq3id2 9905 | 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 Jim Kingdon, 12-Nov-2022.) |
11-Nov-2022 | cvgratgt0 10888 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms beyond some index , then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.) |
11-Nov-2022 | cvgratz 10887 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.) |
4-Nov-2022 | seq3val 9839 | Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 9845, seq3-1 9842 and seq3p1 9849, 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 | ||
4-Nov-2022 | dfseq3-2 9820 |
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 9845,
seq3-1 9842 and
seq3p1 9849. 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 9818 and df-seq3 9819. (Contributed by NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
3-Nov-2022 | seq3f1o 9898 | Rearrange a sum via an arbitrary bijection on . (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 3-Nov-2022.) |
3-Nov-2022 | seq3m1 9854 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.) |
29-Oct-2022 | absgtap 10865 | Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
29-Oct-2022 | absltap 10864 | Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
29-Oct-2022 | 1ap2 8593 | 1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
28-Oct-2022 | expcnv 10859 | A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 28-Oct-2022.) |
28-Oct-2022 | expcnvre 10858 | A sequence of powers of a nonnegative real number less than one converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.) |
24-Oct-2022 | pwm1geoserap1 10863 | The n-th power of a number decreased by 1 expressed by the finite geometric series ... . (Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# | ||
24-Oct-2022 | geoserap 10862 | The value of the finite geometric series ... . This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# | ||
24-Oct-2022 | geosergap 10861 | The value of the finite geometric series ... . (Contributed by Mario Carneiro, 2-May-2016.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# ..^ | ||
23-Oct-2022 | expcnvap0 10857 | A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 23-Oct-2022.) |
# | ||
22-Oct-2022 | divcnv 10852 | The sequence of reciprocals of positive integers, multiplied by the factor , converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Jim Kingdon, 22-Oct-2022.) |
21-Oct-2022 | isumsplit 10847 | Split off the first terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.) |
21-Oct-2022 | seq3split 9872 | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.) |
20-Oct-2022 | fidcenumlemrk 6642 | Lemma for fidcenum 6644. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
20-Oct-2022 | fidcenumlemrks 6641 | Lemma for fidcenum 6644. Induction step for fidcenumlemrk 6642. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenum 6644 | A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenumlemr 6643 | Lemma for fidcenum 6644. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenumlemim 6640 | Lemma for fidcenum 6644. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
17-Oct-2022 | iser3shft 10699 | Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.) |
17-Oct-2022 | seq3shft 10237 | Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.) |
17-Oct-2022 | seq3shft2 9864 | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 17-Oct-2022.) |
16-Oct-2022 | resqrexlemf1 10406 | Lemma for resqrex 10424. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlemf 10405 | Lemma for resqrex 10424. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlemp1rp 10404 | Lemma for resqrex 10424. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 9845 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlem1arp 10403 | Lemma for resqrex 10424. is a positive real (expressed in a way that will help apply seqf 9845 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | seq3feq 9862 | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
15-Oct-2022 | inffz 11574 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
inf | ||
15-Oct-2022 | supfz 11573 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
12-Oct-2022 | fsumlessfi 10817 | A shorter sum of nonnegative terms is no greater than a longer one. (Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon, 12-Oct-2022.) |
12-Oct-2022 | modfsummodlemstep 10814 | Induction step for modfsummod 10815. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.) |
10-Oct-2022 | fsum3 10743 | The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | fsumgcl 10741 | Closure for a function used to describe a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | seq3distr 9911 | The distributive property for series. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | seq3homo 9909 | Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 10-Oct-2022.) |
8-Oct-2022 | fsum2dlemstep 10791 | Lemma for fsum2d 10792- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.) |
7-Oct-2022 | iunfidisj 6634 | The finite union of disjoint finite sets is finite. Note that depends on , i.e. can be thought of as . (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
7-Oct-2022 | disjnims 3829 | If a collection for is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
6-Oct-2022 | disjnim 3828 | If a collection for is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.) |
Disj | ||
5-Oct-2022 | dcun 3388 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) |
DECID DECID DECID | ||
4-Oct-2022 | ser3add 9900 | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 4-Oct-2022.) |
4-Oct-2022 | iseqseq3 9867 | Equality of and . (Contributed by Jim Kingdon, 4-Oct-2022.) |
3-Oct-2022 | ser3le 9918 | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Jim Kingdon, 3-Oct-2022.) |
3-Oct-2022 | seq3-1 9842 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.) |
3-Oct-2022 | df-seq3 9819 | Define a three-argument version of . By theorems such as iseqsst 9851, 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.) |
3-Oct-2022 | brrelex12i 4469 | Two classes that are related by a binary relation are sets. (An artifact of our ordered pair definition.) (Contributed by BJ, 3-Oct-2022.) |
1-Oct-2022 | fsum3ser 10754 | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 10769 and fsump1 10777, which should make our notation clear and from which, along with closure fsumcl 10757, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.) |
1-Oct-2022 | fisumser 10753 | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 10769 and fsump1 10777, which should make our notation clear and from which, along with closure fsumcl 10757, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.) Use fsum3ser 10754 instead. (New usage is discouraged.) |
1-Oct-2022 | tpfidisj 6618 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
28-Sep-2022 | seq3clss 9852 | Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.) |
27-Sep-2022 | zmaxcl 10621 | The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.) |
24-Sep-2022 | isumss2 10749 | Change the index set of a sum by adding zeroes. The nonzero elements are in the contained set and the added zeroes compose the rest of the containing set which needs to be summable. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.) |
DECID DECID | ||
24-Sep-2022 | preimaf1ofi 6639 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
24-Sep-2022 | ifmdc 3424 | If a conditional class is inhabited, then the condition is decidable. This shows that conditionals are not very useful unless one can prove the condition decidable. (Contributed by BJ, 24-Sep-2022.) |
DECID | ||
23-Sep-2022 | fisumss 10748 | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.) |
DECID | ||
21-Sep-2022 | pw1dom2 11546 | The power set of dominates . (Contributed by Jim Kingdon, 21-Sep-2022.) |
21-Sep-2022 | isumss 10747 | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 21-Sep-2022.) |
DECID DECID | ||
18-Sep-2022 | sumfct 10727 | A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.) |
16-Sep-2022 | isumz 10745 | Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 16-Sep-2022.) |
DECID | ||
16-Sep-2022 | fser0const 9916 | Simplifying an expression which turns out just to be a constant zero sequence. (Contributed by Jim Kingdon, 16-Sep-2022.) |
14-Sep-2022 | fisum 10742 | The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 14-Sep-2022.) Use fsum3 10743 instead. (New usage is discouraged.) |
10-Sep-2022 | isummo 10737 | A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 10-Sep-2022.) |
♯ DECID | ||
8-Sep-2022 | isummolem2 10736 | Lemma for isummo 10737. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 8-Sep-2022.) |
♯ DECID | ||
8-Sep-2022 | zfz1isolemiso 10209 | Lemma for zfz1iso 10211. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.) |
♯ ♯ ♯ ♯ ♯ | ||
8-Sep-2022 | zfz1isolemsplit 10208 | Lemma for zfz1iso 10211. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.) |
♯ ♯ ♯ | ||
7-Sep-2022 | zfz1isolem1 10210 | Lemma for zfz1iso 10211. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.) |
♯ ♯ | ||
6-Sep-2022 | fimaxq 10200 | A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.) |
5-Sep-2022 | fimax2gtri 6597 | A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.) |
5-Sep-2022 | fimax2gtrilemstep 6596 | Lemma for fimax2gtri 6597. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.) |
5-Sep-2022 | tridc 6595 | A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.) |
DECID | ||
3-Sep-2022 | isummolem2a 10735 | Lemma for isummo 10737. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 3-Sep-2022.) |
DECID ♯ ♯ | ||
3-Sep-2022 | zfz1iso 10211 | A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.) |
♯ | ||
1-Sep-2022 | ssidd 3043 | Weakening of ssid 3042. (Contributed by BJ, 1-Sep-2022.) |
31-Aug-2022 | fveqeq2 5298 | Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.) |
30-Aug-2022 | iseqf1olemfvp 9891 | Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 30-Aug-2022.) |
30-Aug-2022 | fveqeq2d 5297 | Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.) |
29-Aug-2022 | seq3f1olemqsumkj 9892 | Lemma for seq3f1o 9898. gives the same sum as in the range . (Contributed by Jim Kingdon, 29-Aug-2022.) |
..^ | ||
29-Aug-2022 | iseqf1olemqpcl 9890 | Lemma for seq3f1o 9898. A closure lemma involving and . (Contributed by Jim Kingdon, 29-Aug-2022.) |
29-Aug-2022 | iseqf1olemjpcl 9889 | Lemma for seq3f1o 9898. A closure lemma involving and . (Contributed by Jim Kingdon, 29-Aug-2022.) |
28-Aug-2022 | iseqf1olemqval 9881 | Lemma for seq3f1o 9898. Value of the function . (Contributed by Jim Kingdon, 28-Aug-2022.) |
27-Aug-2022 | iseqf1olemmo 9886 | Lemma for seq3f1o 9898. Showing that is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemnanb 9884 | Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemab 9883 | Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemnab 9882 | Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemqcl 9880 | Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.) |
Copyright terms: Public domain | W3C HTML validation [external] |