Home | Intuitionistic Logic Explorer Theorem List (p. 69 of 108) | < 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 | ltexprlemfu 6801* | Lemma for ltexpri 6803. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemru 6802* | Lemma for ltexpri 6803. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexpri 6803* | Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) |
Theorem | addcanprleml 6804 | Lemma for addcanprg 6806. (Contributed by Jim Kingdon, 25-Dec-2019.) |
Theorem | addcanprlemu 6805 | Lemma for addcanprg 6806. (Contributed by Jim Kingdon, 25-Dec-2019.) |
Theorem | addcanprg 6806 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.) |
Theorem | lteupri 6807* | The difference from ltexpri 6803 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) |
Theorem | ltaprlem 6808 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) |
Theorem | ltaprg 6809 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.) |
Theorem | prplnqu 6810* | Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.) |
Theorem | addextpr 6811 | Strong extensionality of addition (ordering version). This is similar to addext 7710 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.) |
Theorem | recexprlemell 6812* | Membership in the lower cut of . Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemelu 6813* | Membership in the upper cut of . Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemm 6814* | is inhabited. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemopl 6815* | The lower cut of is open. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemlol 6816* | The lower cut of is lower. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemopu 6817* | The upper cut of is open. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemupu 6818* | The upper cut of is upper. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemrnd 6819* | is rounded. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemdisj 6820* | is disjoint. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemloc 6821* | is located. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlempr 6822* | is a positive real. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssl 6823* | The lower cut of one is a subset of the lower cut of . Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssu 6824* | The upper cut of one is a subset of the upper cut of . Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1l 6825* | The lower cut of is a subset of the lower cut of one. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1u 6826* | The upper cut of is a subset of the upper cut of one. Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemex 6827* | is the reciprocal of . Lemma for recexpr 6828. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexpr 6828* | 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 6829 | Lemma for aptipr 6831. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptiprlemu 6830 | Lemma for aptipr 6831. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptipr 6831 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | ltmprr 6832 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
Theorem | archpr 6833* | 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 6743. (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | caucvgprlemcanl 6834* | Lemma for cauappcvgprlemladdrl 6847. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
Theorem | cauappcvgprlemm 6835* | Lemma for cauappcvgpr 6852. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemopl 6836* | Lemma for cauappcvgpr 6852. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemlol 6837* | Lemma for cauappcvgpr 6852. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemopu 6838* | Lemma for cauappcvgpr 6852. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemupu 6839* | Lemma for cauappcvgpr 6852. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemrnd 6840* | Lemma for cauappcvgpr 6852. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemdisj 6841* | Lemma for cauappcvgpr 6852. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemloc 6842* | Lemma for cauappcvgpr 6852. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemcl 6843* | Lemma for cauappcvgpr 6852. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgprlemladdfu 6844* | Lemma for cauappcvgprlemladd 6848. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdfl 6845* | Lemma for cauappcvgprlemladd 6848. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdru 6846* | Lemma for cauappcvgprlemladd 6848. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdrl 6847* | Lemma for cauappcvgprlemladd 6848. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladd 6848* | Lemma for cauappcvgpr 6852. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem1 6849* | Lemma for cauappcvgpr 6852. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem2 6850* | Lemma for cauappcvgpr 6852. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlemlim 6851* | Lemma for cauappcvgpr 6852. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgpr 6852* |
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 6872 and caucvgprpr 6902 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
Theorem | archrecnq 6853* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | archrecpr 6854* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprlemk 6855 | Lemma for caucvgpr 6872. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemnkj 6856* | Lemma for caucvgpr 6872. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
Theorem | caucvgprlemnbj 6857* | Lemma for caucvgpr 6872. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
Theorem | caucvgprlemm 6858* | Lemma for caucvgpr 6872. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemopl 6859* | Lemma for caucvgpr 6872. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemlol 6860* | Lemma for caucvgpr 6872. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemopu 6861* | Lemma for caucvgpr 6872. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemupu 6862* | Lemma for caucvgpr 6872. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemrnd 6863* | Lemma for caucvgpr 6872. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemdisj 6864* | Lemma for caucvgpr 6872. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemloc 6865* | Lemma for caucvgpr 6872. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemcl 6866* | Lemma for caucvgpr 6872. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
Theorem | caucvgprlemladdfu 6867* | Lemma for caucvgpr 6872. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemladdrl 6868* | Lemma for caucvgpr 6872. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
Theorem | caucvgprlem1 6869* | Lemma for caucvgpr 6872. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlem2 6870* | Lemma for caucvgpr 6872. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlemlim 6871* | Lemma for caucvgpr 6872. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
Theorem | caucvgpr 6872* |
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 6852 and caucvgprpr 6902. Reading cauappcvgpr 6852 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
Theorem | caucvgprprlemk 6873* | Lemma for caucvgprpr 6902. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
Theorem | caucvgprprlemloccalc 6874* | Lemma for caucvgprpr 6902. Rearranging some expressions for caucvgprprlemloc 6893. (Contributed by Jim Kingdon, 8-Feb-2021.) |
Theorem | caucvgprprlemell 6875* | Lemma for caucvgprpr 6902. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
Theorem | caucvgprprlemelu 6876* | Lemma for caucvgprpr 6902. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
Theorem | caucvgprprlemcbv 6877* | Lemma for caucvgprpr 6902. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemval 6878* | Lemma for caucvgprpr 6902. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
Theorem | caucvgprprlemnkltj 6879* | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkeqj 6880* | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnjltk 6881* | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkj 6882* | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
Theorem | caucvgprprlemnbj 6883* | Lemma for caucvgprpr 6902. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
Theorem | caucvgprprlemml 6884* | Lemma for caucvgprpr 6902. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemmu 6885* | Lemma for caucvgprpr 6902. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemm 6886* | Lemma for caucvgprpr 6902. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopl 6887* | Lemma for caucvgprpr 6902. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemlol 6888* | Lemma for caucvgprpr 6902. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopu 6889* | Lemma for caucvgprpr 6902. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemupu 6890* | Lemma for caucvgprpr 6902. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemrnd 6891* | Lemma for caucvgprpr 6902. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemdisj 6892* | Lemma for caucvgprpr 6902. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemloc 6893* | Lemma for caucvgprpr 6902. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemcl 6894* | Lemma for caucvgprpr 6902. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.) |
Theorem | caucvgprprlemclphr 6895* | Lemma for caucvgprpr 6902. The putative limit is a positive real. Like caucvgprprlemcl 6894 but without a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Jun-2021.) |
Theorem | caucvgprprlemexbt 6896* | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.) |
Theorem | caucvgprprlemexb 6897* | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.) |
Theorem | caucvgprprlemaddq 6898* | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.) |
Theorem | caucvgprprlem1 6899* | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprprlem2 6900* | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |