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
 
12-Dec-2019distrlem1prl 6415 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
 P.  P.  C  P.  1st `  .P.  +P.  C  C_  1st `  .P.  +P.  .P.  C
 
12-Dec-2019ltdcnq 6250 Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
 Q.  Q. DECID 
 <Q
 
12-Dec-2019ltdcpi 6177 Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
 N.  N. DECID 
 <N
 
11-Dec-2019mulassprg 6414 Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
 P.  P.  C  P.  .P.  .P.  C  .P.  .P.  C
 
11-Dec-2019mulcomprg 6413 Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
 P.  P.  .P.  .P.
 
11-Dec-2019addassprg 6412 Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
 P.  P.  C  P.  +P.  +P.  C  +P.  +P.  C
 
11-Dec-2019addcomprg 6411 Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
 P.  P.  +P.  +P.
 
11-Dec-2019genpassg 6375 Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   &    
 Q.  Q.  G 
 Q.   &     dom  F  P.  X.  P.   &     P.  P.  F  P.   &     Q.  Q.  h  Q.  G G h  G G h   =>     P.  P.  C  P.  F F C  F F C
 
11-Dec-2019genpassu 6374 Associativity of upper cuts. Lemma for genpassg 6375. (Contributed by Jim Kingdon, 11-Dec-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   &    
 Q.  Q.  G 
 Q.   &     dom  F  P.  X.  P.   &     P.  P.  F  P.   &     Q.  Q.  h  Q.  G G h  G G h   =>     P.  P.  C  P.  2nd `  F F C  2nd `  F F C
 
11-Dec-2019genpassl 6373 Associativity of lower cuts. Lemma for genpassg 6375. (Contributed by Jim Kingdon, 11-Dec-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   &    
 Q.  Q.  G 
 Q.   &     dom  F  P.  X.  P.   &     P.  P.  F  P.   &     Q.  Q.  h  Q.  G G h  G G h   =>     P.  P.  C  P.  1st `  F F C  1st `  F F C
 
11-Dec-2019preqlu 6320 Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.)
 P.  P.  1st `  1st `  2nd `  2nd `
 
10-Dec-2019mullocprlem 6408 Calculations for mullocpr 6409. (Contributed by Jim Kingdon, 10-Dec-2019.)
 P.  P.   &     U  .Q  Q  <Q  E  .Q  D  .Q  U   &     E  .Q  D  .Q  U  <Q  T  .Q  D  .Q  U   &     T  .Q  D  .Q  U 
 <Q  D  .Q  R   &     Q  Q.  R  Q.   &     D  Q.  U  Q.   &     D  1st `  U  2nd `    &     E  Q.  T  Q.   =>     Q  1st `  .P.  R  2nd `  .P.
 
10-Dec-2019mulnqpru 6407 Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
 P.  G  2nd `  P.  H  2nd `  X  Q.  G  .Q  H  <Q  X  X  2nd `  .P.
 
10-Dec-2019mulnqprl 6406 Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
 P.  G  1st `  P.  H  1st `  X  Q.  X  <Q  G  .Q  H 
 X  1st `  .P.
 
9-Dec-2019prmuloclemcalc 6403 Calculations for prmuloc 6404. (Contributed by Jim Kingdon, 9-Dec-2019.)
 R  <Q  U   &     U  <Q  D  +Q  P   &     +Q  X    &     P  .Q  <Q  R  .Q  X   &     Q.   &     Q.   &     D  Q.   &     P  Q.   &     X  Q.   =>     U  .Q  <Q  D  .Q
 
9-Dec-2019appdiv0nq 6402 Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6401 in which is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.)
 Q.  C  Q.  m  Q.  m  .Q  C 
 <Q
 
9-Dec-2019ltmnqi 6256 Ordering property of multiplication for positive fractions. One direction of ltmnqg 6254. (Contributed by Jim Kingdon, 9-Dec-2019.)
 <Q  C  Q.  C  .Q  <Q  C  .Q
 
9-Dec-2019ltanqi 6255 Ordering property of addition for positive fractions. One direction of ltanqg 6253. (Contributed by Jim Kingdon, 9-Dec-2019.)
 <Q  C  Q.  C  +Q  <Q  C  +Q
 
8-Dec-2019bj-nn0sucALT 7335 Alternate proof of bj-nn0suc 7321, also constructive but from ax-inf2 7333, hence requiring ax-bdsetind 7325. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
 om  (/)  om  suc
 
8-Dec-2019bj-omex2 7334 Using bounded set induction and the strong axiom of infinity,  om is a set, that is, we recover ax-infvn 7302 (see bj-2inf 7299 for the equivalence of the latter with bj-omex 7303). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
 om  _V
 
8-Dec-2019bj-inf2vn2 7332 A sufficient condition for  om to be a set; unbounded version of bj-inf2vn 7331. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
 V  (/)  suc  om
 
8-Dec-2019bj-inf2vn 7331 A sufficient condition for  om to be a set. See bj-inf2vn2 7332 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED    =>     V  (/)  suc  om
 
8-Dec-2019bj-inf2vnlem4 7330 Lemma for bj-inf2vn2 7332. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
 (/)  suc Ind  Z  C_  Z
 
8-Dec-2019bj-inf2vnlem3 7329 Lemma for bj-inf2vn 7331. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED    &    BOUNDED  Z   =>     (/)  suc Ind  Z  C_  Z
 
8-Dec-2019bj-inf2vnlem2 7328 Lemma for bj-inf2vnlem3 7329 and bj-inf2vnlem4 7330. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
 (/)  suc Ind  Z  t  t  t  Z  Z
 
8-Dec-2019bj-inf2vnlem1 7327 Lemma for bj-inf2vn 7331. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
 (/)  suc Ind
 
8-Dec-2019bj-bdcel 7203 Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
BOUNDED    =>    BOUNDED
 
8-Dec-2019bj-ex 7148 Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1467 and 19.9ht 1510 or 19.23ht 1363). (Proof modification is discouraged.)
 
8-Dec-2019mullocpr 6409 Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both and are positive, not just ). (Contributed by Jim Kingdon, 8-Dec-2019.)
 P.  P.  q  Q.  r  Q.  q  <Q  r  q  1st `  .P.  r  2nd `  .P.
 
8-Dec-2019prmuloc 6404 Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
 <. L ,  U >.  P.  <Q  d  Q.  Q.  d  L  U  .Q  <Q  d  .Q
 
8-Dec-2019appdivnq 6401 Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where and are positive, as well as  C). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.)
 <Q  C  Q.  m  Q.  <Q  m  .Q  C  m  .Q  C 
 <Q
 
8-Dec-2019nqprlu 6395 The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
 Q.  <. {  |  <Q  } ,  {  |  <Q  } >.  P.
 
8-Dec-2019nqprloc 6394 A cut produced from a rational is located. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
 Q.  q  Q.  r  Q.  q  <Q  r  q  {  |  <Q  }  r  {  |  <Q  }
 
8-Dec-2019nqprdisj 6393 A cut produced from a rational is disjoint. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
 Q.  q  Q.  q  {  |  <Q  }  q 
 {  |  <Q  }
 
8-Dec-2019nqprrnd 6392 A cut produced from a rational is rounded. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
 Q.  q 
 Q.  q 
 {  |  <Q  }  r  Q.  q  <Q  r  r  {  |  <Q  }  r  Q.  r 
 {  |  <Q  }  q  Q.  q  <Q  r  q  {  |  <Q  }
 
8-Dec-2019nqprm 6391 A cut produced from a rational is inhabited. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
 Q.  q 
 Q.  q  {  |  <Q  }  r  Q.  r  {  |  <Q  }
 
8-Dec-2019mpvlu 6388 Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
 P.  P.  .P.  <. {  Q.  |  1st `  1st `  .Q  } ,  {  Q.  |  2nd `  2nd `  .Q  } >.
 
8-Dec-2019plpvlu 6387 Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
 P.  P.  +P.  <. {  Q.  |  1st `  1st `  +Q  } ,  {  Q.  |  2nd `  2nd `  +Q  } >.
 
7-Dec-2019addlocprlemeqgt 6381 Lemma for addlocpr 6385. This is a step used in both the  Q  D  +Q  E and  D  +Q  E  <Q  Q cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
 P.   &     P.   &     Q  <Q  R   &     P  Q.   &     Q  +Q  P  +Q  P  R   &     D  1st `    &     U  2nd `    &     U  <Q  D  +Q  P   &     E  1st `    &     T  2nd `    &     T  <Q  E  +Q  P   =>     U  +Q  T  <Q  D  +Q  E  +Q  P  +Q  P
 
7-Dec-2019addnqprulem 6377 Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
 <. L ,  U >.  P.  G  U  X  Q.  S  <Q  X  X  .Q  *Q `  S 
 .Q  G  U
 
7-Dec-2019addnqprllem 6376 Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
 <. L ,  U >.  P.  G  L  X  Q.  X  <Q  S  X  .Q  *Q `  S 
 .Q  G  L
 
7-Dec-2019lt2addnq 6257 Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
 Q.  Q.  C  Q.  D  Q.  <Q  C  <Q  D  +Q  C 
 <Q  +Q  D
 
6-Dec-2019addlocprlem 6384 Lemma for addlocpr 6385. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
 P.   &     P.   &     Q  <Q  R   &     P  Q.   &     Q  +Q  P  +Q  P  R   &     D  1st `    &     U  2nd `    &     U  <Q  D  +Q  P   &     E  1st `    &     T  2nd `    &     T  <Q  E  +Q  P   =>     Q  1st `  +P.  R  2nd `  +P.
 
6-Dec-2019addlocprlemgt 6383 Lemma for addlocpr 6385. The  D  +Q  E  <Q  Q case. (Contributed by Jim Kingdon, 6-Dec-2019.)
 P.   &     P.   &     Q  <Q  R   &     P  Q.   &     Q  +Q  P  +Q  P  R   &     D  1st `    &     U  2nd `    &     U  <Q  D  +Q  P   &     E  1st `    &     T  2nd `    &     T  <Q  E  +Q  P   =>     D  +Q  E 
 <Q  Q  R  2nd `  +P.
 
6-Dec-2019addlocprlemeq 6382 Lemma for addlocpr 6385. The  Q  D  +Q  E case. (Contributed by Jim Kingdon, 6-Dec-2019.)
 P.   &     P.   &     Q  <Q  R   &     P  Q.   &     Q  +Q  P  +Q  P  R   &     D  1st `    &     U  2nd `    &     U  <Q  D  +Q  P   &     E  1st `    &     T  2nd `    &     T  <Q  E  +Q  P   =>     Q  D  +Q  E  R  2nd `  +P.
 
6-Dec-2019addlocprlemlt 6380 Lemma for addlocpr 6385. The  Q  <Q  D  +Q  E case. (Contributed by Jim Kingdon, 6-Dec-2019.)
 P.   &     P.   &     Q  <Q  R   &     P  Q.   &     Q  +Q  P  +Q  P  R   &     D  1st `    &     U  2nd `    &     U  <Q  D  +Q  P   &     E  1st `    &     T  2nd `    &     T  <Q  E  +Q  P   =>     Q  <Q  D  +Q  E  Q  1st `  +P.
 
5-Dec-2019addlocpr 6385 Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6351 to both and , and uses nqtri3or 6249 rather than prloc 6339 to decide whether  q is too big to be in the lower cut of  +P. (and deduce that if it is, then  r must be in the upper cut). What the two proofs have in common is that they take the difference between  q and  r to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.)
 P.  P.  q  Q.  r  Q.  q  <Q  r  q  1st `  +P.  r  2nd `  +P.
 
5-Dec-2019addnqpru 6379 Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
 P.  G  2nd `  P.  H  2nd `  X  Q.  G  +Q  H  <Q  X  X  2nd `  +P.
 
5-Dec-2019addnqprl 6378 Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
 P.  G  1st `  P.  H  1st `  X  Q.  X  <Q  G  +Q  H 
 X  1st `  +P.
 
5-Dec-2019genpmu 6367 The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   &    
 Q.  Q.  G 
 Q.   =>     P.  P.  q  Q.  q  2nd `  F
 
5-Dec-2019genpelxp 6359 Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   =>     P.  P.  F  ~P Q.  X. 
 ~P Q.
 
3-Dec-2019addassnq0lemcl 6310 A natural number closure law. Lemma for addassnq0 6311. (Contributed by Jim Kingdon, 3-Dec-2019.)
 I  om  J  N.  K  om  L  N.  I  .o  L  +o  J  .o  K  om  J  .o  L 
 N.
 
3-Dec-2019nndir 5980 Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
 om  om  C  om  +o  .o  C 
 .o  C  +o  .o  C
 
1-Dec-2019nnanq0 6307 Addition of non-negative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.)
 N  om  M  om  N.  <. N  +o  M ,  >. ~Q0  <. N ,  >. ~Q0 +Q0  <. M ,  >. ~Q0
 
1-Dec-2019archnqq 6268 For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.)
 Q.  N.  <Q  <. ,  1o >.  ~Q
 
30-Nov-2019bj-2inf 7299 Two formulations of the axiom of infinity (see ax-infvn 7302 and bj-omex 7303) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
 om  _V Ind Ind  C_
 
30-Nov-2019bj-om 7298 A set is equal to  om if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
 V  om Ind Ind  C_
 
30-Nov-2019bj-ssom 7297 A characterization of subclasses of  om. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
Ind  C_  C_  om
 
30-Nov-2019bj-omssind 7296  om is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
 V Ind  om  C_
 
30-Nov-2019bj-omind 7295  om is an inductive class. (Contributed by BJ, 30-Nov-2019.)
Ind  om
 
30-Nov-2019bj-dfom 7294 Alternate definition of  om, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
 om  |^| {  | Ind  }
 
30-Nov-2019bj-indint 7293 The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
Ind  |^| {  | Ind  }
 
30-Nov-2019bj-bdind 7292 Boundedness of the formula "the setvar is an inductive class". (Contributed by BJ, 30-Nov-2019.)
BOUNDED Ind
 
30-Nov-2019bj-indeq 7291 Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
Ind Ind
 
30-Nov-2019bj-indsuc 7290 A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
Ind  suc
 
30-Nov-2019df-bj-ind 7289 Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
Ind  (/)  suc
 
30-Nov-2019bj-bdsucel 7248 Boundedness of the formula "the successor of the setvar belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.)
BOUNDED  suc
 
30-Nov-2019bj-bd0el 7234 Boundedness of the formula "the empty set belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.)
BOUNDED  (/)
 
30-Nov-2019bj-sseq 7177 If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.)
 C_    &     C_    =>   
 
30-Nov-2019nqpnq0nq 6302 A positive fraction plus a non-negative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.)
 Q. Q0 +Q0  Q.
 
30-Nov-2019mulclnq0 6301 Closure of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.)
Q0 Q0 ·Q0 Q0
 
30-Nov-2019prarloclemarch 6269 A version of the Archimedean property. This variation is "stronger" than archnqq 6268 in the sense that we provide an integer which is larger than a given rational even after being multiplied by a second rational . (Contributed by Jim Kingdon, 30-Nov-2019.)
 Q.  Q.  N.  <Q  <. ,  1o >.  ~Q  .Q
 
29-Nov-2019bj-elssuniab 7176 Version of elssuni 3578 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
 F/_   =>     V  [.  ].  C_  U.
 {  |  }
 
29-Nov-2019bj-intabssel1 7175 Version of intss1 3600 using a class abstraction and implicit substitution. Closed form of intmin3 3612. (Contributed by BJ, 29-Nov-2019.)
 F/_   &    
 F/   &       =>     V  |^| {  |  }  C_
 
29-Nov-2019bj-intabssel 7174 Version of intss1 3600 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
 F/_   =>     V  [.  ].  |^| {  |  }  C_
 
29-Nov-2019nq02m 6313 Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.)
Q0  <. 2o ,  1o >. ~Q0 ·Q0 +Q0
 
29-Nov-2019distnq0r 6312 Multiplication of non-negative fractions is distributive. Version of distrnq0 6308 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.)
Q0 Q0  C Q0 +Q0  C ·Q0 ·Q0 +Q0  C ·Q0
 
29-Nov-2019addassnq0 6311 Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
Q0 Q0  C Q0 +Q0 +Q0  C +Q0 +Q0  C
 
29-Nov-2019addclnq0 6300 Closure of addition on non-negative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.)
Q0 Q0 +Q0 Q0
 
29-Nov-2019mulcanenq0ec 6294 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.)
 N.  om  C  N.  <.  .o  , 
 .o  C >. ~Q0 
 <. ,  C >. ~Q0
 
28-Nov-2019ax-bdsetind 7325 Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
BOUNDED    =>     a  a  a  a
 
28-Nov-2019bj-peano4 7316 Remove from peano4 4243 dependency on ax-setind 4200. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
 om  om  suc  suc
 
28-Nov-2019bj-nnen2lp 7315 A version of en2lp 4212 for natural numbers, which does not require ax-setind 4200.

Note: using this theorem and bj-nnelirr 7314, one can remove dependency on ax-setind 4200 from nntri2 5984 and nndcel 5987; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)

 om  om
 
27-Nov-2019mulcomnq0 6309 Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.)
Q0 Q0 ·Q0 ·Q0
 
27-Nov-2019distrnq0 6308 Multiplication of non-negative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.)
Q0 Q0  C Q0 ·Q0 +Q0  C ·Q0 +Q0 ·Q0  C
 
25-Nov-2019prcunqu 6333 An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
 <. L ,  U >.  P.  C  U  C  <Q  U
 
25-Nov-2019prarloclemarch2 6270 Like prarloclemarch 6269 but the integer must be at least two, and there is also added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6351. (Contributed by Jim Kingdon, 25-Nov-2019.)
 Q.  Q.  C  Q.  N.  1o  <N  <Q  +Q  <. ,  1o >.  ~Q  .Q  C
 
25-Nov-2019subhalfnqq 6265 There is a number which is less than half of any positive fraction. The case where is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6261). (Contributed by Jim Kingdon, 25-Nov-2019.)
 Q.  Q.  +Q  <Q
 
24-Nov-2019bj-nnelirr 7314 A natural number does not belong to itself. Version of elirr 4204 for natural numbers, which does not require ax-setind 4200. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
 om
 
24-Nov-2019bdcriota 7249 A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
BOUNDED    &       =>    BOUNDED  iota_
 
24-Nov-2019nq0nn 6291 Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
Q0  om  N.  <. ,  >. ~Q0
 
24-Nov-2019enq0eceq 6286 Equivalence class equality of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.)
 om  N.  C  om  D  N.  <. ,  >. ~Q0  <. C ,  D >. ~Q0  .o  D  .o  C
 
24-Nov-2019dfplq0qs 6279 Addition on non-negative fractions. This definition is similar to df-plq0 6276 but expands Q0 (Contributed by Jim Kingdon, 24-Nov-2019.)
+Q0  {
 <. <. ,  >. ,  >.  |  om  X.  N. /. ~Q0  om  X.  N. /. ~Q0 
 <. ,  >. ~Q0  <. ,  >. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0  }
 
23-Nov-2019addnq0mo 6296 There is at most one result from adding non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
 om  X.  N. /. ~Q0  om  X.  N. /. ~Q0  t  <. ,  >. ~Q0  <. ,  t >. ~Q0  <. 
 .o  t  +o  .o  , 
 .o  t >. ~Q0
 
23-Nov-2019nnnq0lem1 6295 Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6298 and mulnnnq0 6299. (Contributed by Jim Kingdon, 23-Nov-2019.)
 om  X. 
 N. /. ~Q0  om  X.  N. /. ~Q0  <. ,  >. ~Q0  <. ,  t >. ~Q0  C ~Q0  <. s ,  >. ~Q0  <. ,  h >. ~Q0  q  D ~Q0  om  N.  s  om  N.  om  t  N.  om  h  N.  .o  .o  s 
 .o  h  t  .o
 
23-Nov-2019addcmpblnq0 6292 Lemma showing compatibility of addition on non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
 om  N.  C  om  D  N.  F  om  G  N.  R  om  S  N. 
 .o  D  .o  C  F  .o  S  G  .o  R  <. 
 .o  G  +o  .o  F , 
 .o  G >. ~Q0  <. C  .o  S 
 +o  D  .o  R ,  D  .o  S >.
 
23-Nov-2019ee8anv 1788 Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
 t s  t s
 
23-Nov-201919.42vvvv 1768 Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
 
22-Nov-2019bdsetindis 7326 Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     F/   &     F/   &     F/   &     F/   &       &       =>   
 
22-Nov-2019setindis 7324 Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.)
 F/   &     F/   &     F/   &     F/   &       &       =>   
 
22-Nov-2019setindf 7323 Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
 F/   =>   
 
22-Nov-2019setindft 7322 Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
 F/
 
22-Nov-2019bj-nntrans2 7313 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
 om  Tr
 
22-Nov-2019bj-nntrans 7312 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
 om  C_
 
22-Nov-2019bdfind 7307 Bounded induction (principle of induction when is assumed to be bounded), proved from basic constructive axioms. See find 4245 for a nonconstructive proof of the general case. See findset 7306 for a proof when is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    =>     C_  om  (/)  suc  om
 
22-Nov-2019findset 7306 Bounded induction (principle of induction when is assumed to be a set) allowing a proof from basic constructive axioms. See find 4245 for a nonconstructive proof of the general case. See bdfind 7307 for a proof when is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
 V  C_  om  (/)  suc  om
 
22-Nov-2019cbvrald 7173 Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.)
 F/   &     F/   &     F/   &     F/   &       =>   
 
22-Nov-2019addnnnq0 6298 Addition of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
 om  N.  C  om  D  N.  <. ,  >. ~Q0 +Q0  <. C ,  D >. ~Q0  <.  .o  D  +o  .o  C ,  .o  D >. ~Q0
 
22-Nov-2019dfmq0qs 6278 Multiplication on non-negative fractions. This definition is similar to df-mq0 6277 but expands Q0 (Contributed by Jim Kingdon, 22-Nov-2019.)
·Q0  { <.
 <. ,  >. ,  >.  |  om  X.  N. /. ~Q0  om  X.  N. /. ~Q0 
 <. ,  >. ~Q0  <. ,  >. ~Q0  <.  .o  ,  .o  >. ~Q0  }
 
21-Nov-2019bj-findes 7338 Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 7336 for explanations. From this version, it is easy to prove findes 4249. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
 [. (/)  ].  om  [. suc  ].  om
 
21-Nov-2019bj-findisg 7337 Version of bj-findis 7336 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 7336 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
 F/   &     F/   &     F/   &     (/)    &       &     suc    &     F/_   &     F/   &       =>     om  om
 
21-Nov-2019bj-bdfindes 7310 Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 7308 for explanations. From this version, it is easy to prove the bounded version of findes 4249. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    =>     [. (/)  ].  om  [. suc  ].  om
 
21-Nov-2019bj-bdfindisg 7309 Version of bj-bdfindis 7308 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 7308 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     F/   &     F/   &     F/   &     (/)    &       &     suc    &     F/_   &     F/   &       =>     om  om
 
21-Nov-2019bj-bdfindis 7308 Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4246 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     F/   &     F/   &     F/   &     (/)    &       &     suc    =>     om  om
 
21-Nov-2019bdeqsuc 7247 Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
BOUNDED  suc
 
21-Nov-2019bdop 7241 The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
BOUNDED 
 <. ,  >.
 
21-Nov-2019bdeq0 7233 Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
BOUNDED  (/)
 
21-Nov-2019bj-rspg 7172 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2626 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
 F/_   &     F/_   &     F/   &       =>   
 
21-Nov-2019bj-rspgt 7171 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2626 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
 F/_   &     F/_   &     F/   =>   
 
21-Nov-2019elabg2 7170 One implication of elabg 2661. (Contributed by BJ, 21-Nov-2019.)
   =>     V  {  |  }
 
21-Nov-2019elab2a 7169 One implication of elab 2660. (Contributed by BJ, 21-Nov-2019.)
 _V   &       =>     {  |  }
 
21-Nov-2019elab1 7168 One implication of elab 2660. (Contributed by BJ, 21-Nov-2019.)
   =>     {  |  }
 
21-Nov-2019elabf2 7167 One implication of elabf 2659. (Contributed by BJ, 21-Nov-2019.)
 F/   &     _V   &       =>     {  |  }
 
21-Nov-2019elabf1 7166 One implication of elabf 2659. (Contributed by BJ, 21-Nov-2019.)
 F/   &       =>     {  |  }
 
21-Nov-2019elabgf2 7165 One implication of elabgf 2658. (Contributed by BJ, 21-Nov-2019.)
 F/_   &    
 F/   &       =>     {  |  }
 
21-Nov-2019elabgf1 7164 One implication of elabgf 2658. (Contributed by BJ, 21-Nov-2019.)
 F/_   &    
 F/   &       =>     {  |  }
 
21-Nov-2019elabgft1 7163 One implication of elabgf 2658, in closed form. (Contributed by BJ, 21-Nov-2019.)
 F/_   &    
 F/   =>     {  |  }
 
21-Nov-2019elabgf0 7162 Lemma for elabgf 2658. (Contributed by BJ, 21-Nov-2019.)
 {  |  }
 
21-Nov-2019bj-vtoclgf 7161 Weakening two hypotheses of vtoclgf 2585. (Contributed by BJ, 21-Nov-2019.)
 F/_   &    
 F/   &       &       =>     V
 
21-Nov-2019bj-vtoclgft 7160 Weakening two hypotheses of vtoclgf 2585. (Contributed by BJ, 21-Nov-2019.)
 F/_   &    
 F/   &       =>     V
 
21-Nov-2019bj-exlimmpi 7156 Lemma for bj-vtoclgf 7161. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
 F/   &       &       =>   
 
21-Nov-2019bj-exlimmp 7155 Lemma for bj-vtoclgf 7161. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
 F/   &       =>   
 
20-Nov-2019mulnq0mo 6297 There is at most one result from multiplying non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
 om  X.  N. /. ~Q0  om  X.  N. /. ~Q0  t  <. ,  >. ~Q0  <. ,  t >. ~Q0  <.  .o  , 
 .o  t >. ~Q0
 
20-Nov-2019mulcmpblnq0 6293 Lemma showing compatibility of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
 om  N.  C  om  D  N.  F  om  G  N.  R  om  S  N. 
 .o  D  .o  C  F  .o  S  G  .o  R  <.  .o  F , 
 .o  G >. ~Q0  <. C  .o  R ,  D  .o  S
 >.
 
19-Nov-2019bj-nn0suc 7321 Proof of (biconditional form of) nn0suc 4250 from the core axioms of CZF. See also bj-nn0sucALT 7335. As a characterization of the elements of  om, this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
 om  (/)  om  suc
 
19-Nov-2019bj-nn0suc0 7311 Constructive proof of a variant of nn0suc 4250. For a constructive proof of nn0suc 4250, see bj-nn0suc 7321. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
 om  (/)  suc
 
19-Nov-2019speano5 7305 Version of peano5 4244 when is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
 V  (/)  om  suc  om  C_
 
19-Nov-2019bdpeano5 7304 Bounded version of peano5 4244. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    =>     (/)  om  suc  om  C_
 
19-Nov-2019peano5set 7301 Version of peano5 4244 when  om  i^i is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
 om  i^i  V  (/)  om  suc  om  C_
 
19-Nov-2019bj-inex 7269 The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
 V  W  i^i  _V
 
19-Nov-2019bdrabexg 7268 Bounded version of rabexg 3870. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &    BOUNDED    =>     V  {  |  }  _V
 
19-Nov-2019bds 7217 Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 7188; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 7188. (Contributed by BJ, 19-Nov-2019.)
BOUNDED    &       =>    BOUNDED
 
19-Nov-2019mulnnnq0 6299 Multiplication of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 19-Nov-2019.)
 om  N.  C  om  D  N.  <. ,  >. ~Q0 ·Q0  <. C ,  D >. ~Q0  <.  .o  C ,  .o  D >. ~Q0
 
18-Nov-2019bj-peano2 7300 Constructive proof of peano2 4241. Temporary note: another possibility is to simply replace sucexg 4170 with bj-sucexg 7284 in the proof of peano2 4241. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 om  suc  om
 
18-Nov-2019bj-intnexr 7271 vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 |^|  _V 
 |^|  _V
 
18-Nov-2019bj-intexr 7270 vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 |^|  _V  =/=  (/)
 
18-Nov-2019bj-vnex 7260 vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 _V
 
18-Nov-2019bj-nvel 7259 nvel 3859 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 _V
 
18-Nov-2019bj-vprc 7258 vprc 3858 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 _V  _V
 
18-Nov-2019bj-nalset 7257 nalset 3857 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
 
18-Nov-2019nqnq0 6290 A positive fraction is a non-negative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.)

 Q.  C_ Q0
 
18-Nov-2019nq0ex 6289 The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
Q0  _V
 
18-Nov-2019enq0ex 6288 The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
~Q0  _V
 
14-Nov-2019ax-inf2 7333 Another axiom of infinity in a constructive setting (see ax-infvn 7302). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
 a  a  (/)  a  suc
 
14-Nov-2019bj-omex 7303 Proof of omex 4239 from ax-infvn 7302. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.)
 om  _V
 
14-Nov-2019ax-infvn 7302 Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4234) from which one then proves (omex 4239) using full separation that the wanted set exists. "vn" is for "Von Neumann". (Contributed by BJ, 14-Nov-2019.)
Ind Ind  C_
 
14-Nov-2019enq0tr 6283 The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
~Q0 ~Q0  h ~Q0  h
 
14-Nov-2019enq0ref 6282 The equivalence relation for non-negative fractions is reflexive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
 om  X.  N. ~Q0
 
14-Nov-2019enq0sym 6281 The equivalence relation for non-negative fractions is symmetric. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
~Q0 ~Q0
 
13-Nov-2019bj-sucex 7285 sucex 4171 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 _V   =>    
 suc  _V
 
13-Nov-2019bj-sucexg 7284 sucexg 4170 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 V  suc  _V
 
13-Nov-2019bj-unexg 7283 unexg 4124 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 V  W  u.  _V
 
13-Nov-2019bdunexb 7282 Bounded version of unexb 4123. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &    BOUNDED    =>     _V  _V  u. 
 _V
 
13-Nov-2019bj-unex 7281 unex 4122 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 _V   &     _V   =>     u.  _V
 
13-Nov-2019bj-uniexg 7280 uniexg 4121 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 V  U.  _V
 
13-Nov-2019bj-uniex 7279 uniex 4120 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 _V   =>    
 U.  _V
 
13-Nov-2019bdssexd 7267 Bounded version of ssexd 3867. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
 C   &     C_    &    BOUNDED    =>     _V
 
13-Nov-2019bdssexg 7266 Bounded version of ssexg 3866. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    =>     C_  C  _V
 
13-Nov-2019bdssexi 7265 Bounded version of ssexi 3865. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     _V   &     C_    =>     _V
 
13-Nov-2019bdssex 7264 Bounded version of ssex 3864. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     _V   =>     C_  _V
 
13-Nov-2019bdinex1g 7263 Bounded version of inex1g 3863. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    =>     V  i^i  _V
 
13-Nov-2019bdinex2 7262 Bounded version of inex2 3862. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     _V   =>     i^i  _V
 
13-Nov-2019bdinex1 7261 Bounded version of inex1 3861. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED    &     _V   =>     i^i  _V
 
13-Nov-2019bdzfauscl 7255 Closed form of the version of zfauscl 3847 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
BOUNDED    =>     V
 
12-Nov-2019enq0er 6284 The equivalence relation for non-negative fractions is an equivalence relation. (Contributed by Jim Kingdon, 12-Nov-2019.)
~Q0  Er  om  X.  N.
 
12-Nov-2019enq0enq 6280 Equivalence on positive fractions in terms of equivalence on non-negative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)

 ~Q ~Q0  i^i  N.  X. 
 N.  X.  N.  X.  N.
 
10-Nov-2019prarloclemup 6343 Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.)
 X  om  <. L ,  U >. 
 P.  L  P  Q. 
 om  +Q  <. 
 +o  2o  +o  X ,  1o >.  ~Q  .Q  P  U +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  suc  X ,  1o >. 
 ~Q  .Q  P  U  om +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  X ,  1o >.  ~Q  .Q  P  U
 
10-Nov-2019prarloclemlo 6342 Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.)
 X  om  <. L ,  U >. 
 P.  L  P  Q. 
 om  +Q  <.  +o  1o ,  1o >. 
 ~Q  .Q  P  L +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  suc  X ,  1o >. 
 ~Q  .Q  P  U  om +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  X ,  1o >.  ~Q  .Q  P  U
 
10-Nov-2019prarloclemlt 6341 Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.)
 X  om  <. L ,  U >. 
 P.  L  P  Q. 
 om  +Q  <.  +o  1o ,  1o >.  ~Q  .Q  P  <Q 
 +Q  <.  +o  2o  +o  X ,  1o >.  ~Q  .Q  P
 
10-Nov-2019nqnq0m 6304 Multiplication of positive fractions is equal with  .Q or ·Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
 Q.  Q.  .Q ·Q0
 
10-Nov-2019nqnq0a 6303 Addition of positive fractions is equal with  +Q or +Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
 Q.  Q.  +Q +Q0
 
10-Nov-2019nqnq0pi 6287 A non-negative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)
 N.  N.  <. ,  >. ~Q0  <. ,  >.  ~Q
 
10-Nov-2019nnppipi 6196 A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
 om  N.  +o  N.
 
9-Nov-2019prarloclem3step 6344 Induction step for prarloclem3 6345. (Contributed by Jim Kingdon, 9-Nov-2019.)
 X  om  <. L ,  U >. 
 P.  L  P  Q.  om +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  suc  X ,  1o >. 
 ~Q  .Q  P  U  om +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  X ,  1o >.  ~Q  .Q  P  U
 
8-Nov-2019genpcuu 6369 Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   &    
 Q.  Q.  G 
 Q.   &     P.  2nd `  P.  h  2nd `  Q.  G h 
 <Q  2nd `  F   =>     P.  P.  2nd `  F  <Q  2nd `  F
 
7-Nov-2019genppreclu 6363 Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.)
 F  P. ,  P.  |->  <. {  Q.  | 
 Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.   &    
 Q.  Q.  G 
 Q.   =>     P.  P.  C  2nd `  D  2nd `  C G D  2nd `  F
 
7-Nov-2019prnminu 6337 An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.)
 <. L ,  U >.  P.  U  U  <Q
 
5-Nov-2019prarloclemn 6347 Subtracting two from a positive integer. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 5-Nov-2019.)
 N  N.  1o  <N  N  om  2o  +o  N
 
5-Nov-2019nq0a0 6306 Addition with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
Q0 +Q0 0Q0
 
5-Nov-2019nq0m0r 6305 Multiplication with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
Q0 0Q0 ·Q0 0Q0
 
5-Nov-2019df-0nq0 6275 Define non-negative fraction constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 5-Nov-2019.)
0Q0 
 <. (/) ,  1o >. ~Q0
 
4-Nov-2019prarloclem5 6348 A substitution of zero for and  N minus two for . Lemma for prarloc 6351. (Contributed by Jim Kingdon, 4-Nov-2019.)
 <. L ,  U >.  P.  L  N  N.  P  Q.  1o  <N  N  +Q  <. N ,  1o >.  ~Q  .Q  P  U  om  om +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  ,  1o >.  ~Q  .Q  P  U
 
4-Nov-2019prarloclem4 6346 A slight rearrangement of prarloclem3 6345. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 4-Nov-2019.)
 <. L ,  U >.  P.  L  P  Q.  om  om +Q0  <. ,  1o >. ~Q0 ·Q0  P  L  +Q  <. 
 +o  2o  +o  ,  1o >.  ~Q  .Q  P  U  j  om +Q0  <. j ,  1o >. ~Q0 ·Q0  P  L  +Q  <. j  +o  2o ,  1o >. 
 ~Q  .Q  P