P. 74 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7301-7400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	acfun 7301*	A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.)
|- ( ph -> CHOICE )   &    |- ( ph -> A e. V )   &    |- ( 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	exmidaclem 7302*	Lemma for exmidac 7303. 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 7303	The axiom of choice implies excluded middle. See acexmid 5933 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 7304	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 7305	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ⊔ C ) ~~ ( B ⊔ D ) )
Theorem	djuenun 7306	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 7307	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 7308	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 7309	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 7310	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 7311	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 7312	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 7313	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 7314	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 7315	Lemma for exmidontriim 7319. A variation of r19.30dc 2652. (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 7316*	Lemma for exmidontriim 7319. (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 7317*	Lemma for exmidontriim 7319. 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 7318*	Lemma for exmidontriim 7319. 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 7319*	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	pw1on 7320	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
|- ~P 1o e. On
Theorem	pw1dom2 7321	The power set of 1o dominates 2o. Also see pwpw0ss 3844 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
|- 2o ~<_ ~P 1o
Theorem	pw1ne0 7322	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= (/)
Theorem	pw1ne1 7323	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 1o
Theorem	pw1ne3 7324	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 3o
Theorem	pw1nel3 7325	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 7326	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 7327	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 7328	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 7329	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 7330	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 7331*	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 7332), (3) implies (5) (onntri35 7331), (5) implies (1) (onntri51 7334), (2) implies (4) (onntri24 7336), (4) implies (5) (onntri45 7335), and (5) implies (2) (onntri52 7338). 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 7333 and exmidontri2or 7337, respectively. Thus -. -. EXMID is equivalent to (1) or (2). In addition, -. -. EXMID is equivalent to (3) by onntri3or 7339 and (4) by onntri2or 7340. (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 7332	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 7333*	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 7334*	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 7335*	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 7336	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 7337*	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 7338*	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 7339*	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 7340*	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 ) )
2.6.46  Apartness relations
Syntax	wap 7341	Apartness predicate symbol.
wff R Ap A
Definition	df-pap 7342*	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 7343	Tight apartness predicate symbol.
wff R TAp A
Definition	df-tap 7344*	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 7345*	Tight apartness with the apartness properties from df-pap 7342 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 7346	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
|- ( R = S -> ( R TAp A <-> S TAp A ) )
Theorem	tapeq2 7347	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
|- ( A = B -> ( R TAp A <-> R TAp B ) )
Theorem	netap 7348*	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 7349*	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 7350*	(/) 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 7351*	Lemma for 2omotap 7353. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( -. -. ph -> { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ ( ph /\ u =/= v ) ) } TAp 2o )
Theorem	2omotaplemst 7352*	Lemma for 2omotap 7353. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( ( E* r r TAp 2o /\ -. -. ph ) -> ph )
Theorem	2omotap 7353	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 7354*	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 7355*	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 7300 but since it implies excluded middle as shown at exmidac 7303, 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 7356	Formula for an abbreviation of countable choice.
wff CCHOICE
Definition	df-cc 7357*	The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7300 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 7358*	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 7359*	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 7360*	Lemma for cc2 7361. (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 7361*	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 7362*	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 7363*	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 7364*	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 7365*	Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7364, 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 7366	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 6550 and similar theorems ), going from there to positive integers (df-ni 7399) and then positive rational numbers (df-nqqs 7443) 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 7561. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 8027 and the MacNeille reals fail to satisfy axltwlin 8122, 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 7367	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 7368	Positive integer addition.
class +N
Syntax	cmi 7369	Positive integer multiplication.
class .N
Syntax	clti 7370	Positive integer ordering relation.
class <N
Syntax	cplpq 7371	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 7372	Positive pre-fraction multiplication.
class .pQ
Syntax	cltpq 7373	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 7374	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 7375	Set of positive fractions.
class Q.
Syntax	c1q 7376	The positive fraction constant 1.
class 1Q
Syntax	cplq 7377	Positive fraction addition.
class +Q
Syntax	cmq 7378	Positive fraction multiplication.
class .Q
Syntax	crq 7379	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 7380	Positive fraction ordering relation.
class <Q
Syntax	ceq0 7381	Equivalence class used to construct nonnegative fractions.
class ~Q0
Syntax	cnq0 7382	Set of nonnegative fractions.
class Q0
Syntax	c0q0 7383	The nonnegative fraction constant 0.
class 0Q0
Syntax	cplq0 7384	Nonnegative fraction addition.
class +Q0
Syntax	cmq0 7385	Nonnegative fraction multiplication.
class ·Q0
Syntax	cnp 7386	Set of positive reals.
class P.
Syntax	c1p 7387	Positive real constant 1.
class 1P
Syntax	cpp 7388	Positive real addition.
class +P.
Syntax	cmp 7389	Positive real multiplication.
class .P.
Syntax	cltp 7390	Positive real ordering relation.
class <P
Syntax	cer 7391	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 7392	Set of signed reals.
class R.
Syntax	c0r 7393	The signed real constant 0.
class 0R
Syntax	c1r 7394	The signed real constant 1.
class 1R
Syntax	cm1r 7395	The signed real constant -1.
class -1R
Syntax	cplr 7396	Signed real addition.
class +R
Syntax	cmr 7397	Signed real multiplication.
class .R
Syntax	cltr 7398	Signed real ordering relation.
class <R
Definition	df-ni 7399	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.)
|- N. = ( om \ { (/) } )
Definition	df-pli 7400	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
|- +N = ( +o |` ( N. X. N. ) )