P. 130 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12901-13000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uzwo2 12901*	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 12902*	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 12903*	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 12904*	Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦)))
Theorem	indstr 12905*	Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝑥 ∈ ℕ → 𝜑)
Theorem	eluznn0 12906	Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0)
Theorem	eluznn 12907	Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)
Theorem	eluz2b1 12908	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
Theorem	eluz2gt1 12909	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁)
Theorem	eluz2b2 12910	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
Theorem	eluz2b3 12911	Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.)
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
Theorem	uz2m1nn 12912	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 12913	1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.)
⊢ ¬ 1 ∈ (ℤ≥‘2)
Theorem	elnn1uz2 12914	A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2)))
Theorem	uz2mulcl 12915	Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2))
Theorem	indstr2 12916*	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 12917	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 12918	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 12919	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 12920	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 12921	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 12922*	The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦)
Theorem	eqreznegel 12923*	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴})
Theorem	supminf 12924*	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 12925*	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))
Theorem	zsupss 12926*	Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 11191.) (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	suprzcl2 12927*	The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 12647 avoids ax-pre-sup 11191.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	suprzub 12928*	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 12929*	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 12930	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 12931	Alternate proof of nn0ge2m1nn 12546: 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 12833, 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 12546. (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 12932*	Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 12901 allows the lower bound 𝐵 to be any real number. See also nnwo 12902 and nnwos 12904. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.)
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	zmin 12933*	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 12934*	There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))
Theorem	zbtwnre 12935*	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 12936*	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 12937	Extend class notation to include the class of rationals.
class ℚ
Definition	df-q 12938	Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 12939 for the relation "is rational". (Contributed by NM, 8-Jan-2002.)
⊢ ℚ = ( / “ (ℤ × ℕ))
Theorem	elq 12939*	Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	qmulz 12940*	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 12941	The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qre 12942	A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)
Theorem	zq 12943	An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
Theorem	qred 12944	A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	zssq 12945	The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
⊢ ℤ ⊆ ℚ
Theorem	nn0ssq 12946	The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ0 ⊆ ℚ
Theorem	nnssq 12947	The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
⊢ ℕ ⊆ ℚ
Theorem	qssre 12948	The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
⊢ ℚ ⊆ ℝ
Theorem	qsscn 12949	The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℚ ⊆ ℂ
Theorem	qex 12950	The set of rational numbers exists. See also qexALT 12953. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℚ ∈ V
Theorem	nnq 12951	A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ)
Theorem	qcn 12952	A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
Theorem	qexALT 12953	Alternate proof of qex 12950. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℚ ∈ V
Theorem	qaddcl 12954	Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)
Theorem	qnegcl 12955	Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ)
Theorem	qmulcl 12956	Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ)
Theorem	qsubcl 12957	Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ)
Theorem	qreccl 12958	Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ)
Theorem	qdivcl 12959	Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ)
Theorem	qrevaddcl 12960	Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ))
Theorem	nnrecq 12961	The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ)
Theorem	irradd 12962	The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	irrmul 12963	The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ))
Theorem	elpq 12964*	A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
Theorem	elpqb 12965*	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 12966*	Lemma for rpnnen1 12972. (Contributed by Mario Carneiro, 12-May-2013.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    ⇒   ⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(𝑇, ℝ, < ) ∈ ℤ)
Theorem	rpnnen1lem1 12967*	Lemma for rpnnen1 12972. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑m ℕ))
Theorem	rpnnen1lem3 12968*	Lemma for rpnnen1 12972. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)
Theorem	rpnnen1lem4 12969*	Lemma for rpnnen1 12972. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ)
Theorem	rpnnen1lem5 12970*	Lemma for rpnnen1 12972. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥)
Theorem	rpnnen1lem6 12971*	Lemma for rpnnen1 12972. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.)
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥}    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)))    &   ⊢ ℕ ∈ V    &   ⊢ ℚ ∈ V    ⇒   ⊢ ℝ ≼ (ℚ ↑m ℕ)
Theorem	rpnnen1 12972	One half of rpnnen 16175, 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 12971) 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 12223 and qex 12950, or nnexALT 12219 and qexALT 12953. 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 12973	Alternate proof of reex 11204. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℝ ∈ V
Theorem	cnref1o 12974*	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 11119), 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 12975	The set of complex numbers exists. This theorem shows that ax-cnex 11169 is redundant if we assume ax-rep 5286. See also ax-cnex 11169. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	xrex 12976	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
⊢ ℝ* ∈ V
Theorem	addex 12977	The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ + ∈ V
Theorem	mulex 12978	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 12979	Extend class notation to include the class of positive reals.
class ℝ+
Definition	df-rp 12980	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
Theorem	elrp 12981	Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	elrpii 12982	Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ∈ ℝ+
Theorem	1rp 12983	1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ 1 ∈ ℝ+
Theorem	2rp 12984	2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ 2 ∈ ℝ+
Theorem	3rp 12985	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 3 ∈ ℝ+
Theorem	rpssre 12986	The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
⊢ ℝ+ ⊆ ℝ
Theorem	rpre 12987	A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
Theorem	rpxr 12988	A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)
Theorem	rpcn 12989	A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)
Theorem	nnrp 12990	A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Theorem	rpgt0 12991	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
Theorem	rpge0 12992	A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
Theorem	rpregt0 12993	A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	rprege0 12994	A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rpne0 12995	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
Theorem	rprene0 12996	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0))
Theorem	rpcnne0 12997	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
Theorem	rpcndif0 12998	A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ {0}))
Theorem	ralrp 12999	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑))
Theorem	rexrp 13000	Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑))