Home | Intuitionistic Logic Explorer Theorem List (p. 68 of 102) | < 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 | ltexprlemopu 6701* | The upper cut of our constructed difference is open. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemupu 6702* | The upper cut of our constructed difference is upper. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemrnd 6703* | Our constructed difference is rounded. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemdisj 6704* | Our constructed difference is disjoint. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemloc 6705* | Our constructed difference is located. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlempr 6706* | Our constructed difference is a positive real. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemfl 6707* | Lemma for ltexpri 6711. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemrl 6708* | Lemma for ltexpri 6711. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemfu 6709* | Lemma for ltexpri 6711. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemru 6710* | Lemma for ltexpri 6711. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexpri 6711* | Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) |
Theorem | addcanprleml 6712 | Lemma for addcanprg 6714. (Contributed by Jim Kingdon, 25-Dec-2019.) |
Theorem | addcanprlemu 6713 | Lemma for addcanprg 6714. (Contributed by Jim Kingdon, 25-Dec-2019.) |
Theorem | addcanprg 6714 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.) |
Theorem | lteupri 6715* | The difference from ltexpri 6711 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) |
Theorem | ltaprlem 6716 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) |
Theorem | ltaprg 6717 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.) |
Theorem | prplnqu 6718* | Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.) |
Theorem | addextpr 6719 | Strong extensionality of addition (ordering version). This is similar to addext 7601 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.) |
Theorem | recexprlemell 6720* | Membership in the lower cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemelu 6721* | Membership in the upper cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemm 6722* | is inhabited. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemopl 6723* | The lower cut of is open. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemlol 6724* | The lower cut of is lower. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemopu 6725* | The upper cut of is open. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemupu 6726* | The upper cut of is upper. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemrnd 6727* | is rounded. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemdisj 6728* | is disjoint. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemloc 6729* | is located. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlempr 6730* | is a positive real. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssl 6731* | The lower cut of one is a subset of the lower cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssu 6732* | The upper cut of one is a subset of the upper cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1l 6733* | The lower cut of is a subset of the lower cut of one. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1u 6734* | The upper cut of is a subset of the upper cut of one. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemex 6735* | is the reciprocal of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexpr 6736* | The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
Theorem | aptiprleml 6737 | Lemma for aptipr 6739. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptiprlemu 6738 | Lemma for aptipr 6739. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptipr 6739 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | ltmprr 6740 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
Theorem | archpr 6741* | For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer is embedded into the reals as described at nnprlu 6651. (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | caucvgprlemcanl 6742* | Lemma for cauappcvgprlemladdrl 6755. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
Theorem | cauappcvgprlemm 6743* | Lemma for cauappcvgpr 6760. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemopl 6744* | Lemma for cauappcvgpr 6760. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemlol 6745* | Lemma for cauappcvgpr 6760. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemopu 6746* | Lemma for cauappcvgpr 6760. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemupu 6747* | Lemma for cauappcvgpr 6760. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemrnd 6748* | Lemma for cauappcvgpr 6760. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemdisj 6749* | Lemma for cauappcvgpr 6760. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemloc 6750* | Lemma for cauappcvgpr 6760. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemcl 6751* | Lemma for cauappcvgpr 6760. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgprlemladdfu 6752* | Lemma for cauappcvgprlemladd 6756. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdfl 6753* | Lemma for cauappcvgprlemladd 6756. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdru 6754* | Lemma for cauappcvgprlemladd 6756. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdrl 6755* | Lemma for cauappcvgprlemladd 6756. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladd 6756* | Lemma for cauappcvgpr 6760. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem1 6757* | Lemma for cauappcvgpr 6760. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem2 6758* | Lemma for cauappcvgpr 6760. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlemlim 6759* | Lemma for cauappcvgpr 6760. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgpr 6760* |
A Cauchy approximation has a limit. A Cauchy approximation, here
, is similar
to a Cauchy sequence but is indexed by the desired
tolerance (that is, how close together terms needs to be) rather than
by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p.
(varies) with a few differences such as that we are proving the
existence of a limit without anything about how fast it converges
(that is, mere existence instead of existence, in HoTT terms), and
that the codomain of is
rather than . We
also
specify that every term needs to be larger than a fraction , to
avoid the case where we have positive terms which "converge"
to zero
(which is not a positive real).
This proof (including its lemmas) is similar to the proofs of caucvgpr 6780 and caucvgprpr 6810 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
Theorem | archrecnq 6761* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | archrecpr 6762* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprlemk 6763 | Lemma for caucvgpr 6780. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemnkj 6764* | Lemma for caucvgpr 6780. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
Theorem | caucvgprlemnbj 6765* | Lemma for caucvgpr 6780. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
Theorem | caucvgprlemm 6766* | Lemma for caucvgpr 6780. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemopl 6767* | Lemma for caucvgpr 6780. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemlol 6768* | Lemma for caucvgpr 6780. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemopu 6769* | Lemma for caucvgpr 6780. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemupu 6770* | Lemma for caucvgpr 6780. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemrnd 6771* | Lemma for caucvgpr 6780. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemdisj 6772* | Lemma for caucvgpr 6780. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemloc 6773* | Lemma for caucvgpr 6780. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemcl 6774* | Lemma for caucvgpr 6780. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
Theorem | caucvgprlemladdfu 6775* | Lemma for caucvgpr 6780. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemladdrl 6776* | Lemma for caucvgpr 6780. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
Theorem | caucvgprlem1 6777* | Lemma for caucvgpr 6780. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlem2 6778* | Lemma for caucvgpr 6780. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlemlim 6779* | Lemma for caucvgpr 6780. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
Theorem | caucvgpr 6780* |
A Cauchy sequence of positive fractions with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
of the nth term (it should later be able
to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a fraction , to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This proof (including its lemmas) is similar to the proofs of cauappcvgpr 6760 and caucvgprpr 6810. Reading cauappcvgpr 6760 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
Theorem | caucvgprprlemk 6781* | Lemma for caucvgprpr 6810. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
Theorem | caucvgprprlemloccalc 6782* | Lemma for caucvgprpr 6810. Rearranging some expressions for caucvgprprlemloc 6801. (Contributed by Jim Kingdon, 8-Feb-2021.) |
Theorem | caucvgprprlemell 6783* | Lemma for caucvgprpr 6810. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
Theorem | caucvgprprlemelu 6784* | Lemma for caucvgprpr 6810. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
Theorem | caucvgprprlemcbv 6785* | Lemma for caucvgprpr 6810. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemval 6786* | Lemma for caucvgprpr 6810. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
Theorem | caucvgprprlemnkltj 6787* | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkeqj 6788* | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnjltk 6789* | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkj 6790* | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
Theorem | caucvgprprlemnbj 6791* | Lemma for caucvgprpr 6810. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
Theorem | caucvgprprlemml 6792* | Lemma for caucvgprpr 6810. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemmu 6793* | Lemma for caucvgprpr 6810. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemm 6794* | Lemma for caucvgprpr 6810. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopl 6795* | Lemma for caucvgprpr 6810. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemlol 6796* | Lemma for caucvgprpr 6810. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopu 6797* | Lemma for caucvgprpr 6810. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemupu 6798* | Lemma for caucvgprpr 6810. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemrnd 6799* | Lemma for caucvgprpr 6810. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemdisj 6800* | Lemma for caucvgprpr 6810. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |