Home | Intuitionistic Logic Explorer Theorem List (p. 75 of 133) | < 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 | ltnqpr 7401* | We can order fractions via or . (Contributed by Jim Kingdon, 19-Jun-2021.) |
Theorem | ltnqpri 7402* | We can order fractions via or . (Contributed by Jim Kingdon, 8-Jan-2021.) |
Theorem | ltpopr 7403 | Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 7404. (Contributed by Jim Kingdon, 15-Dec-2019.) |
Theorem | ltsopr 7404 | Positive real 'less than' is a weak linear order (in the sense of df-iso 4219). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.) |
Theorem | ltaddpr 7405 | The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
Theorem | ltexprlemell 7406* | Element in lower cut of the constructed difference. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemelu 7407* | Element in upper cut of the constructed difference. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemm 7408* | Our constructed difference is inhabited. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemopl 7409* | The lower cut of our constructed difference is open. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemlol 7410* | The lower cut of our constructed difference is lower. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemopu 7411* | The upper cut of our constructed difference is open. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemupu 7412* | The upper cut of our constructed difference is upper. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.) |
Theorem | ltexprlemrnd 7413* | Our constructed difference is rounded. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemdisj 7414* | Our constructed difference is disjoint. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemloc 7415* | Our constructed difference is located. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlempr 7416* | Our constructed difference is a positive real. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemfl 7417* | Lemma for ltexpri 7421. One direction of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemrl 7418* | Lemma for ltexpri 7421. Reverse direction of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemfu 7419* | Lemma for ltexpri 7421. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexprlemru 7420* | Lemma for ltexpri 7421. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
Theorem | ltexpri 7421* | Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) |
Theorem | addcanprleml 7422 | Lemma for addcanprg 7424. (Contributed by Jim Kingdon, 25-Dec-2019.) |
Theorem | addcanprlemu 7423 | Lemma for addcanprg 7424. (Contributed by Jim Kingdon, 25-Dec-2019.) |
Theorem | addcanprg 7424 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.) |
Theorem | lteupri 7425* | The difference from ltexpri 7421 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) |
Theorem | ltaprlem 7426 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) |
Theorem | ltaprg 7427 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.) |
Theorem | prplnqu 7428* | Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.) |
Theorem | addextpr 7429 | Strong extensionality of addition (ordering version). This is similar to addext 8372 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.) |
Theorem | recexprlemell 7430* | Membership in the lower cut of . Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemelu 7431* | Membership in the upper cut of . Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemm 7432* | is inhabited. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemopl 7433* | The lower cut of is open. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemlol 7434* | The lower cut of is lower. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemopu 7435* | The upper cut of is open. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemupu 7436* | The upper cut of is upper. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemrnd 7437* | is rounded. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemdisj 7438* | is disjoint. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemloc 7439* | is located. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlempr 7440* | is a positive real. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssl 7441* | The lower cut of one is a subset of the lower cut of . Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssu 7442* | The upper cut of one is a subset of the upper cut of . Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1l 7443* | The lower cut of is a subset of the lower cut of one. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1u 7444* | The upper cut of is a subset of the upper cut of one. Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemex 7445* | is the reciprocal of . Lemma for recexpr 7446. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexpr 7446* | 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 7447 | Lemma for aptipr 7449. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptiprlemu 7448 | Lemma for aptipr 7449. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptipr 7449 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | ltmprr 7450 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
Theorem | archpr 7451* | 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 7361. (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | caucvgprlemcanl 7452* | Lemma for cauappcvgprlemladdrl 7465. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
Theorem | cauappcvgprlemm 7453* | Lemma for cauappcvgpr 7470. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemopl 7454* | Lemma for cauappcvgpr 7470. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemlol 7455* | Lemma for cauappcvgpr 7470. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemopu 7456* | Lemma for cauappcvgpr 7470. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemupu 7457* | Lemma for cauappcvgpr 7470. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemrnd 7458* | Lemma for cauappcvgpr 7470. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemdisj 7459* | Lemma for cauappcvgpr 7470. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemloc 7460* | Lemma for cauappcvgpr 7470. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemcl 7461* | Lemma for cauappcvgpr 7470. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgprlemladdfu 7462* | Lemma for cauappcvgprlemladd 7466. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdfl 7463* | Lemma for cauappcvgprlemladd 7466. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdru 7464* | Lemma for cauappcvgprlemladd 7466. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdrl 7465* | Lemma for cauappcvgprlemladd 7466. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladd 7466* | Lemma for cauappcvgpr 7470. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem1 7467* | Lemma for cauappcvgpr 7470. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem2 7468* | Lemma for cauappcvgpr 7470. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlemlim 7469* | Lemma for cauappcvgpr 7470. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgpr 7470* |
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 7490 and caucvgprpr 7520 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
Theorem | archrecnq 7471* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | archrecpr 7472* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprlemk 7473 | Lemma for caucvgpr 7490. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemnkj 7474* | Lemma for caucvgpr 7490. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
Theorem | caucvgprlemnbj 7475* | Lemma for caucvgpr 7490. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
Theorem | caucvgprlemm 7476* | Lemma for caucvgpr 7490. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemopl 7477* | Lemma for caucvgpr 7490. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemlol 7478* | Lemma for caucvgpr 7490. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemopu 7479* | Lemma for caucvgpr 7490. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemupu 7480* | Lemma for caucvgpr 7490. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemrnd 7481* | Lemma for caucvgpr 7490. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemdisj 7482* | Lemma for caucvgpr 7490. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemloc 7483* | Lemma for caucvgpr 7490. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemcl 7484* | Lemma for caucvgpr 7490. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
Theorem | caucvgprlemladdfu 7485* | Lemma for caucvgpr 7490. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemladdrl 7486* | Lemma for caucvgpr 7490. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
Theorem | caucvgprlem1 7487* | Lemma for caucvgpr 7490. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlem2 7488* | Lemma for caucvgpr 7490. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlemlim 7489* | Lemma for caucvgpr 7490. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
Theorem | caucvgpr 7490* |
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 7470 and caucvgprpr 7520. Reading cauappcvgpr 7470 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
Theorem | caucvgprprlemk 7491* | Lemma for caucvgprpr 7520. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
Theorem | caucvgprprlemloccalc 7492* | Lemma for caucvgprpr 7520. Rearranging some expressions for caucvgprprlemloc 7511. (Contributed by Jim Kingdon, 8-Feb-2021.) |
Theorem | caucvgprprlemell 7493* | Lemma for caucvgprpr 7520. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
Theorem | caucvgprprlemelu 7494* | Lemma for caucvgprpr 7520. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
Theorem | caucvgprprlemcbv 7495* | Lemma for caucvgprpr 7520. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemval 7496* | Lemma for caucvgprpr 7520. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
Theorem | caucvgprprlemnkltj 7497* | Lemma for caucvgprpr 7520. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkeqj 7498* | Lemma for caucvgprpr 7520. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnjltk 7499* | Lemma for caucvgprpr 7520. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkj 7500* | Lemma for caucvgprpr 7520. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |