P. 122 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12101-12200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lereci 12101	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴)))
Theorem	lt2msqi 12102	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵)))
Theorem	le2msqi 12103	The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
Theorem	msq11i 12104	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divgt0i2i 12105	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐵    ⇒   ⊢ (0 < 𝐴 → 0 < (𝐴 / 𝐵))
Theorem	ltrecii 12106	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))
Theorem	divgt0ii 12107	The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 / 𝐵)
Theorem	ltmul1i 12108	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)))
Theorem	ltdiv1i 12109	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	ltmuldivi 12110	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmul2i 12111	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵)))
Theorem	lemul1i 12112	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))
Theorem	lemul2i 12113	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	ltdiv23i 12114	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((0 < 𝐵 ∧ 0 < 𝐶) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	ledivp1i 12115	"Less than or equal to" and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · 𝐶) ≤ 𝐵)
Theorem	ltdivp1i 12116	Less-than and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 < (𝐵 / (𝐶 + 1))) → (𝐴 · 𝐶) < 𝐵)
Theorem	ltdiv23ii 12117	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐵    &   ⊢ 0 < 𝐶    ⇒   ⊢ ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)
Theorem	ltmul1ii 12118	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))
Theorem	ltdiv1ii 12119	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))
Theorem	ltp1d 12120	A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐴 + 1))
Theorem	lep1d 12121	A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1))
Theorem	ltm1d 12122	A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 1) < 𝐴)
Theorem	lem1d 12123	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 1) ≤ 𝐴)
Theorem	recgt0d 12124	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 0 < (1 / 𝐴))
Theorem	divgt0d 12125	The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 / 𝐵))
Theorem	mulgt1d 12126	The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	lemulge11d 12127	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 · 𝐵))
Theorem	lemulge12d 12128	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐵 · 𝐴))
Theorem	lemul1ad 12129	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))
Theorem	lemul2ad 12130	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
Theorem	ltmul12ad 12131	Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐷))
Theorem	lemul12ad 12132	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))
Theorem	lemul12bd 12133	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐷)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))
5.3.8  Completeness Axiom and Suprema
Theorem	fimaxre 12134*	A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
Theorem	fimaxre2 12135*	A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
Theorem	fimaxre3 12136*	A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑦 ∈ 𝐴 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝐵 ≤ 𝑥)
Theorem	fiminre 12137*	A nonempty finite set of real numbers has a minimum. Analogous to fimaxre 12134. (Contributed by AV, 9-Aug-2020.) (Proof shortened by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	fiminre2 12138*	A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	negfi 12139*	The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin)
Theorem	lbreu 12140*	If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ∃!𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)
Theorem	lbcl 12141*	If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆)
Theorem	lble 12142*	If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ≤ 𝐴)
Theorem	lbinf 12143*	If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → inf(𝑆, ℝ, < ) = (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦))
Theorem	lbinfcl 12144*	If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → inf(𝑆, ℝ, < ) ∈ 𝑆)
Theorem	lbinfle 12145*	If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝐴)
Theorem	sup2 12146*	A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sup3 12147*	A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	infm3lem 12148*	Lemma for infm3 12149. (Contributed by NM, 14-Jun-2005.)
⊢ (𝑥 ∈ ℝ → ∃𝑦 ∈ ℝ 𝑥 = -𝑦)
Theorem	infm3 12149*	The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 12147.) (Contributed by NM, 14-Jun-2005.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	suprcl 12150*	Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	suprub 12151*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprubd 12152*	Natural deduction form of suprubd 12152. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprcld 12153*	Natural deduction form of suprcl 12150. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	suprlub 12154*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧))
Theorem	suprnub 12155*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧))
Theorem	suprleub 12156*	The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵))
Theorem	supaddc 12157*	The supremum function distributes over addition in a sense similar to that in supmul1 12159. (Contributed by Brendan Leahy, 25-Sep-2017.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵)}    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < ))
Theorem	supadd 12158*	The supremum function distributes over addition in a sense similar to that in supmul 12162. (Contributed by Brendan Leahy, 26-Sep-2017.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)    &   ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏)}    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Theorem	supmul1 12159*	The supremum function distributes over multiplication, in the sense that 𝐴 · (sup𝐵) = sup(𝐴 · 𝐵), where 𝐴 · 𝐵 is shorthand for {𝐴 · 𝑏 ∣ 𝑏 ∈ 𝐵} and is defined as 𝐶 below. This is the simple version, with only one set argument; see supmul 12162 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐵 𝑧 = (𝐴 · 𝑣)}    &   ⊢ (𝜑 ↔ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → (𝐴 · sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Theorem	supmullem1 12160*	Lemma for supmul 12162. (Contributed by Mario Carneiro, 5-Jul-2013.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)}    &   ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) · sup(𝐵, ℝ, < )))
Theorem	supmullem2 12161*	Lemma for supmul 12162. (Contributed by Mario Carneiro, 5-Jul-2013.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)}    &   ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → (𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥))
Theorem	supmul 12162*	The supremum function distributes over multiplication, in the sense that (sup𝐴) · (sup𝐵) = sup(𝐴 · 𝐵), where 𝐴 · 𝐵 is shorthand for {𝑎 · 𝑏 ∣ 𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵} and is defined as 𝐶 below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp 10944). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)}    &   ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) · sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Theorem	sup3ii 12163*	A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))
Theorem	suprclii 12164*	Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ sup(𝐴, ℝ, < ) ∈ ℝ
Theorem	suprubii 12165*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprlubii 12166*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ ℝ → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧))
Theorem	suprnubii 12167*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ ℝ → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧))
Theorem	suprleubii 12168*	The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ ℝ → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵))
Theorem	riotaneg 12169*	The negative of the unique real such that 𝜑. (Contributed by NM, 13-Jun-2005.)
⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ ℝ 𝜑 → (℩𝑥 ∈ ℝ 𝜑) = -(℩𝑦 ∈ ℝ 𝜓))
Theorem	negiso 12170	Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ -𝑥)    ⇒   ⊢ (𝐹 Isom < , ◡ < (ℝ, ℝ) ∧ ◡𝐹 = 𝐹)
Theorem	dfinfre 12171*	The infimum of a set of reals 𝐴. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ (𝐴 ⊆ ℝ → inf(𝐴, ℝ, < ) = ∪ {𝑥 ∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))})
Theorem	infrecl 12172*	Closure of infimum of a nonempty bounded set of reals. (Contributed by NM, 8-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ)
Theorem	infrenegsup 12173*	The infimum of a set of reals 𝐴 is the negative of the supremum of the negatives of its elements. The antecedent ensures that 𝐴 is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))
Theorem	infregelb 12174*	Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013.) (Revised by AV, 4-Sep-2020.) (Proof modification is discouraged.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧))
Theorem	infrelb 12175*	If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝐵 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴)
Theorem	infrefilb 12176	The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴)
Theorem	supfirege 12177	The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = sup(𝐵, ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝑆)
5.3.9  Imaginary and complex number properties
Theorem	neg1cn 12178	-1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 12179	-1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 12180	-1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 12181	-1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	negneg1e1 12182	--1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	inelr 12183	The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.)
⊢ ¬ i ∈ ℝ
Theorem	rimul 12184	A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → 𝐴 = 0)
Theorem	cru 12185	The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) = (𝐶 + (i · 𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	crne0 12186	The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0))
Theorem	creur 12187*	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	creui 12188*	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑦 ∈ ℝ ∃𝑥 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	cju 12189*	The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))
5.3.10  Function operation analogue theorems
Theorem	ofsubeq0 12190	Function analogue of subeq0 11455. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → ((𝐹 ∘f − 𝐺) = (𝐴 × {0}) ↔ 𝐹 = 𝐺))
Theorem	ofnegsub 12191	Function analogue of negsub 11477. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → (𝐹 ∘f + ((𝐴 × {-1}) ∘f · 𝐺)) = (𝐹 ∘f − 𝐺))
Theorem	ofsubge0 12192	Function analogue of subge0 11698. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ) → ((𝐴 × {0}) ∘r ≤ (𝐹 ∘f − 𝐺) ↔ 𝐺 ∘r ≤ 𝐹))
5.4  Integer sets
5.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 12193	Extend class notation to include the class of positive integers.
class ℕ
Definition	df-nn 12194	Define the set of positive integers. Some authors, especially in analysis books, call these the natural numbers, whereas other authors choose to include 0 in their definition of natural numbers. Note that ℕ is a subset of complex numbers (nnsscn 12198), in contrast to the more elementary ordinal natural numbers ω, df-om 7846). See nnind 12211 for the principle of mathematical induction. See df-n0 12450 for the set of nonnegative integers ℕ0. See dfn2 12462 for ℕ defined in terms of ℕ0. This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9601 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 12207 (or its slight variant dfnn2 12206). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
Theorem	nnexALT 12195	Alternate proof of nnex 12199, more direct, that makes use of ax-rep 5237. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℕ ∈ V
Theorem	peano5nni 12196*	Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ℕ ⊆ 𝐴)
Theorem	nnssre 12197	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 12198	The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 12197 and ax-resscn 11132 at the cost of using more axioms. (Contributed by NM, 2-Aug-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ ℕ ⊆ ℂ
Theorem	nnex 12199	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℕ ∈ V
Theorem	nnre 12200	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)