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	nghmrcl2 24901	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp)
Theorem	nghmghm 24902	A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	nmo0 24903	The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0)
Theorem	nmoeq0 24904	The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) = 0 ↔ 𝐹 = (𝑉 × { 0 })))
Theorem	nmoco 24905	An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑈)    &   ⊢ 𝐿 = (𝑇 normOp 𝑈)    &   ⊢ 𝑀 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺)))
Theorem	nghmco 24906	The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈))
Theorem	nmotri 24907	Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘f + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺)))
Theorem	nghmplusg 24908	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NGHom 𝑇))
Theorem	0nghm 24909	The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇))
Theorem	nmoid 24910	The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑆)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉) → (𝑁‘( I ↾ 𝑉)) = 1)
Theorem	idnghm 24911	The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆))
Theorem	nmods 24912	Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐶 = (dist‘𝑆)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐹‘𝐴)𝐷(𝐹‘𝐵)) ≤ ((𝑁‘𝐹) · (𝐴𝐶𝐵)))
Theorem	nghmcn 24913	A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝐾 = (TopOpen‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	isnmhm 24914	A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
Theorem	nmhmrcl1 24915	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod)
Theorem	nmhmrcl2 24916	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod)
Theorem	nmhmlmhm 24917	A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇))
Theorem	nmhmnghm 24918	A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nmhmghm 24919	A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	isnmhm2 24920	A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ))
Theorem	nmhmcl 24921	A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	idnmhm 24922	The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆))
Theorem	0nmhm 24923	The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐹 = (Scalar‘𝑆)    &   ⊢ 𝐺 = (Scalar‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺) → (𝑉 × { 0 }) ∈ (𝑆 NMHom 𝑇))
Theorem	nmhmco 24924	The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈))
Theorem	nmhmplusg 24925	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 24926	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 24927	The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases
Theorem	retopbas 24928	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 24929	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
⊢ (topGen‘ran (,)) ∈ Top
Theorem	uniretop 24930	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
⊢ ℝ = ∪ (topGen‘ran (,))
Theorem	retopon 24931	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
Theorem	retps 24932	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐾 = {⟨(Base‘ndx), ℝ⟩, ⟨(TopSet‘ndx), (topGen‘ran (,))⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	iooretop 24933	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.)
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
Theorem	icccld 24934	Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	icopnfcld 24935	Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	iocmnfcld 24936	Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	qdensere 24937	ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.)
⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ
Theorem	cnmetdval 24938	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 24939	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 24940	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
Theorem	cnbl0 24941	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅))
Theorem	cnblcld 24942*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅})
Theorem	cnfldms 24943	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ MetSp
Theorem	cnfldxms 24944	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ ∞MetSp
Theorem	cnfldtps 24945	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ TopSp
Theorem	cnfldnm 24946	The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ abs = (norm‘ℂfld)
Theorem	cnngp 24947	The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ℂfld ∈ NrmGrp
Theorem	cnnrg 24948	The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ℂfld ∈ NrmRing
Theorem	cnfldtopn 24949	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
Theorem	cnfldtopon 24950	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ (TopOn‘ℂ)
Theorem	cnfldtop 24951	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	cnfldhaus 24952	The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Haus
Theorem	unicntop 24953	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 24954	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 24955	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 24956	The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ NrmRing
Theorem	remetdval 24957	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	remet 24958	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (Met‘ℝ)
Theorem	rexmet 24959	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ)
Theorem	bl2ioo 24960	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 24961	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 24962	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷))
Theorem	blssioo 24963	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 24964	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 24965	ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((cls‘𝐽)‘ℚ) = ℝ
Theorem	blcvx 24966	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 24967	The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.)
⊢ (topGen‘ran (,)) ∈ Haus
Theorem	tgqioo 24968	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 24969	The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 2ndω
Theorem	resubmet 24970	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 24971	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 24972	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 24973	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 24974	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 24975	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 24976	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = (ordTop‘ ≤ )    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	xrrest2 24977	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑋 = (ordTop‘ ≤ )    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴))
Theorem	xrsxmet 24978	The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ*)
Theorem	xrsdsre 24979	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 24980	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 24981	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 24982	The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ ℤ ∈ (Clsd‘𝐽)
Theorem	recld2 24983	The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ℝ ∈ (Clsd‘𝐽)
Theorem	zcld2 24984	The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ℤ ∈ (Clsd‘𝐽)
Theorem	zdis 24985	The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ
Theorem	sszcld 24986	Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽))
Theorem	reperflem 24987*	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 24988	The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐽 ↾t ℝ) ∈ Perf
Theorem	cnperf 24989	The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Perf
Theorem	iccntr 24990	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 24991*	Lemma for icccmp 24994. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵))
Theorem	icccmplem2 24992*	Lemma for icccmp 24994. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉)    &   ⊢ 𝐺 = sup(𝑆, ℝ, < )    &   ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑆)
Theorem	icccmplem3 24993*	Lemma for icccmp 24994. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑆)
Theorem	icccmp 24994	A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp)
Theorem	reconnlem1 24995	Lemma for reconn 24997. 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 24996*	Lemma for reconn 24997. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,)))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴))    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    &   ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )    ⇒   ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉))
Theorem	reconn 24997*	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 24998	Corollary of reconn 24997. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
⊢ (topGen‘ran (,)) ∈ Conn
Theorem	iccconn 24999	A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
Theorem	opnreen 25000	Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ)