P. 129 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uzwo 12801*	Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
Theorem	uzwo2 12802*	Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃!𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
Theorem	nnwo 12803*	Well-ordering principle: any nonempty set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.)
⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	nnwof 12804*	Well-ordering principle: any nonempty set of positive integers has a least element. This version allows 𝑥 and 𝑦 to be present in 𝐴 as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	nnwos 12805*	Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦)))
Theorem	indstr 12806*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	eluznn0 12807	Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0)
Theorem	eluznn 12808	Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)
Theorem	eluz2b1 12809	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
Theorem	eluz2gt1 12810	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁)
Theorem	eluz2b2 12811	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
Theorem	eluz2b3 12812	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
Theorem	uz2m1nn 12813	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 12814	1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ ¬ 1 ∈ (ℤ≥‘2)
Theorem	elnn1uz2 12815	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2)))
Theorem	uz2mulcl 12816	Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2))
Theorem	indstr2 12817*	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 12818	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 12819	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 12820	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 12821	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 12822	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 12823*	The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦)
Theorem	eqreznegel 12824*	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴})
Theorem	supminf 12825*	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 12826*	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))
Theorem	zsupss 12827*	Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 11076.) (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	suprzcl2 12828*	The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 12545 avoids ax-pre-sup 11076.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	suprzub 12829*	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 12830*	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 12831	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 12832	Alternate proof of nn0ge2m1nn 12443: 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 12730, 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 12443. (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 12833*	Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 12802 allows the lower bound 𝐵 to be any real number. See also nnwo 12803 and nnwos 12805. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.)
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	zmin 12834*	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 12835*	There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))
Theorem	zbtwnre 12836*	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 12837*	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 12838	Extend class notation to include the class of rationals.
class ℚ
Definition	df-q 12839	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 12840 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
⊢ ℚ = ( / “ (ℤ × ℕ))
Theorem	elq 12840*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	qmulz 12841*	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 12842	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qre 12843	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
Theorem	zq 12844	An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
Theorem	qred 12845	A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	zssq 12846	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
⊢ ℤ ⊆ ℚ
Theorem	nn0ssq 12847	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ0 ⊆ ℚ
Theorem	nnssq 12848	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ ⊆ ℚ
Theorem	qssre 12849	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
⊢ ℚ ⊆ ℝ
Theorem	qsscn 12850	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℚ ⊆ ℂ
Theorem	qex 12851	The set of rational numbers exists. See also qexALT 12854. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℚ ∈ V
Theorem	nnq 12852	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ)
Theorem	qcn 12853	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
Theorem	qexALT 12854	Alternate proof of qex 12851. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℚ ∈ V
Theorem	qaddcl 12855	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)
Theorem	qnegcl 12856	Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ)
Theorem	qmulcl 12857	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ)
Theorem	qsubcl 12858	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ)
Theorem	qreccl 12859	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ)
Theorem	qdivcl 12860	Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qrevaddcl 12861	Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ))
Theorem	nnrecq 12862	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ)
Theorem	irradd 12863	The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	irrmul 12864	The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	elpq 12865*	A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	elpqb 12866*	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 12867*	Lemma for rpnnen1 12873. (Contributed by Mario Carneiro, 12-May-2013.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(𝑇, ℝ, < ) ∈ ℤ)
Theorem	rpnnen1lem1 12868*	Lemma for rpnnen1 12873. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑m ℕ))
Theorem	rpnnen1lem3 12869*	Lemma for rpnnen1 12873. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)
Theorem	rpnnen1lem4 12870*	Lemma for rpnnen1 12873. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ)
Theorem	rpnnen1lem5 12871*	Lemma for rpnnen1 12873. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥)
Theorem	rpnnen1lem6 12872*	Lemma for rpnnen1 12873. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ ℝ ≼ (ℚ ↑m ℕ)
Theorem	rpnnen1 12873	One half of rpnnen 16128, 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 12872) 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 12123 and qex 12851, or nnexALT 12119 and qexALT 12854. 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 12874	Alternate proof of reex 11089. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℝ ∈ V
Theorem	cnref1o 12875*	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 11004), 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 12876	The set of complex numbers exists. This theorem shows that ax-cnex 11054 is redundant if we assume ax-rep 5215. See also ax-cnex 11054. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	xrex 12877	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
⊢ ℝ* ∈ V
Theorem	mpoaddex 12878*	The addition operation is a set. Version of addex 12879 using maps-to notation , which does not require ax-addf 11077. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) ∈ V
Theorem	addex 12879	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ + ∈ V
Theorem	mpomulex 12880*	The multiplication operation is a set. Version of mulex 12881 using maps-to notation , which does not require ax-mulf 11078. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ V
Theorem	mulex 12881	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 12882	Extend class notation to include the class of positive reals.
class ℝ+
Definition	df-rp 12883	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
Theorem	elrp 12884	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	elrpii 12885	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ∈ ℝ+
Theorem	1rp 12886	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ 1 ∈ ℝ+
Theorem	2rp 12887	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ 2 ∈ ℝ+
Theorem	3rp 12888	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 3 ∈ ℝ+
Theorem	5rp 12889	5 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 5 ∈ ℝ+
Theorem	rpssre 12890	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
⊢ ℝ+ ⊆ ℝ
Theorem	rpre 12891	A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
Theorem	rpxr 12892	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)
Theorem	rpcn 12893	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)
Theorem	nnrp 12894	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Theorem	rpgt0 12895	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
Theorem	rpge0 12896	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
Theorem	rpregt0 12897	A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	rprege0 12898	A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rpne0 12899	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
Theorem	rprene0 12900	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0))