P. 132 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rebtwnz 13101*	There is a unique greatest integer less than or equal to a real number. Exercise 4 of [Apostol] p. 28. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))
5.4.13  Rational numbers (as a subset of complex numbers)
Syntax	cq 13102	Extend class notation to include the class of rationals.
class ℚ
Definition	df-q 13103	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 13104 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
⊢ ℚ = ( / “ (ℤ × ℕ))
Theorem	elq 13104*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	qmulz 13105*	If 𝐴 is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐴 ∈ ℚ → ∃𝑥 ∈ ℕ (𝐴 · 𝑥) ∈ ℤ)
Theorem	znq 13106	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qre 13107	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
Theorem	zq 13108	An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
Theorem	qred 13109	A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	zssq 13110	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
⊢ ℤ ⊆ ℚ
Theorem	nn0ssq 13111	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ0 ⊆ ℚ
Theorem	nnssq 13112	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ ⊆ ℚ
Theorem	qssre 13113	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
⊢ ℚ ⊆ ℝ
Theorem	qsscn 13114	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℚ ⊆ ℂ
Theorem	qex 13115	The set of rational numbers exists. See also qexALT 13118. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℚ ∈ V
Theorem	nnq 13116	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ)
Theorem	qcn 13117	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
Theorem	qexALT 13118	Alternate proof of qex 13115. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℚ ∈ V
Theorem	1q 13119	The number 1 is rational. (Contributed by SN, 30-Aug-2026.)
⊢ 1 ∈ ℚ
Theorem	qaddcl 13120	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)
Theorem	qnegcl 13121	Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ)
Theorem	qmulcl 13122	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ)
Theorem	qsubcl 13123	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ)
Theorem	qreccl 13124	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ)
Theorem	qdivcl 13125	Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qrevaddcl 13126	Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ))
Theorem	nnrecq 13127	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ)
Theorem	irradd 13128	The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	irrmul 13129	The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	elpq 13130*	A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	elpqb 13131*	A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
5.4.14  Existence of the set of complex numbers
Theorem	rpnnen1lem2 13132*	Lemma for rpnnen1 13138. (Contributed by Mario Carneiro, 12-May-2013.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(𝑇, ℝ, < ) ∈ ℤ)
Theorem	rpnnen1lem1 13133*	Lemma for rpnnen1 13138. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑m ℕ))
Theorem	rpnnen1lem3 13134*	Lemma for rpnnen1 13138. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)
Theorem	rpnnen1lem4 13135*	Lemma for rpnnen1 13138. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ)
Theorem	rpnnen1lem5 13136*	Lemma for rpnnen1 13138. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥)
Theorem	rpnnen1lem6 13137*	Lemma for rpnnen1 13138. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ ℝ ≼ (ℚ ↑m ℕ)
Theorem	rpnnen1 13138	One half of rpnnen 16424, where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number 𝑥 to the sequence (𝐹‘𝑥):ℕ⟶ℚ (see rpnnen1lem6 13137) such that ((𝐹‘𝑥)‘𝑘) is the largest rational number with denominator 𝑘 that is strictly less than 𝑥. In this manner, we get a monotonically increasing sequence that converges to 𝑥, and since each sequence converges to a unique real number, this mapping from reals to sequences of rational numbers is injective. Note: The ℕ and ℚ existence hypotheses provide for use with either nnex 12368 and qex 13115, or nnexALT 12364 and qexALT 13118. The proof should not be modified to use any of those 4 theorems. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 16-Jun-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.)
⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ ℝ ≼ (ℚ ↑m ℕ)
Theorem	reexALT 13139	Alternate proof of reex 11318. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℝ ∈ V
Theorem	cnref1o 13140*	There is a natural one-to-one mapping from (ℝ × ℝ) to ℂ, where we map ⟨𝑥, 𝑦⟩ to (𝑥 + (i · 𝑦)). In our construction of the complex numbers, this is in fact our definition of ℂ (see df-c 11233), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ 𝐹:(ℝ × ℝ)⟶1-1ontoℂ
Theorem	cnexALT 13141	The set of complex numbers exists. This theorem shows that ax-cnex 11283 is redundant if we assume ax-rep 5235. See also ax-cnex 11283. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	xrex 13142	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
⊢ ℝ* ∈ V
Theorem	mpoaddex 13143*	The addition operation is a set. Version of addex 13144 using maps-to notation , which does not require ax-addf 11306. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) ∈ V
Theorem	addex 13144	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ + ∈ V
Theorem	mpomulex 13145*	The multiplication operation is a set. Version of mulex 13146 using maps-to notation , which does not require ax-mulf 11307. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ V
Theorem	mulex 13146	The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ · ∈ V
5.5  Order sets
5.5.1  Positive reals (as a subset of complex numbers)
Syntax	crp 13147	Extend class notation to include the class of positive reals.
class ℝ+
Definition	df-rp 13148	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
Theorem	elrp 13149	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	elrpii 13150	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ∈ ℝ+
Theorem	1rp 13151	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ 1 ∈ ℝ+
Theorem	2rp 13152	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ 2 ∈ ℝ+
Theorem	3rp 13153	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 3 ∈ ℝ+
Theorem	5rp 13154	5 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 5 ∈ ℝ+
Theorem	rpssre 13155	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
⊢ ℝ+ ⊆ ℝ
Theorem	rpre 13156	A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
Theorem	rpxr 13157	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)
Theorem	rpcn 13158	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)
Theorem	nnrp 13159	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Theorem	rpgt0 13160	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
Theorem	rpge0 13161	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
Theorem	rpregt0 13162	A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	rprege0 13163	A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rpne0 13164	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
Theorem	rprene0 13165	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0))
Theorem	rpcnne0 13166	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
Theorem	neglt 13167	The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ+ → -𝐴 < 𝐴)
Theorem	rpcndif0 13168	A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ {0}))
Theorem	ralrp 13169	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑))
Theorem	rexrp 13170	Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑))
Theorem	rpaddcl 13171	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℝ+)
Theorem	rpmulcl 13172	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)
Theorem	rpmtmip 13173	"Minus times minus is plus", see also nnmtmip 12391, holds for positive reals, too (formalized to "The product of two negative reals is a positive real"). "The reason for this" in this case is that ( -𝐴 · -𝐵) = (𝐴 · 𝐵) for all complex numbers 𝐴 and 𝐵 because of mul2neg 11782, 𝐴 and 𝐵 are complex numbers because of rpcn 13158, and (𝐴 · 𝐵) ∈ ℝ+ because of rpmulcl 13172. Note that the opposites -𝐴 and -𝐵 of the positive reals 𝐴 and 𝐵 are negative reals. (Contributed by AV, 23-Dec-2022.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ( -𝐴 · -𝐵) ∈ ℝ+)
Theorem	rpdivcl 13174	Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
Theorem	rpreccl 13175	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+)
Theorem	rphalfcl 13176	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+)
Theorem	rpgecl 13177	A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ+)
Theorem	rphalflt 13178	Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴)
Theorem	rerpdivcl 13179	Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	ge0p1rp 13180	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈ ℝ+)
Theorem	rpneg 13181	Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of [Apostol] p. 20. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 ∈ ℝ+ ↔ ¬ -𝐴 ∈ ℝ+))
Theorem	negelrp 13182	Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.)
⊢ (𝐴 ∈ ℝ → ( -𝐴 ∈ ℝ+ ↔ 𝐴 < 0))
Theorem	negelrpd 13183	The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℝ+)
Theorem	0nrp 13184	Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ¬ 0 ∈ ℝ+
Theorem	ltsubrp 13185	Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 − 𝐵) < 𝐴)
Theorem	ltaddrp 13186	Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵))
Theorem	difrp 13187	Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℝ+))
Theorem	elrpd 13188	Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ+)
Theorem	nnrpd 13189	A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ+)
Theorem	zgt1rpn0n1 13190	An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g., base 2, base 3, or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017.) (Proof shortened by AV, 9-Jul-2022.)
⊢ (𝐵 ∈ (ℤ≥‘2) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1))
Theorem	rpred 13191	A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rpxrd 13192	A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	rpcnd 13193	A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	rpgt0d 13194	A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	rpge0d 13195	A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 ≤ 𝐴)
Theorem	rpne0d 13196	A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	rpregt0d 13197	A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	rprege0d 13198	A positive real is real and greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rprene0d 13199	A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0))
Theorem	rpcnne0d 13200	A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))