P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnfldtop 24901	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	cnfldhaus 24902	The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Haus
Theorem	unicntop 24903	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 24904	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 24905	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 24906	The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ NrmRing
Theorem	remetdval 24907	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	remet 24908	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (Met‘ℝ)
Theorem	rexmet 24909	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ)
Theorem	bl2ioo 24910	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 24911	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 24912	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷))
Theorem	blssioo 24913	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 24914	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 24915	ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((cls‘𝐽)‘ℚ) = ℝ
Theorem	blcvx 24916	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 24917	The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.)
⊢ (topGen‘ran (,)) ∈ Haus
Theorem	tgqioo 24918	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 24919	The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 2ndω
Theorem	resubmet 24920	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 24921	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 24922	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 24923	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 24924	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 24925	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 24926	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = (ordTop‘ ≤ )    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	xrrest2 24927	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑋 = (ordTop‘ ≤ )    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴))
Theorem	xrsxmet 24928	The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ*)
Theorem	xrsdsre 24929	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 24930	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 24931	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 24932	The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ ℤ ∈ (Clsd‘𝐽)
Theorem	recld2 24933	The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ℝ ∈ (Clsd‘𝐽)
Theorem	zcld2 24934	The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ℤ ∈ (Clsd‘𝐽)
Theorem	zdis 24935	The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ
Theorem	sszcld 24936	Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽))
Theorem	reperflem 24937*	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 24938	The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐽 ↾t ℝ) ∈ Perf
Theorem	cnperf 24939	The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Perf
Theorem	iccntr 24940	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 24941*	Lemma for icccmp 24944. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵))
Theorem	icccmplem2 24942*	Lemma for icccmp 24944. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉)    &   ⊢ 𝐺 = sup(𝑆, ℝ, < )    &   ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑆)
Theorem	icccmplem3 24943*	Lemma for icccmp 24944. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑆)
Theorem	icccmp 24944	A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp)
Theorem	reconnlem1 24945	Lemma for reconn 24947. 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 24946*	Lemma for reconn 24947. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴))    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    &   ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )    ⇒   ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉))
Theorem	reconn 24947*	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 24948	Corollary of reconn 24947. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
⊢ (topGen‘ran (,)) ∈ Conn
Theorem	iccconn 24949	A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
Theorem	opnreen 24950	Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ)
Theorem	rectbntr0 24951	A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅)
Theorem	xrge0gsumle 24952	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 24953*	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 24954	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 24955	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 24956	The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 24957 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 24957	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 24958	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 24959	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 24960	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 24961*	Continuity of the metric function; analogue of cnmpt12f 23784 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 24962*	Continuity of the metric function; analogue of cnmpt22f 23793 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 24963	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 24964	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 24965	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 24966*	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 24967*	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 24968*	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 24969*	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 24970*	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 24971*	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 24972*	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 24973*	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 24974*	Lemma for metdscn 24975. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) +𝑒 -𝑒(𝐹‘𝐵)) < 𝑅)
Theorem	metdscn 24975*	The function 𝐹 which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	metdscn2 24976*	The function 𝐹 which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	metnrmlem1a 24977*	Lemma for metnrm 24981. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 < (𝐹‘𝐴) ∧ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ+))
Theorem	metnrmlem1 24978*	Lemma for metnrm 24981. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ≤ (𝐴𝐷𝐵))
Theorem	metnrmlem2 24979*	Lemma for metnrm 24981. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈))
Theorem	metnrmlem3 24980*	Lemma for metnrm 24981. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑇 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))
Theorem	metnrm 24981	A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013.) (Revised by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Nrm)
Theorem	metreg 24982	A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Reg)
Theorem	addcnlem 24983*	Lemma for addcn 24984, subcn 24985, and mulcn 24986. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ + :(ℂ × ℂ)⟶ℂ    &   ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎))    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	addcn 24984	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	subcn 24985	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	mulcn 24986	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) Usage of this theorem is discouraged because it depends on ax-mulf 11168. Use mpomulcn 24987 instead. (New usage is discouraged.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	mpomulcn 24987*	Complex number multiplication is a continuous function. Version of mulcn 24986 using maps-to notation, which does not require ax-mulf 11168. (Contributed by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	divcn 24988	Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) Avoid ax-mulf 11168. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t (ℂ ∖ {0}))    ⇒   ⊢ / ∈ ((𝐽 ×t 𝐾) Cn 𝐽)
Theorem	cnfldtgp 24989	The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ℂfld ∈ TopGrp
Theorem	fsumcn 24990*	A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for 𝐵 normally contains free variables 𝑘 and 𝑥 to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	fsum2cn 24991*	Version of fsumcn 24990 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾))
Theorem	expcn 24992*	The power function on complex numbers, for fixed exponent 𝑁, is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) Avoid ax-mulf 11168. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (𝐽 Cn 𝐽))
Theorem	divccn 24993*	Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) Avoid ax-mulf 11168. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ∈ (𝐽 Cn 𝐽))
Theorem	sqcn 24994*	The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (𝐽 Cn 𝐽)
12.4.11  Topological definitions using the reals
Syntax	cii 24995	Extend class notation with the unit interval.
class II
Syntax	ccncf 24996	Extend class notation to include the operation which returns a class of continuous complex functions.
class –cn→
Definition	df-ii 24997	Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
Definition	df-cncf 24998*	Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})
Theorem	iitopon 24999	The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ II ∈ (TopOn‘(0[,]1))
Theorem	iitop 25000	The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ II ∈ Top