P. 248 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24701-24800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nmhmplusg 24701	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇))
12.4.10  Topology on the reals
Theorem	qtopbaslem 24702	The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝑆 ⊆ ℝ*    ⇒   ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases
Theorem	qtopbas 24703	The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases
Theorem	retopbas 24704	A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
⊢ ran (,) ∈ TopBases
Theorem	retop 24705	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
⊢ (topGen‘ran (,)) ∈ Top
Theorem	uniretop 24706	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
⊢ ℝ = ∪ (topGen‘ran (,))
Theorem	retopon 24707	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
Theorem	retps 24708	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐾 = {⟨(Base‘ndx), ℝ⟩, ⟨(TopSet‘ndx), (topGen‘ran (,))⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	iooretop 24709	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.)
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
Theorem	icccld 24710	Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	icopnfcld 24711	Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	iocmnfcld 24712	Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	qdensere 24713	ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.)
⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ
Theorem	cnmetdval 24714	Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	cnmet 24715	The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)
⊢ (abs ∘ − ) ∈ (Met‘ℂ)
Theorem	cnxmet 24716	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
Theorem	cnbl0 24717	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅))
Theorem	cnblcld 24718*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅})
Theorem	cnfldms 24719	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ MetSp
Theorem	cnfldxms 24720	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ ∞MetSp
Theorem	cnfldtps 24721	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ TopSp
Theorem	cnfldnm 24722	The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ abs = (norm‘ℂfld)
Theorem	cnngp 24723	The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ℂfld ∈ NrmGrp
Theorem	cnnrg 24724	The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ℂfld ∈ NrmRing
Theorem	cnfldtopn 24725	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
Theorem	cnfldtopon 24726	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ (TopOn‘ℂ)
Theorem	cnfldtop 24727	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	cnfldhaus 24728	The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Haus
Theorem	unicntop 24729	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ℂ = ∪ (TopOpen‘ℂfld)
Theorem	cnopn 24730	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ℂ ∈ (TopOpen‘ℂfld)
Theorem	cnn0opn 24731	The set of nonzero complex numbers is open with respect to the standard topology on complex numbers. (Contributed by SN, 7-Oct-2025.)
⊢ (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld)
Theorem	zringnrg 24732	The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ NrmRing
Theorem	remetdval 24733	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	remet 24734	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (Met‘ℝ)
Theorem	rexmet 24735	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ)
Theorem	bl2ioo 24736	A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(ball‘𝐷)𝐵) = ((𝐴 − 𝐵)(,)(𝐴 + 𝐵)))
Theorem	ioo2bl 24737	An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) = (((𝐴 + 𝐵) / 2)(ball‘𝐷)((𝐵 − 𝐴) / 2)))
Theorem	ioo2blex 24738	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷))
Theorem	blssioo 24739	The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ran (ball‘𝐷) ⊆ ran (,)
Theorem	tgioo 24740	The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (topGen‘ran (,)) = 𝐽
Theorem	qdensere2 24741	ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((cls‘𝐽)‘ℚ) = ℝ
Theorem	blcvx 24742	An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)    ⇒   ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)
Theorem	rehaus 24743	The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.)
⊢ (topGen‘ran (,)) ∈ Haus
Theorem	tgqioo 24744	The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝑄 = (topGen‘((,) “ (ℚ × ℚ)))    ⇒   ⊢ (topGen‘ran (,)) = 𝑄
Theorem	re2ndc 24745	The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 2ndω
Theorem	resubmet 24746	The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
⊢ 𝑅 = (topGen‘ran (,))    &   ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴)))    ⇒   ⊢ (𝐴 ⊆ ℝ → 𝐽 = (𝑅 ↾t 𝐴))
Theorem	tgioo2 24747	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (topGen‘ran (,)) = (𝐽 ↾t ℝ)
Theorem	rerest 24748	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	tgioo4 24749	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
Theorem	tgioo3 24750	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Thierry Arnoux, 3-Jul-2019.)
⊢ 𝐽 = (TopOpen‘ℝfld)    ⇒   ⊢ (topGen‘ran (,)) = 𝐽
Theorem	xrtgioo 24751	The topology on the extended reals coincides with the standard topology on the reals, when restricted to ℝ. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t ℝ)    ⇒   ⊢ (topGen‘ran (,)) = 𝐽
Theorem	xrrest 24752	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = (ordTop‘ ≤ )    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	xrrest2 24753	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑋 = (ordTop‘ ≤ )    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴))
Theorem	xrsxmet 24754	The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ*)
Theorem	xrsdsre 24755	The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
Theorem	xrsblre 24756	Any ball of the metric of the extended reals centered on an element of ℝ is entirely contained in ℝ. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ ℝ)
Theorem	xrsmopn 24757	The metric on the extended reals generates a topology, but this does not match the order topology on ℝ*; for example {+∞} is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (ordTop‘ ≤ ) ⊆ 𝐽
Theorem	zcld 24758	The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ ℤ ∈ (Clsd‘𝐽)
Theorem	recld2 24759	The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ℝ ∈ (Clsd‘𝐽)
Theorem	zcld2 24760	The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ℤ ∈ (Clsd‘𝐽)
Theorem	zdis 24761	The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ
Theorem	sszcld 24762	Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽))
Theorem	reperflem 24763*	A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ 𝑆)    &   ⊢ 𝑆 ⊆ ℂ    ⇒   ⊢ (𝐽 ↾t 𝑆) ∈ Perf
Theorem	reperf 24764	The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐽 ↾t ℝ) ∈ Perf
Theorem	cnperf 24765	The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Perf
Theorem	iccntr 24766	The interior of a closed interval in the standard topology on ℝ is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
Theorem	icccmplem1 24767*	Lemma for icccmp 24770. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵))
Theorem	icccmplem2 24768*	Lemma for icccmp 24770. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉)    &   ⊢ 𝐺 = sup(𝑆, ℝ, < )    &   ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑆)
Theorem	icccmplem3 24769*	Lemma for icccmp 24770. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑆)
Theorem	icccmp 24770	A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp)
Theorem	reconnlem1 24771	Lemma for reconn 24773. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
⊢ (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴)
Theorem	reconnlem2 24772*	Lemma for reconn 24773. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴))    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    &   ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )    ⇒   ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉))
Theorem	reconn 24773*	A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ⊆ ℝ → (((topGen‘ran (,)) ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴))
Theorem	retopconn 24774	Corollary of reconn 24773. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
⊢ (topGen‘ran (,)) ∈ Conn
Theorem	iccconn 24775	A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
Theorem	opnreen 24776	Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ)
Theorem	rectbntr0 24777	A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅)
Theorem	xrge0gsumle 24778	A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ (𝒫 𝐴 ∩ Fin))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ≤ (𝐺 Σg (𝐹 ↾ 𝐵)))
Theorem	xrge0tsms 24779*	Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Proof shortened by AV, 26-Jul-2019.)
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))    &   ⊢ 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < )    ⇒   ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆})
Theorem	xrge0tsms2 24780	Any finite or infinite sum in the nonnegative extended reals is convergent. This is a rather unique property of the set [0, +∞]; a similar theorem is not true for ℝ* or ℝ or [0, +∞). It is true for ℕ0 ∪ {+∞}, however, or more generally any additive submonoid of [0, +∞) with +∞ adjoined. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,]+∞)) → (𝐺 tsums 𝐹) ≈ 1o)
Theorem	metdcnlem 24781	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐴𝐷𝑌) < (𝑅 / 2))    &   ⊢ (𝜑 → (𝐵𝐷𝑍) < (𝑅 / 2))    ⇒   ⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) < 𝑅)
Theorem	xmetdcn2 24782	The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 24783 we use the metric topology instead of the order topology on ℝ*, which makes the theorem a bit stronger. Since +∞ is an isolated point in the metric topology, this is saying that for any points 𝐴, 𝐵 which are an infinite distance apart, there is a product neighborhood around ⟨𝐴, 𝐵⟩ such that 𝑑(𝑎, 𝑏) = +∞ for any 𝑎 near 𝐴 and 𝑏 near 𝐵, i.e., the distance function is locally constant +∞. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
Theorem	xmetdcn 24783	The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (ordTop‘ ≤ )    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
Theorem	metdcn2 24784	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
Theorem	metdcn 24785	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
Theorem	msdcn 24786	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    &   ⊢ 𝐽 = (TopOpen‘𝑀)    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
Theorem	cnmpt1ds 24787*	Continuity of the metric function; analogue of cnmpt12f 23610 which cannot be used directly because 𝐷 is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑅 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐺 ∈ MetSp)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐷𝐵)) ∈ (𝐾 Cn 𝑅))
Theorem	cnmpt2ds 24788*	Continuity of the metric function; analogue of cnmpt22f 23619 which cannot be used directly because 𝐷 is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑅 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐺 ∈ MetSp)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴𝐷𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝑅))
Theorem	nmcn 24789	The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	ngnmcncn 24790	The norm of a normed group is a continuous function to ℂ. (Contributed by NM, 12-Aug-2007.) (Revised by AV, 17-Oct-2021.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	abscn 24791	The absolute value function on complex numbers is continuous. (Contributed by NM, 22-Aug-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ abs ∈ (𝐽 Cn 𝐾)
Theorem	metdsval 24792*	Value of the "distance to a set" function. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = inf(ran (𝑦 ∈ 𝑆 ↦ (𝐴𝐷𝑦)), ℝ*, < ))
Theorem	metdsf 24793*	The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞))
Theorem	metdsge 24794*	The distance from the point 𝐴 to the set 𝑆 is greater than 𝑅 iff the 𝑅-ball around 𝐴 misses 𝑆. (Contributed by Mario Carneiro, 4-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝑅 ∈ ℝ*) → (𝑅 ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑅)) = ∅))
Theorem	metds0 24795*	If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) = 0)
Theorem	metdstri 24796*	A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol 𝑑 denotes the point-point and point-set distance functions, this theorem would be written 𝑑(𝑎, 𝑆) ≤ 𝑑(𝑎, 𝑏) + 𝑑(𝑏, 𝑆). (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))
Theorem	metdsle 24797*	The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ≤ (𝐴𝐷𝐵))
Theorem	metdsre 24798*	The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹:𝑋⟶ℝ)
Theorem	metdseq0 24799*	The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))
Theorem	metdscnlem 24800*	Lemma for metdscn 24801. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) +𝑒 -𝑒(𝐹‘𝐵)) < 𝑅)