P. 108 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10701-10800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	addclnq 10701	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) ∈ Q)
Theorem	mulpqf 10702	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
Theorem	mulclnq 10703	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) ∈ Q)
Theorem	addnqf 10704	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ +Q :(Q × Q)⟶Q
Theorem	mulnqf 10705	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ ·Q :(Q × Q)⟶Q
Theorem	addcompq 10706	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 +pQ 𝐵) = (𝐵 +pQ 𝐴)
Theorem	addcomnq 10707	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴)
Theorem	mulcompq 10708	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ·pQ 𝐵) = (𝐵 ·pQ 𝐴)
Theorem	mulcomnq 10709	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴)
Theorem	adderpqlem 10710	Lemma for adderpq 10712. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 +pQ 𝐶) ~Q (𝐵 +pQ 𝐶)))
Theorem	mulerpqlem 10711	Lemma for mulerpq 10713. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 ·pQ 𝐶) ~Q (𝐵 ·pQ 𝐶)))
Theorem	adderpq 10712	Addition is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (([Q]‘𝐴) +Q ([Q]‘𝐵)) = ([Q]‘(𝐴 +pQ 𝐵))
Theorem	mulerpq 10713	Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (([Q]‘𝐴) ·Q ([Q]‘𝐵)) = ([Q]‘(𝐴 ·pQ 𝐵))
Theorem	addassnq 10714	Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ ((𝐴 +Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q 𝐶))
Theorem	mulassnq 10715	Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵 ·Q 𝐶))
Theorem	mulcanenq 10716	Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ⟨(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)⟩ ~Q ⟨𝐵, 𝐶⟩)
Theorem	distrnq 10717	Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶))
Theorem	1nqenq 10718	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 1Q ~Q ⟨𝐴, 𝐴⟩)
Theorem	mulidnq 10719	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = 𝐴)
Theorem	recmulnq 10720	Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
Theorem	recidnq 10721	A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → (𝐴 ·Q (*Q‘𝐴)) = 1Q)
Theorem	recclnq 10722	Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ Q)
Theorem	recrecnq 10723	Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → (*Q‘(*Q‘𝐴)) = 𝐴)
Theorem	dmrecnq 10724	Domain of reciprocal on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ dom *Q = Q
Theorem	ltsonq 10725	'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.) (New usage is discouraged.)
⊢ <Q Or Q
Theorem	lterpq 10726	Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.)
⊢ (𝐴 <pQ 𝐵 ↔ ([Q]‘𝐴) <Q ([Q]‘𝐵))
Theorem	ltanq 10727	Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐶 ∈ Q → (𝐴 <Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵)))
Theorem	ltmnq 10728	Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐶 ∈ Q → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
Theorem	1lt2nq 10729	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ 1Q <Q (1Q +Q 1Q)
Theorem	ltaddnq 10730	The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐴 <Q (𝐴 +Q 𝐵))
Theorem	ltexnq 10731*	Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by NM, 24-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐵 ∈ Q → (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 +Q 𝑥) = 𝐵))
Theorem	halfnq 10732*	One-half of any positive fraction exists. Lemma for Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 16-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → ∃𝑥(𝑥 +Q 𝑥) = 𝐴)
Theorem	nsmallnq 10733*	The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → ∃𝑥 𝑥 <Q 𝐴)
Theorem	ltbtwnnq 10734*	There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))
Theorem	ltrnq 10735	Ordering property of reciprocal for positive fractions. Proposition 9-2.6(iv) of [Gleason] p. 120. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐴 <Q 𝐵 ↔ (*Q‘𝐵) <Q (*Q‘𝐴))
Theorem	archnq 10736*	For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ N 𝐴 <Q ⟨𝑥, 1o⟩)
Definition	df-np 10737*	Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. A positive real is defined as the lower class of a Dedekind cut. Definition 9-3.1 of [Gleason] p. 121. (Note: This is a "temporary" definition used in the construction of complex numbers df-c 10877, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
⊢ P = {𝑥 ∣ ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧ ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))}
Definition	df-1p 10738	Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10877, and is intended to be used only by the construction. Definition of [Gleason] p. 122. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ 1P = {𝑥 ∣ 𝑥 <Q 1Q}
Definition	df-plp 10739*	Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10877, and is intended to be used only by the construction. From Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 +Q 𝑢)})
Definition	df-mp 10740*	Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10877, and is intended to be used only by the construction. From Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
⊢ ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 ·Q 𝑢)})
Definition	df-ltp 10741*	Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10877, and is intended to be used only by the construction. From Proposition 9-3.2 of [Gleason] p. 122. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ 𝑥 ⊊ 𝑦)}
Theorem	npex 10742	The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
⊢ P ∈ V
Theorem	elnp 10743*	Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ P ↔ ((∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))
Theorem	elnpi 10744*	Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ P ↔ ((𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦)))
Theorem	prn0 10745	A positive real is not empty. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ P → 𝐴 ≠ ∅)
Theorem	prpssnq 10746	A positive real is a subset of the positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ P → 𝐴 ⊊ Q)
Theorem	elprnq 10747	A positive real is a set of positive fractions. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q)
Theorem	0npr 10748	The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ P
Theorem	prcdnq 10749	A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of [Gleason] p. 121. (Contributed by NM, 25-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → (𝐶 <Q 𝐵 → 𝐶 ∈ 𝐴))
Theorem	prub 10750	A positive fraction not in a positive real is an upper bound. Remark (1) of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ Q) → (¬ 𝐶 ∈ 𝐴 → 𝐵 <Q 𝐶))
Theorem	prnmax 10751*	A positive real has no largest member. Definition 9-3.1(iii) of [Gleason] p. 121. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 <Q 𝑥)
Theorem	npomex 10752	A simplifying observation, and an indication of why any attempt to develop a theory of the real numbers without the Axiom of Infinity is doomed to failure: since every member of P is an infinite set, the negation of Infinity implies that P, and hence ℝ, is empty. (Note that this proof, which used the fact that Dedekind cuts have no maximum, could just as well have used that they have no minimum, since they are downward-closed by prcdnq 10749 and nsmallnq 10733). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.)
⊢ (𝐴 ∈ P → ω ∈ V)
Theorem	prnmadd 10753*	A positive real has no largest member. Addition version. (Contributed by NM, 7-Apr-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → ∃𝑥(𝐵 +Q 𝑥) ∈ 𝐴)
Theorem	ltrelpr 10754	Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
⊢ <P ⊆ (P × P)
Theorem	genpv 10755*	Value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) = {𝑓 ∣ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ)})
Theorem	genpelv 10756*	Membership in value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐶 ∈ (𝐴𝐹𝐵) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝐶 = (𝑔𝐺ℎ)))
Theorem	genpprecl 10757*	Pre-closure law for general operation on positive reals. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐺𝐷) ∈ (𝐴𝐹𝐵)))
Theorem	genpdm 10758*	Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ dom 𝐹 = (P × P)
Theorem	genpn0 10759*	The result of an operation on positive reals is not empty. (Contributed by NM, 28-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∅ ⊊ (𝐴𝐹𝐵))
Theorem	genpss 10760*	The result of an operation on positive reals is a subset of the positive fractions. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) ⊆ Q)
Theorem	genpnnp 10761*	The result of an operation on positive reals is different from the set of positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ (𝑧 ∈ Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))    &   ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ¬ (𝐴𝐹𝐵) = Q)
Theorem	genpcd 10762*	Downward closure of an operation on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔𝐺ℎ) → 𝑥 ∈ (𝐴𝐹𝐵)))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑓 ∈ (𝐴𝐹𝐵) → (𝑥 <Q 𝑓 → 𝑥 ∈ (𝐴𝐹𝐵))))
Theorem	genpnmax 10763*	An operation on positive reals has no largest member. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ (𝑣 ∈ Q → (𝑧 <Q 𝑤 ↔ (𝑣𝐺𝑧) <Q (𝑣𝐺𝑤)))    &   ⊢ (𝑧𝐺𝑤) = (𝑤𝐺𝑧)    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑓 ∈ (𝐴𝐹𝐵) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))
Theorem	genpcl 10764*	Closure of an operation on reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ (ℎ ∈ Q → (𝑓 <Q 𝑔 ↔ (ℎ𝐺𝑓) <Q (ℎ𝐺𝑔)))    &   ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)    &   ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔𝐺ℎ) → 𝑥 ∈ (𝐴𝐹𝐵)))    ⇒   ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) ∈ P)
Theorem	genpass 10765*	Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)})    &   ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)    &   ⊢ dom 𝐹 = (P × P)    &   ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)    &   ⊢ ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))    ⇒   ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
Theorem	plpv 10766*	Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦 +Q 𝑧)})
Theorem	mpv 10767*	Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦 ·Q 𝑧)})
Theorem	dmplp 10768	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
⊢ dom +P = (P × P)
Theorem	dmmp 10769	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
⊢ dom ·P = (P × P)
Theorem	nqpr 10770*	The canonical embedding of the rationals into the reals. (Contributed by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → {𝑥 ∣ 𝑥 <Q 𝐴} ∈ P)
Theorem	1pr 10771	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 1P ∈ P
Theorem	addclprlem1 10772	Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔 +Q ℎ) → ((𝑥 ·Q (*Q‘(𝑔 +Q ℎ))) ·Q 𝑔) ∈ 𝐴))
Theorem	addclprlem2 10773*	Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔 +Q ℎ) → 𝑥 ∈ (𝐴 +P 𝐵)))
Theorem	addclpr 10774	Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) ∈ P)
Theorem	mulclprlem 10775*	Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 14-Mar-1996.) (New usage is discouraged.)
⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q (𝑔 ·Q ℎ) → 𝑥 ∈ (𝐴 ·P 𝐵)))
Theorem	mulclpr 10776	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) ∈ P)
Theorem	addcompr 10777	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 +P 𝐵) = (𝐵 +P 𝐴)
Theorem	addasspr 10778	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 +P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P 𝐶))
Theorem	mulcompr 10779	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ·P 𝐵) = (𝐵 ·P 𝐴)
Theorem	mulasspr 10780	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ·P 𝐵) ·P 𝐶) = (𝐴 ·P (𝐵 ·P 𝐶))
Theorem	distrlem1pr 10781	Lemma for distributive law for positive reals. (Contributed by NM, 1-May-1996.) (Revised by Mario Carneiro, 13-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴 ·P (𝐵 +P 𝐶)) ⊆ ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶)))
Theorem	distrlem4pr 10782*	Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P 𝐶)))
Theorem	distrlem5pr 10783	Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶)) ⊆ (𝐴 ·P (𝐵 +P 𝐶)))
Theorem	distrpr 10784	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ·P (𝐵 +P 𝐶)) = ((𝐴 ·P 𝐵) +P (𝐴 ·P 𝐶))
Theorem	1idpr 10785	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ P → (𝐴 ·P 1P) = 𝐴)
Theorem	ltprord 10786	Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<P 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	psslinpr 10787	Proper subset is a linear ordering on positive reals. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
Theorem	ltsopr 10788	Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
⊢ <P Or P
Theorem	prlem934 10789*	Lemma 9-3.4 of [Gleason] p. 122. (Contributed by NM, 25-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴)
Theorem	ltaddpr 10790	The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → 𝐴<P (𝐴 +P 𝐵))
Theorem	ltaddpr2 10791	The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ P → ((𝐴 +P 𝐵) = 𝐶 → 𝐴<P 𝐶))
Theorem	ltexprlem1 10792*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → (𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅))
Theorem	ltexprlem2 10793*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → 𝐶 ⊊ Q)
Theorem	ltexprlem3 10794*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → (𝑥 ∈ 𝐶 → ∀𝑧(𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶)))
Theorem	ltexprlem4 10795*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (𝐵 ∈ P → (𝑥 ∈ 𝐶 → ∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧)))
Theorem	ltexprlem5 10796*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ ((𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵) → 𝐶 ∈ P)
Theorem	ltexprlem6 10797*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ 𝐴 ⊊ 𝐵) → (𝐴 +P 𝐶) ⊆ 𝐵)
Theorem	ltexprlem7 10798*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}    ⇒   ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ 𝐴 ⊊ 𝐵) → 𝐵 ⊆ (𝐴 +P 𝐶))
Theorem	ltexpri 10799*	Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ (𝐴<P 𝐵 → ∃𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵)
Theorem	ltaprlem 10800	Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))