P. 75 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exmidaclem 7401*	Lemma for exmidac 7402. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }   &    |- C = { A , B }   =>    |- (CHOICE -> EXMID )
Theorem	exmidac 7402	The axiom of choice implies excluded middle. See acexmid 6006 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.)
|- (CHOICE -> EXMID )
2.6.43  Cardinal number arithmetic
Theorem	endjudisj 7403	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( A ⊔ B ) ~~ ( A u. B ) )
Theorem	djuen 7404	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ⊔ C ) ~~ ( B ⊔ D ) )
Theorem	djuenun 7405	Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A ⊔ C ) ~~ ( B u. D ) )
Theorem	dju1en 7406	Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ -. A e. A ) -> ( A ⊔ 1o ) ~~ suc A )
Theorem	dju0en 7407	Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. V -> ( A ⊔ (/) ) ~~ A )
Theorem	xp2dju 7408	Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( 2o X. A ) = ( A ⊔ A )
Theorem	djucomen 7409	Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) ~~ ( B ⊔ A ) )
Theorem	djuassen 7410	Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ⊔ B ) ⊔ C ) ~~ ( A ⊔ ( B ⊔ C ) ) )
Theorem	xpdjuen 7411	Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. ( B ⊔ C ) ) ~~ ( ( A X. B ) ⊔ ( A X. C ) ) )
Theorem	djudoml 7412	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> A ~<_ ( A ⊔ B ) )
Theorem	djudomr 7413	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> B ~<_ ( A ⊔ B ) )
2.6.44  Ordinal trichotomy
Theorem	exmidontriimlem1 7414	Lemma for exmidontriim 7418. A variation of r19.30dc 2678. (Contributed by Jim Kingdon, 12-Aug-2024.)
|- ( ( A. x e. A ( ph \/ ps \/ ch ) /\ EXMID ) -> ( E. x e. A ph \/ E. x e. A ps \/ A. x e. A ch ) )
Theorem	exmidontriimlem2 7415*	Lemma for exmidontriim 7418. (Contributed by Jim Kingdon, 12-Aug-2024.)
|- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. y e. B ( A e. y \/ A = y \/ y e. A ) )   =>    |- ( ph -> ( A e. B \/ A. y e. B y e. A ) )
Theorem	exmidontriimlem3 7416*	Lemma for exmidontriim 7418. What we get to do based on induction on both A and B. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. z e. A A. y e. On ( z e. y \/ z = y \/ y e. z ) )   &    |- ( ph -> A. y e. B ( A e. y \/ A = y \/ y e. A ) )   =>    |- ( ph -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	exmidontriimlem4 7417*	Lemma for exmidontriim 7418. The induction step for the induction on A. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. z e. A A. y e. On ( z e. y \/ z = y \/ y e. z ) )   =>    |- ( ph -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	exmidontriim 7418*	Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- (EXMID -> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
2.6.45  Excluded middle and the power set of a singleton
Theorem	iftrueb01 7419	Using an if expression to represent a truth value by (/) or 1o. Unlike some theorems using if, ph does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- ( if ( ph , 1o , (/) ) = 1o <-> ph )
Theorem	pw1m 7420*	A truth value which is inhabited is equal to true. This is a variation of pwntru 4283 and pwtrufal 16422. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )
Theorem	pw1if 7421	Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. ~P 1o -> if ( A = 1o , 1o , (/) ) = A )
Theorem	pw1on 7422	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
|- ~P 1o e. On
Theorem	pw1dom2 7423	The power set of 1o dominates 2o. Also see pwpw0ss 3883 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
|- 2o ~<_ ~P 1o
Theorem	pw1ne0 7424	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= (/)
Theorem	pw1ne1 7425	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 1o
Theorem	pw1ne3 7426	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 3o
Theorem	pw1nel3 7427	Negated excluded middle implies that the power set of 1o is not an element of 3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ( -. EXMID -> -. ~P 1o e. 3o )
Theorem	sucpw1ne3 7428	Negated excluded middle implies that the successor of the power set of 1o is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ( -. EXMID -> suc ~P 1o =/= 3o )
Theorem	sucpw1nel3 7429	The successor of the power set of 1o is not an element of 3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- -. suc ~P 1o e. 3o
Theorem	3nelsucpw1 7430	Three is not an element of the successor of the power set of 1o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- -. 3o e. suc ~P 1o
Theorem	sucpw1nss3 7431	Negated excluded middle implies that the successor of the power set of 1o is not a subset of 3o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
|- ( -. EXMID -> -. suc ~P 1o C_ 3o )
Theorem	3nsssucpw1 7432	Negated excluded middle implies that 3o is not a subset of the successor of the power set of 1o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
|- ( -. EXMID -> -. 3o C_ suc ~P 1o )
Theorem	onntri35 7433*	Double negated ordinal trichotomy. There are five equivalent statements: (1) -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ), (2) -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ), (3) A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ), (4) A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ), and (5) -. -. EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7434), (3) implies (5) (onntri35 7433), (5) implies (1) (onntri51 7436), (2) implies (4) (onntri24 7438), (4) implies (5) (onntri45 7437), and (5) implies (2) (onntri52 7440). Another way of stating this is that EXMID is equivalent to trichotomy, either the x e. y \/ x = y \/ y e. x or the x C_ y \/ y C_ x form, as shown in exmidontri 7435 and exmidontri2or 7439, respectively. Thus -. -. EXMID is equivalent to (1) or (2). In addition, -. -. EXMID is equivalent to (3) by onntri3or 7441 and (4) by onntri2or 7442. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) -> -. -. EXMID )
Theorem	onntri13 7434	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) -> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
Theorem	exmidontri 7435*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
Theorem	onntri51 7436*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. EXMID -> -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
Theorem	onntri45 7437*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) -> -. -. EXMID )
Theorem	onntri24 7438	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ) -> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
Theorem	exmidontri2or 7439*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
Theorem	onntri52 7440*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. EXMID -> -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
Theorem	onntri3or 7441*	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
Theorem	onntri2or 7442*	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
Theorem	fmelpw1o 7443	With a formula ph one can associate an element of ~P 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than T. and F., by nndc 856, which translate to 1o and (/) respectively by iftrue 3607 and iffalse 3610, giving pwtrufal 16422). As proved in if0ab 16224, the associated element of ~P 1o is the extension, in ~P 1o, of the formula ph. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , 1o , (/) ) e. ~P 1o
2.6.46  Apartness relations
Syntax	wap 7444	Apartness predicate symbol.
wff R Ap A
Definition	df-pap 7445*	Apartness predicate. A relation R is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
|- ( R Ap A <-> ( ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) /\ ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) ) ) )
Syntax	wtap 7446	Tight apartness predicate symbol.
wff R TAp A
Definition	df-tap 7447*	Tight apartness predicate. A relation R is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
Theorem	dftap2 7448*	Tight apartness with the apartness properties from df-pap 7445 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
|- ( R TAp A <-> ( R C_ ( A X. A ) /\ ( A. x e. A -. x R x /\ A. x e. A A. y e. A ( x R y -> y R x ) ) /\ ( A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) )
Theorem	tapeq1 7449	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
|- ( R = S -> ( R TAp A <-> S TAp A ) )
Theorem	tapeq2 7450	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
|- ( A = B -> ( R TAp A <-> R TAp B ) )
Theorem	netap 7451*	Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
|- ( A. x e. A A. y e. A DECID x = y -> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } TAp A )
Theorem	2onetap 7452*	Negated equality is a tight apartness on 2o. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ u =/= v ) } TAp 2o
Theorem	2oneel 7453*	(/) and 1o are two unequal elements of 2o. (Contributed by Jim Kingdon, 8-Feb-2025.)
|- <. (/) , 1o >. e. { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ u =/= v ) }
Theorem	2omotaplemap 7454*	Lemma for 2omotap 7456. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( -. -. ph -> { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ ( ph /\ u =/= v ) ) } TAp 2o )
Theorem	2omotaplemst 7455*	Lemma for 2omotap 7456. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( ( E* r r TAp 2o /\ -. -. ph ) -> ph )
Theorem	2omotap 7456	If there is at most one tight apartness on 2o, excluded middle follows. Based on online discussions by Tom de Jong, Andrew W Swan, and Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( E* r r TAp 2o -> EXMID )
Theorem	exmidapne 7457*	Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
|- (EXMID -> ( R TAp A <-> R = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } ) )
Theorem	exmidmotap 7458*	The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
|- (EXMID <-> A. x E* r r TAp x )
PART 3  CHOICE PRINCIPLES We have already introduced the full Axiom of Choice df-ac 7399 but since it implies excluded middle as shown at exmidac 7402, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle.
3.1  Countable Choice and Dependent Choice
3.1.1  Introduce Countable Choice
Syntax	wacc 7459	Formula for an abbreviation of countable choice.
wff CCHOICE
Definition	df-cc 7460*	The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7399 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
Theorem	ccfunen 7461*	Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A ~~ om )   &    |- ( ph -> A. x e. A E. w w e. x )   =>    |- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. x ) )
Theorem	cc1 7462*	Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- (CCHOICE -> A. x ( ( x ~~ om /\ A. z e. x E. w w e. z ) -> E. f A. z e. x ( f ` z ) e. z ) )
Theorem	cc2lem 7463*	Lemma for cc2 7464. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> F Fn om )   &    |- ( ph -> A. x e. om E. w w e. ( F ` x ) )   &    |- A = ( n e. om |-> ( { n } X. ( F ` n ) ) )   &    |- G = ( n e. om |-> ( 2nd ` ( f ` ( A ` n ) ) ) )   =>    |- ( ph -> E. g ( g Fn om /\ A. n e. om ( g ` n ) e. ( F ` n ) ) )
Theorem	cc2 7464*	Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> F Fn om )   &    |- ( ph -> A. x e. om E. w w e. ( F ` x ) )   =>    |- ( ph -> E. g ( g Fn om /\ A. n e. om ( g ` n ) e. ( F ` n ) ) )
Theorem	cc3 7465*	Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A. n e. N F e. _V )   &    |- ( ph -> A. n e. N E. w w e. F )   &    |- ( ph -> N ~~ om )   =>    |- ( ph -> E. f ( f Fn N /\ A. n e. N ( f ` n ) e. F ) )
Theorem	cc4f 7466*	Countable choice by showing the existence of a function f which can choose a value at each index n such that ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A e. V )   &    |- F/_ n A   &    |- ( ph -> N ~~ om )   &    |- ( x = ( f ` n ) -> ( ps <-> ch ) )   &    |- ( ph -> A. n e. N E. x e. A ps )   =>    |- ( ph -> E. f ( f : N --> A /\ A. n e. N ch ) )
Theorem	cc4 7467*	Countable choice by showing the existence of a function f which can choose a value at each index n such that ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A e. V )   &    |- ( ph -> N ~~ om )   &    |- ( x = ( f ` n ) -> ( ps <-> ch ) )   &    |- ( ph -> A. n e. N E. x e. A ps )   =>    |- ( ph -> E. f ( f : N --> A /\ A. n e. N ch ) )
Theorem	cc4n 7468*	Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7467, the hypotheses only require an A(n) for each value of n, not a single set A which suffices for every n e. om. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A. n e. N { x e. A | ps } e. V )   &    |- ( ph -> N ~~ om )   &    |- ( x = ( f ` n ) -> ( ps <-> ch ) )   &    |- ( ph -> A. n e. N E. x e. A ps )   =>    |- ( ph -> E. f ( f Fn N /\ A. n e. N ch ) )
Theorem	acnccim 7469	Given countable choice, every set has choice sets of length om. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- (CCHOICE -> AC om = _V )
PART 4  REAL AND COMPLEX NUMBERS This section derives the basics of real and complex numbers. To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6628 and similar theorems ), going from there to positive integers (df-ni 7502) and then positive rational numbers (df-nqqs 7546) does not involve a major change in approach compared with the Metamath Proof Explorer. It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle or choice principles. With excluded middle, it is natural to define a cut as the lower set only (as Metamath Proof Explorer does), but here we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero". When working constructively, there are several possible definitions of real numbers. Here we adopt the most common definition, as two-sided Dedekind cuts with the properties described at df-inp 7664. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 8130 and the MacNeille reals fail to satisfy axltwlin 8225, and we do not develop them here. For more on differing definitions of the reals, see the introduction to Chapter 11 in [HoTT] or Section 1.2 of [BauerHanson].
4.1  Construction and axiomatization of real and complex numbers
4.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 7470	The set of positive integers, which is the set of natural numbers om with 0 removed. Note: This is the start of the Dedekind-cut construction of real and complex numbers.
class N.
Syntax	cpli 7471	Positive integer addition.
class +N
Syntax	cmi 7472	Positive integer multiplication.
class .N
Syntax	clti 7473	Positive integer ordering relation.
class <N
Syntax	cplpq 7474	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 7475	Positive pre-fraction multiplication.
class .pQ
Syntax	cltpq 7476	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 7477	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 7478	Set of positive fractions.
class Q.
Syntax	c1q 7479	The positive fraction constant 1.
class 1Q
Syntax	cplq 7480	Positive fraction addition.
class +Q
Syntax	cmq 7481	Positive fraction multiplication.
class .Q
Syntax	crq 7482	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 7483	Positive fraction ordering relation.
class <Q
Syntax	ceq0 7484	Equivalence class used to construct nonnegative fractions.
class ~Q0
Syntax	cnq0 7485	Set of nonnegative fractions.
class Q0
Syntax	c0q0 7486	The nonnegative fraction constant 0.
class 0Q0
Syntax	cplq0 7487	Nonnegative fraction addition.
class +Q0
Syntax	cmq0 7488	Nonnegative fraction multiplication.
class ·Q0
Syntax	cnp 7489	Set of positive reals.
class P.
Syntax	c1p 7490	Positive real constant 1.
class 1P
Syntax	cpp 7491	Positive real addition.
class +P.
Syntax	cmp 7492	Positive real multiplication.
class .P.
Syntax	cltp 7493	Positive real ordering relation.
class <P
Syntax	cer 7494	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 7495	Set of signed reals.
class R.
Syntax	c0r 7496	The signed real constant 0.
class 0R
Syntax	c1r 7497	The signed real constant 1.
class 1R
Syntax	cm1r 7498	The signed real constant -1.
class -1R
Syntax	cplr 7499	Signed real addition.
class +R
Syntax	cmr 7500	Signed real multiplication.
class .R