P. 156 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15501-15600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	retop 15501	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
⊢ (topGen‘ran (,)) ∈ Top
Theorem	uniretop 15502	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
⊢ ℝ = ∪ (topGen‘ran (,))
Theorem	retopon 15503	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
Theorem	retps 15504	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐾 = {⟨(Base‘ndx), ℝ⟩, ⟨(TopSet‘ndx), (topGen‘ran (,))⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	iooretopg 15505	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
Theorem	cnmetdval 15506	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 15507	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 15508	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
Theorem	cntoptopon 15509	The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ 𝐽 ∈ (TopOn‘ℂ)
Theorem	cntoptop 15510	The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ 𝐽 ∈ Top
Theorem	cnbl0 15511	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅))
Theorem	cnblcld 15512*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅})
Theorem	cnfldms 15513	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ MetSp
Theorem	cnfldxms 15514	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ ∞MetSp
Theorem	cnfldtps 15515	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ TopSp
Theorem	cnfldtopn 15516	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
Theorem	cnfldtopon 15517	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ (TopOn‘ℂ)
Theorem	cnfldtop 15518	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	unicntopcntop 15519	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
⊢ ℂ = ∪ (MetOpen‘(abs ∘ − ))
Theorem	unicntop 15520	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	cnopncntop 15521	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
⊢ ℂ ∈ (MetOpen‘(abs ∘ − ))
Theorem	cnopn 15522	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	reopnap 15523*	The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.)
⊢ (𝐴 ∈ ℝ → {𝑤 ∈ ℝ ∣ 𝑤 # 𝐴} ∈ (topGen‘ran (,)))
Theorem	remetdval 15524	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	remet 15525	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (Met‘ℝ)
Theorem	rexmet 15526	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ)
Theorem	bl2ioo 15527	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 15528	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 15529	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷))
Theorem	blssioo 15530	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 15531	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	tgqioo 15532	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	resubmet 15533	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	tgioo2cntop 15534	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (topGen‘ran (,)) = (𝐽 ↾t ℝ)
Theorem	rerestcntop 15535	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	tgioo2 15536	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 15537	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	addcncntoplem 15538*	Lemma for addcncntop 15539, subcncntop 15540, and mulcncntop 15541. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    &   ⊢ + :(ℂ × ℂ)⟶ℂ    &   ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎))    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	addcncntop 15539	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.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	subcncntop 15540	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.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	mulcncntop 15541	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.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	divcnap 15542*	Complex number division is a continuous function, when the second argument is apart from zero. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐾 = (𝐽 ↾t {𝑥 ∈ ℂ ∣ 𝑥 # 0})    ⇒   ⊢ (𝑦 ∈ ℂ, 𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (𝑦 / 𝑧)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)
Theorem	mpomulcn 15543*	Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	fsumcncntop 15544*	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.)
⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	fsumcn 15545*	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	expcn 15546*	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 8266. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (𝐽 Cn 𝐽))
9.2.7  Topological definitions using the reals
Syntax	ccncf 15547	Extend class notation to include the operation which returns a class of continuous complex functions.
class –cn→
Definition	df-cncf 15548*	Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑𝑚 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})
Theorem	cncfval 15549*	The value of the continuous complex function operation is the set of continuous functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)})
Theorem	elcncf 15550*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
Theorem	elcncf2 15551*	Version of elcncf 15550 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.)
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦))))
Theorem	cncfrss 15552	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
Theorem	cncfrss2 15553	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
Theorem	cncff 15554	A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)
Theorem	cncfi 15555*	Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝐶))) < 𝑅))
Theorem	elcncf1di 15556*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+))    &   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))    ⇒   ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)))
Theorem	elcncf1ii 15557*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ 𝐹:𝐴⟶𝐵    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+)    &   ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))
Theorem	rescncf 15558	A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐶 ⊆ 𝐴 → (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵)))
Theorem	cncfcdm 15559	Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ 𝐹:𝐴⟶𝐶))
Theorem	cncfss 15560	The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶))
Theorem	climcncf 15561	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐺:𝑍⟶𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷))
Theorem	abscncf 15562	Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ abs ∈ (ℂ–cn→ℝ)
Theorem	recncf 15563	Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℜ ∈ (ℂ–cn→ℝ)
Theorem	imcncf 15564	Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℑ ∈ (ℂ–cn→ℝ)
Theorem	cjcncf 15565	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ∗ ∈ (ℂ–cn→ℂ)
Theorem	mulc1cncf 15566*	Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	divccncfap 15567*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cncfco 15568	The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶))
Theorem	cncfmet 15569	Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ 𝐶 = ((abs ∘ − ) ↾ (𝐴 × 𝐴))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐽 Cn 𝐾))
Theorem	cncfcncntop 15570	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    &   ⊢ 𝐾 = (𝐽 ↾t 𝐴)    &   ⊢ 𝐿 = (𝐽 ↾t 𝐵)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿))
Theorem	cncfcn1cntop 15571	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ (ℂ–cn→ℂ) = (𝐽 Cn 𝐽)
Theorem	cncfcn1 15572	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (ℂ–cn→ℂ) = (𝐽 Cn 𝐽)
Theorem	cncfmptc 15573*	A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ ((𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→𝑇))
Theorem	cncfmptid 15574*	The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝑥) ∈ (𝑆–cn→𝑇))
Theorem	cncfmpt1f 15575*	Composition of continuous functions. –cn→ analogue of cnmpt11f 15261. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2fcntop 15576*	Composition of continuous functions. –cn→ analogue of cnmpt12f 15263. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ 𝐽 = (MetOpen‘(abs ∘ − ))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	addccncf 15577*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	idcncf 15578	The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 15574 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝑥)    ⇒   ⊢ 𝐹 ∈ (ℂ–cn→ℂ)
Theorem	sub1cncf 15579*	Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	sub2cncf 15580*	Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cdivcncfap 15581*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 / 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))
Theorem	negcncf 15582*	The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	negfcncf 15583*	The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝑥))    ⇒   ⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐺 ∈ (𝐴–cn→ℂ))
Theorem	mulcncflem 15584*	Lemma for mulcncf 15585. (Contributed by Jim Kingdon, 29-May-2023.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑆 → (abs‘(((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑢) − ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑉))) < 𝐹))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑇 → (abs‘(((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑢) − ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑉))) < 𝐺))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 (((abs‘(⦋𝑢 / 𝑥⦌𝐴 − ⦋𝑉 / 𝑥⦌𝐴)) < 𝐹 ∧ (abs‘(⦋𝑢 / 𝑥⦌𝐵 − ⦋𝑉 / 𝑥⦌𝐵)) < 𝐺) → (abs‘((⦋𝑢 / 𝑥⦌𝐴 · ⦋𝑢 / 𝑥⦌𝐵) − (⦋𝑉 / 𝑥⦌𝐴 · ⦋𝑉 / 𝑥⦌𝐵))) < 𝐸))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑑 → (abs‘(((𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))‘𝑢) − ((𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))‘𝑉))) < 𝐸))
Theorem	mulcncf 15585*	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	expcncf 15586*	The power function on complex numbers, for fixed exponent N, is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ))
Theorem	cnrehmeocntop 15587*	The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 10001 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if (ℝ × ℝ) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnopnap 15588*	The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.)
⊢ (𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ − )))
PART 10  BASIC REAL AND COMPLEX ANALYSIS
10.1  Continuity
Theorem	addcncf 15589*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	subcncf 15590*	The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	divcncfap 15591*	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→{𝑦 ∈ ℂ ∣ 𝑦 # 0}))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	maxcncf 15592*	The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ sup({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
Theorem	mincncf 15593*	The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ inf({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
10.1.1  Dedekind cuts
Theorem	dedekindeulemuub 15594*	Lemma for dedekindeu 15600. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐴)
Theorem	dedekindeulemub 15595*	Lemma for dedekindeu 15600. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐿 𝑦 < 𝑥)
Theorem	dedekindeulemloc 15596*	Lemma for dedekindeu 15600. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦)))
Theorem	dedekindeulemlub 15597*	Lemma for dedekindeu 15600. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
Theorem	dedekindeulemlu 15598*	Lemma for dedekindeu 15600. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
Theorem	dedekindeulemeu 15599*	Lemma for dedekindeu 15600. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐴 ∧ ∀𝑟 ∈ 𝑈 𝐴 < 𝑟))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐵 ∧ ∀𝑟 ∈ 𝑈 𝐵 < 𝑟))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ⊥)
Theorem	dedekindeu 15600*	A Dedekind cut identifies a unique real number. Similar to df-inp 7797 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.)
⊢ (𝜑 → 𝐿 ⊆ ℝ)    &   ⊢ (𝜑 → 𝑈 ⊆ ℝ)    &   ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))