P. 119 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11801-11900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uz2m1nn 11801	One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ ℕ)
Theorem	1nuz2 11802	1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ ¬ 1 ∈ (ℤ≥‘2)
Theorem	elnn1uz2 11803	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2)))
Theorem	uz2mulcl 11804	Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2))
Theorem	indstr2 11805*	Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜒    &   ⊢ (𝑥 ∈ (ℤ≥‘2) → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	uzinfi 11806	Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ inf((ℤ≥‘𝑀), ℝ, < ) = 𝑀
Theorem	nninf 11807	The infimum of the set of positive integers is one. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.)
⊢ inf(ℕ, ℝ, < ) = 1
Theorem	nn0inf 11808	The infimum of the set of nonnegative integers is zero. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.)
⊢ inf(ℕ0, ℝ, < ) = 0
Theorem	infssuzle 11809	The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝐴 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝐴)
Theorem	infssuzcl 11810	The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → inf(𝑆, ℝ, < ) ∈ 𝑆)
Theorem	ublbneg 11811*	The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦)
Theorem	eqreznegel 11812*	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴})
Theorem	supminf 11813*	The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011.) ( Revised by AV, 13-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))
Theorem	lbzbi 11814*	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))
Theorem	zsupss 11815*	Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 10052.) (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	suprzcl2 11816*	The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 11495 avoids ax-pre-sup 10052.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	suprzub 11817*	The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	uzsupss 11818*	Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 21-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	nn01to3 11819	A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3))
Theorem	nn0ge2m1nnALT 11820	Alternate proof of nn0ge2m1nn 11398: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 11731, a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn 11398. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ)
5.4.12  Well-ordering principle for bounded-below sets of integers
Theorem	uzwo3 11821*	Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 11790 allows the lower bound 𝐵 to be any real number. See also nnwo 11791 and nnwos 11793. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.)
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	zmin 11822*	There is a unique smallest integer greater than or equal to a given real number. (Contributed by NM, 12-Nov-2004.) (Revised by Mario Carneiro, 13-Jun-2014.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)))
Theorem	zmax 11823*	There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))
Theorem	zbtwnre 11824*	There is a unique integer between a real number and the number plus one. Exercise 5 of [Apostol] p. 28. (Contributed by NM, 13-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1)))
Theorem	rebtwnz 11825*	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 11826	Extend class notation to include the class of rationals.
class ℚ
Definition	df-q 11827	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 11828 for the relation "is rational." (Contributed by NM, 8-Jan-2002.)
⊢ ℚ = ( / “ (ℤ × ℕ))
Theorem	elq 11828*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	qmulz 11829*	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 11830	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qre 11831	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
Theorem	zq 11832	An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
Theorem	zssq 11833	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
⊢ ℤ ⊆ ℚ
Theorem	nn0ssq 11834	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ0 ⊆ ℚ
Theorem	nnssq 11835	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ ⊆ ℚ
Theorem	qssre 11836	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
⊢ ℚ ⊆ ℝ
Theorem	qsscn 11837	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℚ ⊆ ℂ
Theorem	qex 11838	The set of rational numbers exists. See also qexALT 11841. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℚ ∈ V
Theorem	nnq 11839	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ)
Theorem	qcn 11840	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
Theorem	qexALT 11841	Alternate proof of qex 11838. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℚ ∈ V
Theorem	qaddcl 11842	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)
Theorem	qnegcl 11843	Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ)
Theorem	qmulcl 11844	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ)
Theorem	qsubcl 11845	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ)
Theorem	qreccl 11846	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ)
Theorem	qdivcl 11847	Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qrevaddcl 11848	Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ))
Theorem	nnrecq 11849	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ)
Theorem	irradd 11850	The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	irrmul 11851	The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ))
5.4.14  Existence of the set of complex numbers
Theorem	rpnnen1lem2 11852*	Lemma for rpnnen1 11858. (Contributed by Mario Carneiro, 12-May-2013.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(𝑇, ℝ, < ) ∈ ℤ)
Theorem	rpnnen1lem1 11853*	Lemma for rpnnen1 11858. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑𝑚 ℕ))
Theorem	rpnnen1lem3 11854*	Lemma for rpnnen1 11858. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)
Theorem	rpnnen1lem4 11855*	Lemma for rpnnen1 11858. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ)
Theorem	rpnnen1lem5 11856*	Lemma for rpnnen1 11858. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥)
Theorem	rpnnen1lem6 11857*	Lemma for rpnnen1 11858. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ ℝ ≼ (ℚ ↑𝑚 ℕ)
Theorem	rpnnen1 11858	One half of rpnnen 15000, 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 11857) 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 11064 and qex 11838, or nnexALT 11060 and qexALT 11841. 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    ⇒   ⊢ ℝ ≼ (ℚ ↑𝑚 ℕ)
Theorem	rpnnen1lem1OLD 11859*	Lemma for rpnnen1OLD 11863. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem1 11853 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑𝑚 ℕ))
Theorem	rpnnen1lem3OLD 11860*	Lemma for rpnnen1OLD 11863. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem3 11854 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)
Theorem	rpnnen1lem4OLD 11861*	Lemma for rpnnen1OLD 11863. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem4 11855 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ)
Theorem	rpnnen1lem5OLD 11862*	Lemma for rpnnen1OLD 11863. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem5 11856 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥)
Theorem	rpnnen1OLD 11863*	One half of rpnnen 15000, where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number 𝑥 to the sequence (𝐹‘𝑥):ℕ⟶ℚ 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. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 16-Jun-2013.) Obsolete version of rpnnen1 11858 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ ℝ ≼ (ℚ ↑𝑚 ℕ)
Theorem	reexALT 11864	Alternate proof of reex 10065. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℝ ∈ V
Theorem	cnref1o 11865*	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 9980), 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-1-onto→ℂ
Theorem	cnexALT 11866	The set of complex numbers exists. This theorem shows that ax-cnex 10030 is redundant if we assume ax-rep 4804. See also ax-cnex 10030. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	xrex 11867	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
⊢ ℝ* ∈ V
Theorem	addex 11868	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ + ∈ V
Theorem	mulex 11869	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 11870	Extend class notation to include the class of positive reals.
class ℝ+
Definition	df-rp 11871	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
Theorem	elrp 11872	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	elrpii 11873	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ∈ ℝ+
Theorem	1rp 11874	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ 1 ∈ ℝ+
Theorem	2rp 11875	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ 2 ∈ ℝ+
Theorem	3rp 11876	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 3 ∈ ℝ+
Theorem	rpre 11877	A positive real is a real. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
Theorem	rpxr 11878	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)
Theorem	rpcn 11879	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)
Theorem	nnrp 11880	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Theorem	rpssre 11881	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
⊢ ℝ+ ⊆ ℝ
Theorem	rpgt0 11882	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
Theorem	rpge0 11883	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
Theorem	rpregt0 11884	A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	rprege0 11885	A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rpne0 11886	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
Theorem	rprene0 11887	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0))
Theorem	rpcnne0 11888	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
Theorem	rpcndif0 11889	A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ {0}))
Theorem	ralrp 11890	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑))
Theorem	rexrp 11891	Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑))
Theorem	rpaddcl 11892	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℝ+)
Theorem	rpmulcl 11893	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)
Theorem	rpdivcl 11894	Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
Theorem	rpreccl 11895	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+)
Theorem	rphalfcl 11896	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+)
Theorem	rpgecl 11897	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ+)
Theorem	rphalflt 11898	Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴)
Theorem	rerpdivcl 11899	Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	ge0p1rp 11900	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈ ℝ+)