Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 25-Jan-2020 at 1:16 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
17-Jan-2020addcom 6737 Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
 CC  CC  +  +
 
17-Jan-2020ax-addcom 6584 Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6558. Proofs should normally use addcom 6737 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
 CC  CC  +  +
 
17-Jan-2020axaddcom 6558 Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 6584 be used later. Instead, use addcom 6737.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)

 CC  CC  +  +
 
16-Jan-2020addid1 6738  0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
 CC  +  0
 
16-Jan-2020ax-0id 6592  0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6566.

Proofs should normally use addid1 6738 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

 CC  +  0
 
16-Jan-2020ax0id 6566  0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 6592.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)

 CC  +  0
 
15-Jan-2020axltwlin 6682 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6597 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
 RR  RR  C  RR  <  <  C  C  <
 
15-Jan-2020axltirr 6681 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6596 with ordering on the extended reals. New proofs should use ltnr 6689 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
 RR  <
 
14-Jan-20202pwuninelg 5816 The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
 V  ~P ~P U.
 
13-Jan-20201re 6622  1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
 1  RR
 
13-Jan-2020ax-1re 6578 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6552. Proofs should use 1re 6622 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
 1  RR
 
13-Jan-2020ax1re 6552 1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 6578.

In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6577 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)

 1  RR
 
12-Jan-2020ax-pre-ltwlin 6597 Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6571. (Contributed by Jim Kingdon, 12-Jan-2020.)
 RR  RR  C  RR  <RR  <RR  C  C  <RR
 
12-Jan-2020ax-pre-ltirr 6596 Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6596. (Contributed by Jim Kingdon, 12-Jan-2020.)
 RR  <RR
 
12-Jan-2020ax-precex 6594 Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6568.

In treatments which assume excluded middle, the  0 
<RR condition is generally replaced by  =/=  0. (Contributed by Jim Kingdon, 12-Jan-2020.)

 RR  0  <RR  RR  x.  1
 
12-Jan-2020ax-0lt1 6590 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6564. Proofs should normally use 0lt1 6728 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
 0  <RR  1
 
12-Jan-2020axpre-ltwlin 6571 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6597. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
 RR  RR  C  RR  <RR  <RR  C  C  <RR
 
12-Jan-2020axpre-ltirr 6570 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6596. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
 RR  <RR
 
12-Jan-2020axprecex 6568 Existence of reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 6594.

In treatments which assume excluded middle, the  0 
<RR condition is generally replaced by  =/=  0. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)

 RR  0  <RR  RR  x.  1
 
12-Jan-2020ax0lt1 6564 0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 6590.

The version of this axiom in the Metamath Proof Explorer reads  1  =/=  0; here we change it to  0  <RR  1. The proof of  0  <RR  1 from  1  =/=  0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)

 0  <RR  1
 
8-Jan-2020ecidg 6077 A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
 V  `'  _E
 
5-Jan-20201idsr 6509 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
 R.  .R  1R
 
4-Jan-2020distrsrg 6500 Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
 R.  R.  C  R.  .R  +R  C 
 .R  +R  .R  C
 
3-Jan-2020mulasssrg 6499 Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
 R.  R.  C  R.  .R  .R  C  .R  .R  C
 
3-Jan-2020mulcomsrg 6498 Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
 R.  R.  .R  .R
 
3-Jan-2020addasssrg 6497 Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
 R.  R.  C  R.  +R  +R  C  +R  +R  C
 
3-Jan-2020addcomsrg 6496 Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
 R.  R.  +R  +R
 
3-Jan-2020caovlem2d 5612 Rearrangement of expression involving multiplication ( G) and addition ( F). (Contributed by Jim Kingdon, 3-Jan-2020.)
 S  S  G  G   &     S  S  S  F G  G F G   &     S  S  S  G G  G G   &     S  S  G  S   &     S   &     S   &     C  S   &     D  S   &     H  S   &     R  S   &     S  S  F  F   &     S  S  S  F F  F F   &     S  S  F  S   =>     G C F G D G H F G D F G C G R  G C G H F D G R F G C G R F D G H
 
2-Jan-2020bj-d0clsepcl 7287 Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
 
2-Jan-2020ax-bj-d0cl 7286 Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
BOUNDED    =>   
 
1-Jan-2020mulcmpblnrlemg 6481 Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
 P.  P.  C  P.  D  P.  F  P.  G  P.  R  P.  S  P. 
 +P.  D  +P.  C  F  +P.  S  G  +P.  R  D  .P.  F  +P.  .P.  F 
 +P.  .P.  G  +P.  C  .P.  S 
 +P.  D  .P.  R  D 
 .P.  F  +P.  .P.  G  +P.  .P.  F  +P.  C  .P.  R 
 +P.  D  .P.  S
 
31-Dec-2019eceq1d 6049 Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
   =>     C  C
 
30-Dec-2019mulsrmo 6485 There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
 P.  X.  P. /.  ~R  P.  X. 
 P. /.  ~R  t  <. ,  >.  ~R  <. ,  t >.  ~R  <.  .P. 
 +P.  .P.  t ,  .P.  t 
 +P.  .P.  >.  ~R
 
30-Dec-2019addsrmo 6484 There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
 P.  X.  P. /.  ~R  P.  X. 
 P. /.  ~R  t  <. ,  >.  ~R  <. ,  t >.  ~R  <. 
 +P.  ,  +P.  t >. 
 ~R
 
30-Dec-2019prsrlem1 6483 Decomposing signed reals into positive reals. Lemma for addsrpr 6486 and mulsrpr 6487. (Contributed by Jim Kingdon, 30-Dec-2019.)
 P.  X. 
 P. /.  ~R  P.  X.  P. /.  ~R  <. ,  >. 
 ~R 
 <. ,  t >. 
 ~R  <. s ,  >.  ~R  <. ,  h >.  ~R  P.  P.  s 
 P.  P.  P.  t  P.  P.  h  P.  +P.  +P.  s 
 +P.  h  t  +P.
 
29-Dec-2019bj-omelon 7320 The set  om is an ordinal. Constructive proof of omelon 4254. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
 om  On
 
29-Dec-2019bj-omord 7319 The set  om is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
 Ord  om
 
29-Dec-2019bj-omtrans2 7318 The set  om is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
 Tr  om
 
29-Dec-2019bj-omtrans 7317 The set  om is transitive. A natural number is included in  om.

The idea is to use bounded induction with the formula  C_ 
om. This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with  C_  a and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)

 om  C_ 
 om
 
29-Dec-2019ltrnqg 6271 Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6272. (Contributed by Jim Kingdon, 29-Dec-2019.)
 Q.  Q.  <Q  *Q `  <Q  *Q `
 
29-Dec-2019rec1nq 6248 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
 *Q `  1Q  1Q
 
28-Dec-2019recexprlemupu 6456 The upper cut of is upper. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  r  Q.  q  Q.  q  <Q  r  q  2nd `  r  2nd `
 
28-Dec-2019recexprlemopu 6455 The upper cut of is open. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  r  Q.  r  2nd `  q  Q.  q  <Q  r  q  2nd `
 
28-Dec-2019recexprlemlol 6454 The lower cut of is lower. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  q  Q.  r  Q.  q  <Q  r  r  1st `  q  1st `
 
28-Dec-2019recexprlemopl 6453 The lower cut of is open. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  q  Q.  q  1st `  r  Q.  q  <Q  r  r  1st `
 
28-Dec-2019prmuloc2 6405 Positive reals are multiplicatively located. This is a variation of prmuloc 6404 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio , there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.)
 <. L ,  U >.  P.  1Q  <Q  L  .Q  U
 
28-Dec-20191pru 6400 The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
 2nd `  1P  {  |  1Q  <Q  }
 
28-Dec-20191prl 6399 The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
 1st `  1P  {  |  <Q  1Q }
 
27-Dec-2019recexprlemex 6465 is the reciprocal of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  .P.  1P
 
27-Dec-2019recexprlemss1u 6464 The upper cut of  .P. is a subset of the upper cut of one. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  2nd `  .P.  C_  2nd `  1P
 
27-Dec-2019recexprlemss1l 6463 The lower cut of  .P. is a subset of the lower cut of one. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  1st `  .P.  C_  1st `  1P
 
27-Dec-2019recexprlem1ssu 6462 The upper cut of one is a subset of the upper cut of  .P. . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  2nd `  1P  C_  2nd `  .P.
 
27-Dec-2019recexprlem1ssl 6461 The lower cut of one is a subset of the lower cut of  .P. . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  1st `  1P  C_  1st `  .P.
 
27-Dec-2019recexprlempr 6460 is a positive real. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  P.
 
27-Dec-2019recexprlemloc 6459 is located. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  q  Q.  r  Q.  q  <Q  r  q  1st `  r  2nd `
 
27-Dec-2019recexprlemdisj 6458 is disjoint. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  q  Q.  q  1st `  q  2nd `
 
27-Dec-2019recexprlemrnd 6457 is rounded. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  q 
 Q.  q  1st `  r  Q.  q  <Q  r  r  1st `  r  Q.  r  2nd `  q  Q.  q  <Q  r  q  2nd `
 
27-Dec-2019recexprlemm 6452 is inhabited. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     P.  q 
 Q.  q  1st `  r  Q.  r  2nd `
 
27-Dec-2019recexprlemelu 6451 Membership in the upper cut of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     C  2nd `  <Q  C  *Q `  1st `
 
27-Dec-2019recexprlemell 6450 Membership in the lower cut of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
 <. {  | 
 <Q  *Q `  2nd `  } ,  {  | 
 <Q  *Q `  1st `  } >.   =>     C  1st `  C  <Q  *Q `  2nd `
 
26-Dec-2019ltaprg 6449 Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies). (Contributed by Jim Kingdon, 26-Dec-2019.)
 P.  P.  C  P.  <P  C 
 +P.  <P  C 
 +P.
 
26-Dec-2019prarloc2 6352 A Dedekind cut is arithmetically located. This is a variation of prarloc 6351 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance  P, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
 <. L ,  U >.  P.  P  Q.  a  L  a  +Q  P  U
 
25-Dec-2019addcanprlemu 6446 Lemma for addcanprg 6447. (Contributed by Jim Kingdon, 25-Dec-2019.)
 P.  P.  C  P. 
 +P.  +P.  C  2nd `  C_  2nd `  C
 
25-Dec-2019addcanprleml 6445 Lemma for addcanprg 6447. (Contributed by Jim Kingdon, 25-Dec-2019.)
 P.  P.  C  P. 
 +P.  +P.  C  1st `  C_  1st `  C
 
24-Dec-2019addcanprg 6447 Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
 P.  P.  C  P.  +P. 
 +P.  C  C
 
23-Dec-2019ltprordil 6422 If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.)
 <P 
 1st `  C_  1st `
 
22-Dec-2019bj-findis 7336 Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 7308 for a bounded version not requiring ax-setind 4200. See finds 4246 for a proof in IZF. From this version, it is easy to prove of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
 F/   &     F/   &     F/   &     (/)    &       &     suc    =>     om  om
 
21-Dec-2019ltexprlemupu 6435 The upper cut of our constructed difference is upper. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  r  Q.  q  Q.  q  <Q  r  q  2nd `  C  r  2nd `  C
 
21-Dec-2019ltexprlemopu 6434 The upper cut of our constructed difference is open. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  r  Q.  r  2nd `  C  q  Q.  q  <Q  r  q  2nd `  C
 
21-Dec-2019ltexprlemlol 6433 The lower cut of our constructed difference is lower. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  q  Q.  r  Q.  q  <Q  r  r  1st `  C  q  1st `  C
 
21-Dec-2019ltexprlemopl 6432 The lower cut of our constructed difference is open. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  q  Q.  q  1st `  C  r  Q.  q  <Q  r  r  1st `  C
 
21-Dec-2019ltexprlemelu 6430 Element in upper cut of the constructed difference. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     r  2nd `  C  r  Q.  1st `  +Q  r  2nd `
 
21-Dec-2019ltexprlemell 6429 Element in lower cut of the constructed difference. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     q  1st `  C  q  Q.  2nd `  +Q  q  1st `
 
17-Dec-2019ltexprlemru 6443 Lemma for ltexpri 6444. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P 
 2nd `  C_  2nd `  +P.  C
 
17-Dec-2019ltexprlemfu 6442 Lemma for ltexpri 6444. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P 
 2nd `  +P.  C  C_  2nd `
 
17-Dec-2019ltexprlemrl 6441 Lemma for ltexpri 6444. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P 
 1st `  C_  1st `  +P.  C
 
17-Dec-2019ltexprlemfl 6440 Lemma for ltexpri 6444. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P 
 1st `  +P.  C  C_  1st `
 
17-Dec-2019ltexprlempr 6439 Our constructed difference is a positive real. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  C  P.
 
17-Dec-2019ltexprlemloc 6438 Our constructed difference is located. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  q  Q.  r  Q.  q  <Q  r  q  1st `  C  r  2nd `  C
 
17-Dec-2019ltexprlemdisj 6437 Our constructed difference is disjoint. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  q  Q.  q  1st `  C  q  2nd `  C
 
17-Dec-2019ltexprlemrnd 6436 Our constructed difference is rounded. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  q  Q.  q  1st `  C  r  Q.  q  <Q  r  r  1st `  C  r  Q.  r  2nd `  C  q  Q.  q  <Q  r  q  2nd `  C
 
17-Dec-2019ltexprlemm 6431 Our constructed difference is inhabited. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
 C  <. {  Q.  |  2nd `  +Q  1st `  } ,  {  Q.  |  1st `  +Q  2nd `  } >.   =>     <P  q  Q.  q  1st `  C  r  Q.  r  2nd `  C
 
16-Dec-2019bj-sbime 7159 A strengthening of sbie 1652 (same proof). (Contributed by BJ, 16-Dec-2019.)
 F/   &       =>   
 
16-Dec-2019bj-sbimeh 7158 A strengthening of sbieh 1651 (same proof). (Contributed by BJ, 16-Dec-2019.)
   &       =>   
 
16-Dec-2019bj-sbimedh 7157 A strengthening of sbiedh 1648 (same proof). (Contributed by BJ, 16-Dec-2019.)
   &       &       =>   
 
16-Dec-2019ltsopr 6427 Positive real 'less than' is a weak linear order (in the sense of df-iso 4004). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)

 <P  Or  P.
 
15-Dec-2019ltpopr 6426 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 6427. (Contributed by Jim Kingdon, 15-Dec-2019.)

 <P  Po  P.
 
15-Dec-2019ltdfpr 6354 More convenient form of df-iltp 6318. (Contributed by Jim Kingdon, 15-Dec-2019.)
 P.  P.  <P  q  Q.  q  2nd `  q  1st `
 
15-Dec-2019prdisj 6340 A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
 <. L ,  U >.  P.  Q.  L  U
 
13-Dec-20191idpru 6424 Lemma for 1idpr 6425. (Contributed by Jim Kingdon, 13-Dec-2019.)
 P.  2nd `  .P.  1P  2nd `
 
13-Dec-20191idprl 6423 Lemma for 1idpr 6425. (Contributed by Jim Kingdon, 13-Dec-2019.)
 P.  1st `  .P.  1P  1st `
 
13-Dec-2019gtnqex 6397 The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)

 {  |  <Q  }  _V
 
13-Dec-2019ltnqex 6396 The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)

 {  |  <Q  }  _V
 
13-Dec-2019sotritrieq 4032 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
 R  Or    &     C  R C  C  C R   =>     C  C  R C  C R
 
12-Dec-2019distrprg 6421 Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  .P.  +P.  C 
 .P.  +P.  .P.  C
 
12-Dec-2019distrlem5pru 6420 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  2nd `  .P. 
 +P.  .P.  C  C_  2nd `  .P.  +P.  C
 
12-Dec-2019distrlem5prl 6419 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  1st `  .P. 
 +P.  .P.  C  C_  1st `  .P.  +P.  C
 
12-Dec-2019distrlem4pru 6418 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  2nd `  2nd `  2nd `  2nd `  C  .Q  +Q  .Q  2nd `  .P.  +P.  C
 
12-Dec-2019distrlem4prl 6417 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  1st `  1st `  1st `  1st `  C  .Q  +Q  .Q  1st `  .P.  +P.  C
 
12-Dec-2019distrlem1pru 6416 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  2nd `  .P.  +P.  C  C_  2nd `  .P.  +P.  .P.  C

  Copyright terms: Public domain W3C HTML validation [external]