HomeTheorem List (p. 78 of 156)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 78 of 156) | < 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 | aptipr 7701 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
     ![/\](wedge.gif "/\"){kind=small}      
 | ||
| Theorem | ltmprr 7702 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
 
| ||
| Theorem | archpr 7703* |
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 7613. (Contributed by Jim
Kingdon, 22-Apr-2020.)
|
      
    ![]](rbrack.gif "]"){kind=small}    | ||
| Theorem | caucvgprlemcanl 7704* | Lemma for cauappcvgprlemladdrl 7717. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
        
  
| ||
| Theorem | cauappcvgprlemm 7705* | Lemma for cauappcvgpr 7722. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
     
 | ||
| Theorem | cauappcvgprlemopl 7706* | Lemma for cauappcvgpr 7722. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
|
| ||
| Theorem | cauappcvgprlemlol 7707* | Lemma for cauappcvgpr 7722. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
|
| ||
| Theorem | cauappcvgprlemopu 7708* | Lemma for cauappcvgpr 7722. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
|
| ||
| Theorem | cauappcvgprlemupu 7709* | Lemma for cauappcvgpr 7722. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
|
| ||
| Theorem | cauappcvgprlemrnd 7710* | Lemma for cauappcvgpr 7722. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
|
| ||
| Theorem | cauappcvgprlemdisj 7711* | Lemma for cauappcvgpr 7722. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
|
| ||
| Theorem | cauappcvgprlemloc 7712* | Lemma for cauappcvgpr 7722. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
|
| ||
| Theorem | cauappcvgprlemcl 7713* | Lemma for cauappcvgpr 7722. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
|
| ||
| Theorem | cauappcvgprlemladdfu 7714* | Lemma for cauappcvgprlemladd 7718. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| ||
| Theorem | cauappcvgprlemladdfl 7715* | Lemma for cauappcvgprlemladd 7718. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
|
| ||
| Theorem | cauappcvgprlemladdru 7716* | Lemma for cauappcvgprlemladd 7718. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
|
| ||
| Theorem | cauappcvgprlemladdrl 7717* | Lemma for cauappcvgprlemladd 7718. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
|
| ||
| Theorem | cauappcvgprlemladd 7718* |
Lemma for cauappcvgpr 7722. This takes and offsets it by the
positive fraction . (Contributed by Jim Kingdon,
23-Jun-2020.)
|
|
| ||
| Theorem | cauappcvgprlem1 7719* | Lemma for cauappcvgpr 7722. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
|
| ||
| Theorem | cauappcvgprlem2 7720* | Lemma for cauappcvgpr 7722. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
|
| ||
| Theorem | cauappcvgprlemlim 7721* | Lemma for cauappcvgpr 7722. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
|
| ||
| Theorem | cauappcvgpr 7722* |
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 7742 and caucvgprpr 7772 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
| ||
| Theorem | archrecnq 7723* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
  | ||
| Theorem | archrecpr 7724* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
|
| ||
| Theorem | caucvgprlemk 7725 | Lemma for caucvgpr 7742. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
   | ||
| Theorem | caucvgprlemnkj 7726* | Lemma for caucvgpr 7742. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
 
| ||
| Theorem | caucvgprlemnbj 7727* | Lemma for caucvgpr 7742. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
|
| ||
| Theorem | caucvgprlemm 7728* | Lemma for caucvgpr 7742. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
|
| ||
| Theorem | caucvgprlemopl 7729* | Lemma for caucvgpr 7742. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
|
| ||
| Theorem | caucvgprlemlol 7730* | Lemma for caucvgpr 7742. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
|
| ||
| Theorem | caucvgprlemopu 7731* | Lemma for caucvgpr 7742. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
|
| ||
| Theorem | caucvgprlemupu 7732* | Lemma for caucvgpr 7742. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
|
| ||
| Theorem | caucvgprlemrnd 7733* | Lemma for caucvgpr 7742. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
|
| ||
| Theorem | caucvgprlemdisj 7734* | Lemma for caucvgpr 7742. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
|
| ||
| Theorem | caucvgprlemloc 7735* | Lemma for caucvgpr 7742. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
|
| ||
| Theorem | caucvgprlemcl 7736* | Lemma for caucvgpr 7742. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
|
| ||
| Theorem | caucvgprlemladdfu 7737* |
Lemma for caucvgpr 7742. Adding after embedding in positive
reals, or adding it as a rational. (Contributed by Jim Kingdon,
9-Oct-2020.)
|
|
| ||
| Theorem | caucvgprlemladdrl 7738* |
Lemma for caucvgpr 7742. Adding after embedding in positive
reals, or adding it as a rational. (Contributed by Jim Kingdon,
8-Oct-2020.)
|
|
| ||
| Theorem | caucvgprlem1 7739* | Lemma for caucvgpr 7742. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
|
| ||
| Theorem | caucvgprlem2 7740* | Lemma for caucvgpr 7742. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
|
| ||
| Theorem | caucvgprlemlim 7741* | Lemma for caucvgpr 7742. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
|
| ||
| Theorem | caucvgpr 7742* |
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 7722 and caucvgprpr 7772. Reading cauappcvgpr 7722 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
|
| ||
| Theorem | caucvgprprlemk 7743* | Lemma for caucvgprpr 7772. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
|
| ||
| Theorem | caucvgprprlemloccalc 7744* | Lemma for caucvgprpr 7772. Rearranging some expressions for caucvgprprlemloc 7763. (Contributed by Jim Kingdon, 8-Feb-2021.) |
 
 
| ||
| Theorem | caucvgprprlemell 7745* | Lemma for caucvgprpr 7772. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
| ||
| Theorem | caucvgprprlemelu 7746* | Lemma for caucvgprpr 7772. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
|
| ||
| Theorem | caucvgprprlemcbv 7747* | Lemma for caucvgprpr 7772. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
| ||
| Theorem | caucvgprprlemval 7748* | Lemma for caucvgprpr 7772. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
|
| ||
| Theorem | caucvgprprlemnkltj 7749* | Lemma for caucvgprpr 7772. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
|
| ||
| Theorem | caucvgprprlemnkeqj 7750* | Lemma for caucvgprpr 7772. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
|
| ||
| Theorem | caucvgprprlemnjltk 7751* | Lemma for caucvgprpr 7772. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
|
| ||
| Theorem | caucvgprprlemnkj 7752* | Lemma for caucvgprpr 7772. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
|
| ||
| Theorem | caucvgprprlemnbj 7753* | Lemma for caucvgprpr 7772. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
|
| ||
| Theorem | caucvgprprlemml 7754* | Lemma for caucvgprpr 7772. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
| ||
| Theorem | caucvgprprlemmu 7755* | Lemma for caucvgprpr 7772. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
 | ||
| Theorem | caucvgprprlemm 7756* | Lemma for caucvgprpr 7772. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemopl 7757* | Lemma for caucvgprpr 7772. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemlol 7758* | Lemma for caucvgprpr 7772. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemopu 7759* | Lemma for caucvgprpr 7772. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemupu 7760* | Lemma for caucvgprpr 7772. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemrnd 7761* | Lemma for caucvgprpr 7772. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemdisj 7762* | Lemma for caucvgprpr 7772. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemloc 7763* | Lemma for caucvgprpr 7772. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.) |
|
| ||
| Theorem | caucvgprprlemcl 7764* | Lemma for caucvgprpr 7772. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.) |
|
| ||
| Theorem | caucvgprprlemclphr 7765* |
Lemma for caucvgprpr 7772. The putative limit is a positive real.
Like caucvgprprlemcl 7764 but without a disjoint variable
condition
between and .
(Contributed by Jim Kingdon,
19-Jun-2021.)
|
|
| ||
| Theorem | caucvgprprlemexbt 7766* | Lemma for caucvgprpr 7772. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.) |
|
| ||
| Theorem | caucvgprprlemexb 7767* | Lemma for caucvgprpr 7772. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.) |
|
| ||
| Theorem | caucvgprprlemaddq 7768* | Lemma for caucvgprpr 7772. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.) |
|
| ||
| Theorem | caucvgprprlem1 7769* | Lemma for caucvgprpr 7772. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
|
| ||
| Theorem | caucvgprprlem2 7770* | Lemma for caucvgprpr 7772. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
|
| ||
| Theorem | caucvgprprlemlim 7771* | Lemma for caucvgprpr 7772. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-2020.) |
|
| ||
| Theorem | caucvgprpr 7772* |
A Cauchy sequence of positive reals 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 given value , to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This is similar to caucvgpr 7742 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 7722) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-2020.) |
|
| ||
| Theorem | suplocexprlemell 7773* | Lemma for suplocexpr 7785. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
 
| ||
| Theorem | suplocexprlem2b 7774 | Lemma for suplocexpr 7785. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
 
| ||
| Theorem | suplocexprlemss 7775* |
Lemma for suplocexpr 7785. is a set of positive reals.
(Contributed by Jim Kingdon, 7-Jan-2024.)
|
| ||
| Theorem | suplocexprlemml 7776* | Lemma for suplocexpr 7785. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemrl 7777* | Lemma for suplocexpr 7785. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemmu 7778* | Lemma for suplocexpr 7785. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemru 7779* | Lemma for suplocexpr 7785. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemdisj 7780* | Lemma for suplocexpr 7785. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemloc 7781* | Lemma for suplocexpr 7785. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemex 7782* | Lemma for suplocexpr 7785. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemub 7783* | Lemma for suplocexpr 7785. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
|
| ||
| Theorem | suplocexprlemlub 7784* | Lemma for suplocexpr 7785. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
|
| ||
| Theorem | suplocexpr 7785* | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) |
|
| ||
| Definition | df-enr 7786* | Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) |
 
| ||
| Definition | df-nr 7787 | Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) |
  | ||
| Definition | df-plr 7788* | Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) |
| ||
| Definition | df-mr 7789* | Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) |
| ||
| Definition | df-ltr 7790* | Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.) |
| ||
| Definition | df-0r 7791 | Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) |
  | ||
| Definition | df-1r 7792 | Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) |
| ||
| Definition | df-m1r 7793 | Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.) |
| ||
| Theorem | enrbreq 7794 | Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) |
| ||
| Theorem | enrer 7795 | The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) |
| ||
| Theorem | enreceq 7796 | Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) |
|
| ||
| Theorem | enrex 7797 | The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) |
 | ||
| Theorem | ltrelsr 7798 | Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) |
| | ||
| Theorem | addcmpblnr 7799 | Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) |
| ||
| Theorem | mulcmpblnrlemg 7800 | Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |