Theorem List for Intuitionistic Logic Explorer - 12701-12800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cntoptopon 12701 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈
(TopOn‘ℂ) |
|
Theorem | cntoptop 12702 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈ Top |
|
Theorem | cnbl0 12703 |
Two ways to write the open ball centered at zero. (Contributed by Mario
Carneiro, 8-Sep-2015.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) |
|
Theorem | cnblcld 12704* |
Two ways to write the closed ball centered at zero. (Contributed by
Mario Carneiro, 8-Sep-2015.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) |
|
Theorem | unicntopcntop 12705 |
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 | cnopncntop 12706 |
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 | reopnap 12707* |
The real numbers apart from a given real number form an open set.
(Contributed by Jim Kingdon, 13-Dec-2023.)
|
⊢ (𝐴 ∈ ℝ → {𝑤 ∈ ℝ ∣ 𝑤 # 𝐴} ∈ (topGen‘ran
(,))) |
|
Theorem | remetdval 12708 |
Value of the distance function of the metric space of real numbers.
(Contributed by NM, 16-May-2007.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) |
|
Theorem | remet 12709 |
The absolute value metric determines a metric space on the reals.
(Contributed by NM, 10-Feb-2007.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ 𝐷 ∈
(Met‘ℝ) |
|
Theorem | rexmet 12710 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ 𝐷 ∈
(∞Met‘ℝ) |
|
Theorem | bl2ioo 12711 |
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 12712 |
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 12713 |
An open interval of reals in terms of a ball. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷)) |
|
Theorem | blssioo 12714 |
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 12715 |
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 12716 |
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 12717 |
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 12718 |
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 12719 |
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 | addcncntoplem 12720* |
Lemma for addcncntop 12721, subcncntop 12722, and mulcncntop 12723.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
22-Oct-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
))
& ⊢ + :(ℂ ×
ℂ)⟶ℂ
& ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) →
∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
|
Theorem | addcncntop 12721 |
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 12722 |
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 12723 |
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 12724* |
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 | fsumcncntop 12725* |
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 𝐾)) |
|
7.2.7 Topological definitions using the
reals
|
|
Syntax | ccncf 12726 |
Extend class notation to include the operation which returns a class of
continuous complex functions.
|
class –cn→ |
|
Definition | df-cncf 12727* |
Define the operation whose value is a class of continuous complex
functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ
↦ {𝑓 ∈ (𝑏 ↑𝑚
𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}) |
|
Theorem | cncfval 12728* |
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 12729* |
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 12730* |
Version of elcncf 12729 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) |
|
Theorem | cncfrss 12731 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) |
|
Theorem | cncfrss2 12732 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) |
|
Theorem | cncff 12733 |
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 12734* |
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 12735* |
Membership in the set of continuous complex functions from 𝐴 to
𝐵. (Contributed by Paul Chapman,
26-Nov-2007.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
& ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈
ℝ+))
& ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) →
((abs‘(𝑥 −
𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) ⇒ ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))) |
|
Theorem | elcncf1ii 12736* |
Membership in the set of continuous complex functions from 𝐴 to
𝐵. (Contributed by Paul Chapman,
26-Nov-2007.)
|
⊢ 𝐹:𝐴⟶𝐵
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈
ℝ+)
& ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) →
((abs‘(𝑥 −
𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)) |
|
Theorem | rescncf 12737 |
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 | cncffvrn 12738 |
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 12739 |
The set of continuous functions is expanded when the range is expanded.
(Contributed by Mario Carneiro, 30-Aug-2014.)
|
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶)) |
|
Theorem | climcncf 12740 |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7-Apr-2015.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺:𝑍⟶𝐴)
& ⊢ (𝜑 → 𝐺 ⇝ 𝐷)
& ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷)) |
|
Theorem | abscncf 12741 |
Absolute value is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ abs ∈ (ℂ–cn→ℝ) |
|
Theorem | recncf 12742 |
Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ ℜ ∈ (ℂ–cn→ℝ) |
|
Theorem | imcncf 12743 |
Imaginary part is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ ℑ ∈ (ℂ–cn→ℝ) |
|
Theorem | cjcncf 12744 |
Complex conjugate is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ ∗ ∈ (ℂ–cn→ℂ) |
|
Theorem | mulc1cncf 12745* |
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |
|
Theorem | divccncfap 12746* |
Division by a constant is continuous. (Contributed by Paul Chapman,
28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → 𝐹 ∈ (ℂ–cn→ℂ)) |
|
Theorem | cncfco 12747 |
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 12748 |
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 12749 |
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17-Feb-2015.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐾 = (𝐽 ↾t 𝐴)
& ⊢ 𝐿 = (𝐽 ↾t 𝐵) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿)) |
|
Theorem | cncfcn1cntop 12750 |
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 | cncfmptc 12751* |
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 12752* |
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 12753* |
Composition of continuous functions. –cn→ analogue of cnmpt11f 12453.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ)) |
|
Theorem | cncfmpt2fcntop 12754* |
Composition of continuous functions. –cn→ analogue of cnmpt12f 12455.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
))
& ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ)) |
|
Theorem | addccncf 12755* |
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |
|
Theorem | cdivcncfap 12756* |
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 12757* |
The negative function is continuous. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ)) |
|
Theorem | negfcncf 12758* |
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 12759* |
Lemma for mulcncf 12760. (Contributed by Jim Kingdon, 29-May-2023.)
|
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → 𝑉 ∈ 𝑋)
& ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐹 ∈ ℝ+) & ⊢ (𝜑 → 𝐺 ∈ ℝ+) & ⊢ (𝜑 → 𝑆 ∈ ℝ+) & ⊢ (𝜑 → 𝑇 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑆 → (abs‘(((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑢) − ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑉))) < 𝐹)) & ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑇 → (abs‘(((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑢) − ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑉))) < 𝐺)) & ⊢ (𝜑 → ∀𝑢 ∈ 𝑋 (((abs‘(⦋𝑢 / 𝑥⦌𝐴 − ⦋𝑉 / 𝑥⦌𝐴)) < 𝐹 ∧ (abs‘(⦋𝑢 / 𝑥⦌𝐵 − ⦋𝑉 / 𝑥⦌𝐵)) < 𝐺) → (abs‘((⦋𝑢 / 𝑥⦌𝐴 · ⦋𝑢 / 𝑥⦌𝐵) − (⦋𝑉 / 𝑥⦌𝐴 · ⦋𝑉 / 𝑥⦌𝐵))) < 𝐸)) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ((abs‘(𝑢 − 𝑉)) < 𝑑 → (abs‘(((𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))‘𝑢) − ((𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵))‘𝑉))) < 𝐸)) |
|
Theorem | mulcncf 12760* |
The multiplication of two continuous complex functions is continuous.
(Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ)) |
|
Theorem | expcncf 12761* |
The power function on complex numbers, for fixed exponent N, is
continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) |
|
Theorem | cnrehmeocntop 12762* |
The canonical bijection from (ℝ × ℝ)
to ℂ described in
cnref1o 9440 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 12763* |
The complex numbers apart from a given complex number form an open set.
(Contributed by Jim Kingdon, 14-Dec-2023.)
|
⊢ (𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘
− ))) |
|
PART 8 BASIC REAL AND COMPLEX
ANALYSIS
|
|
8.0.1 Dedekind cuts
|
|
Theorem | dedekindeulemuub 12764* |
Lemma for dedekindeu 12770. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐴) |
|
Theorem | dedekindeulemub 12765* |
Lemma for dedekindeu 12770. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐿 𝑦 < 𝑥) |
|
Theorem | dedekindeulemloc 12766* |
Lemma for dedekindeu 12770. The set L is located. (Contributed by Jim
Kingdon, 31-Jan-2024.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦))) |
|
Theorem | dedekindeulemlub 12767* |
Lemma for dedekindeu 12770. The set L has a least upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) |
|
Theorem | dedekindeulemlu 12768* |
Lemma for dedekindeu 12770. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |
|
Theorem | dedekindeulemeu 12769* |
Lemma for dedekindeu 12770. Part of proving uniqueness. (Contributed
by
Jim Kingdon, 31-Jan-2024.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐴 ∧ ∀𝑟 ∈ 𝑈 𝐴 < 𝑟))
& ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐵 ∧ ∀𝑟 ∈ 𝑈 𝐵 < 𝑟))
& ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ⊥) |
|
Theorem | dedekindeu 12770* |
A Dedekind cut identifies a unique real number. Similar to df-inp 7274
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.)
|
⊢ (𝜑 → 𝐿 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ⊆ ℝ) & ⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |
|
Theorem | suplociccreex 12771* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7837 but that one is for
the entire real line rather than a closed interval. (Contributed by
Jim Kingdon, 14-Feb-2024.)
|
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 𝐶)
& ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
& ⊢ (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
|
Theorem | suplociccex 12772* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7837 but that one is for the
entire real line rather than a closed interval. (Contributed by Jim
Kingdon, 14-Feb-2024.)
|
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 𝐶)
& ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
& ⊢ (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐵[,]𝐶)(∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐵[,]𝐶)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
|
Theorem | dedekindicclemuub 12773* |
Lemma for dedekindicc 12780. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon,
15-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐶) |
|
Theorem | dedekindicclemub 12774* |
Lemma for dedekindicc 12780. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ 𝐿 𝑦 < 𝑥) |
|
Theorem | dedekindicclemloc 12775* |
Lemma for dedekindicc 12780. The set L is located. (Contributed by Jim
Kingdon, 15-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦))) |
|
Theorem | dedekindicclemlub 12776* |
Lemma for dedekindicc 12780. The set L has a least upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) |
|
Theorem | dedekindicclemlu 12777* |
Lemma for dedekindicc 12780. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |
|
Theorem | dedekindicclemeu 12778* |
Lemma for dedekindicc 12780. Part of proving uniqueness. (Contributed
by Jim Kingdon, 15-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐶 ∧ ∀𝑟 ∈ 𝑈 𝐶 < 𝑟))
& ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐷 ∧ ∀𝑟 ∈ 𝑈 𝐷 < 𝑟))
& ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → ⊥) |
|
Theorem | dedekindicclemicc 12779* |
Lemma for dedekindicc 12780. Same as dedekindicc 12780, except that we
merely show 𝑥 to be an element of (𝐴[,]𝐵). Later we will
strengthen that to (𝐴(,)𝐵). (Contributed by Jim Kingdon,
5-Jan-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |
|
Theorem | dedekindicc 12780* |
A Dedekind cut identifies a unique real number. Similar to df-inp 7274
except that 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, 19-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
& ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
& ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
& ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
& ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) & ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |
|
8.0.2 Intermediate value theorem
|
|
Theorem | ivthinclemlm 12781* |
Lemma for ivthinc 12790. The lower cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿) |
|
Theorem | ivthinclemum 12782* |
Lemma for ivthinc 12790. The upper cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑅) |
|
Theorem | ivthinclemlopn 12783* |
Lemma for ivthinc 12790. The lower cut is open. (Contributed by
Jim
Kingdon, 6-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}
& ⊢ (𝜑 → 𝑄 ∈ 𝐿) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝐿 𝑄 < 𝑟) |
|
Theorem | ivthinclemlr 12784* |
Lemma for ivthinc 12790. The lower cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)) |
|
Theorem | ivthinclemuopn 12785* |
Lemma for ivthinc 12790. The upper cut is open. (Contributed by
Jim
Kingdon, 19-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}
& ⊢ (𝜑 → 𝑆 ∈ 𝑅) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝑅 𝑞 < 𝑆) |
|
Theorem | ivthinclemur 12786* |
Lemma for ivthinc 12790. The upper cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑅 ↔ ∃𝑞 ∈ 𝑅 𝑞 < 𝑟)) |
|
Theorem | ivthinclemdisj 12787* |
Lemma for ivthinc 12790. The lower and upper cuts are disjoint.
(Contributed by Jim Kingdon, 18-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → (𝐿 ∩ 𝑅) = ∅) |
|
Theorem | ivthinclemloc 12788* |
Lemma for ivthinc 12790. Locatedness. (Contributed by Jim Kingdon,
18-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅))) |
|
Theorem | ivthinclemex 12789* |
Lemma for ivthinc 12790. Existence of a number between the lower
cut
and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))
& ⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}
& ⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑧 ∧ ∀𝑟 ∈ 𝑅 𝑧 < 𝑟)) |
|
Theorem | ivthinc 12790* |
The intermediate value theorem, increasing case, for a strictly
monotonic function. Theorem 5.5 of [Bauer], p. 494. This is
Metamath 100 proof #79. (Contributed by Jim Kingdon,
5-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) |
|
Theorem | ivthdec 12791* |
The intermediate value theorem, decreasing case, for a strictly
monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
& ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴))) & ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) < (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) |
|
8.1 Derivatives
|
|
8.1.1 Real and complex
differentiation
|
|
8.1.1.1 Derivatives of functions of one complex
or real variable
|
|
Syntax | climc 12792 |
The limit operator.
|
class limℂ |
|
Syntax | cdv 12793 |
The derivative operator.
|
class D |
|
Definition | df-limced 12794* |
Define the set of limits of a complex function at a point. Under normal
circumstances, this will be a singleton or empty, depending on whether
the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.)
(Revised by Jim Kingdon, 3-Jun-2023.)
|
⊢ limℂ = (𝑓 ∈ (ℂ ↑pm
ℂ), 𝑥 ∈ ℂ
↦ {𝑦 ∈ ℂ
∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))}) |
|
Definition | df-dvap 12795* |
Define the derivative operator. This acts on functions to produce a
function that is defined where the original function is differentiable,
with value the derivative of the function at these points. The set
𝑠 here is the ambient topological space
under which we are
evaluating the continuity of the difference quotient. Although the
definition is valid for any subset of ℂ
and is well-behaved when
𝑠 contains no isolated points, we will
restrict our attention to the
cases 𝑠 = ℝ or 𝑠 = ℂ for the
majority of the development,
these corresponding respectively to real and complex differentiation.
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon,
25-Jun-2023.)
|
⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ
↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs
∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
|
Theorem | limcrcl 12796 |
Reverse closure for the limit operator. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
|
Theorem | limccl 12797 |
Closure of the limit operator. (Contributed by Mario Carneiro,
25-Dec-2016.)
|
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ |
|
Theorem | ellimc3apf 12798* |
Write the epsilon-delta definition of a limit. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
|
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢
Ⅎ𝑧𝐹 ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
|
Theorem | ellimc3ap 12799* |
Write the epsilon-delta definition of a limit. (Contributed by Mario
Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon,
3-Jun-2023.)
|
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
|
Theorem | limcdifap 12800* |
It suffices to consider functions which are not defined at 𝐵 to
define the limit of a function. In particular, the value of the
original function 𝐹 at 𝐵 does not affect the
limit of 𝐹.
(Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon,
3-Jun-2023.)
|
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ)
⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝑥 # 𝐵}) limℂ 𝐵)) |