Theorem List for Intuitionistic Logic Explorer - 12801-12900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | limcmpted 12801* |
Express the limit operator for a function defined by a mapping, via
epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐶 ∈ ((𝑧 ∈ 𝐴 ↦ 𝐷) limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘(𝐷 − 𝐶)) < 𝑥)))) |
|
Theorem | limcimolemlt 12802* |
Lemma for limcimo 12803. (Contributed by Jim Kingdon, 3-Jul-2023.)
|
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆)) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
& ⊢ 𝐾 = (MetOpen‘(abs ∘ −
))
& ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2))) & ⊢ (𝜑 → 𝐺 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2))) ⇒ ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌))) |
|
Theorem | limcimo 12803* |
Conditions which ensure there is at most one limit value of 𝐹 at
𝐵. (Contributed by Mario Carneiro,
25-Dec-2016.) (Revised by
Jim Kingdon, 8-Jul-2023.)
|
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆)) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
& ⊢ 𝐾 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐹 limℂ 𝐵)) |
|
Theorem | limcresi 12804 |
Any limit of 𝐹 is also a limit of the restriction
of 𝐹.
(Contributed by Mario Carneiro, 28-Dec-2016.)
|
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵) |
|
Theorem | cnplimcim 12805 |
If a function is continuous at 𝐵, its limit at 𝐵 equals the
value of the function there. (Contributed by Mario Carneiro,
28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)
|
⊢ 𝐾 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐽 = (𝐾 ↾t 𝐴) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) → (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)))) |
|
Theorem | cnplimclemle 12806 |
Lemma for cnplimccntop 12808. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17-Nov-2023.)
|
⊢ 𝐾 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐽 = (𝐾 ↾t 𝐴)
& ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐴)
& ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝑍 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑍 # 𝐵 ∧ (abs‘(𝑍 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑍) − (𝐹‘𝐵))) < (𝐸 / 2)) & ⊢ (𝜑 → (abs‘(𝑍 − 𝐵)) < 𝐷) ⇒ ⊢ (𝜑 → (abs‘((𝐹‘𝑍) − (𝐹‘𝐵))) < 𝐸) |
|
Theorem | cnplimclemr 12807 |
Lemma for cnplimccntop 12808. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|
⊢ 𝐾 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐽 = (𝐾 ↾t 𝐴)
& ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐴)
& ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) |
|
Theorem | cnplimccntop 12808 |
A function is continuous at 𝐵 iff its limit at 𝐵 equals
the
value of the function there. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
⊢ 𝐾 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐽 = (𝐾 ↾t 𝐴) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)))) |
|
Theorem | cnlimcim 12809* |
If 𝐹 is a continuous function, the limit
of the function at each
point equals the value of the function. (Contributed by Mario Carneiro,
28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.)
|
⊢ (𝐴 ⊆ ℂ → (𝐹 ∈ (𝐴–cn→ℂ) → (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐹 limℂ 𝑥)))) |
|
Theorem | cnlimc 12810* |
𝐹
is a continuous function iff the limit of the function at each
point equals the value of the function. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
⊢ (𝐴 ⊆ ℂ → (𝐹 ∈ (𝐴–cn→ℂ) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐹 limℂ 𝑥)))) |
|
Theorem | cnlimci 12811 |
If 𝐹 is a continuous function, then the
limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐷)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)) |
|
Theorem | cnmptlimc 12812* |
If 𝐹 is a continuous function, then the
limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑋) ∈ (𝐴–cn→𝐷)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴)
& ⊢ (𝑥 = 𝐵 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → 𝑌 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑋) limℂ 𝐵)) |
|
Theorem | limccnpcntop 12813 |
If the limit of 𝐹 at 𝐵 is 𝐶 and
𝐺
is continuous at
𝐶, then the limit of 𝐺 ∘ 𝐹 at 𝐵 is
𝐺(𝐶).
(Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon,
18-Jun-2023.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐷)
& ⊢ (𝜑 → 𝐷 ⊆ ℂ) & ⊢ 𝐾 = (MetOpen‘(abs ∘
− ))
& ⊢ 𝐽 = (𝐾 ↾t 𝐷)
& ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐶)) ⇒ ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝐺 ∘ 𝐹) limℂ 𝐵)) |
|
Theorem | limccnp2lem 12814* |
Lemma for limccnp2cntop 12815. This is most of the result, expressed in
epsilon-delta form, with a large number of hypotheses so that lengthy
expressions do not need to be repeated. (Contributed by Jim Kingdon,
9-Nov-2023.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑌 ⊆ ℂ) & ⊢ 𝐾 = (MetOpen‘(abs ∘
− ))
& ⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵)) & ⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) & ⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐿 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝐿 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝐿) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝐸)) & ⊢ (𝜑 → 𝐹 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝐹) → (abs‘(𝑅 − 𝐶)) < 𝐿)) & ⊢ (𝜑 → 𝐺 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝐺) → (abs‘(𝑆 − 𝐷)) < 𝐿)) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝐸)) |
|
Theorem | limccnp2cntop 12815* |
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. Binary operation version.
(Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon,
14-Nov-2023.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌)
& ⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑌 ⊆ ℂ) & ⊢ 𝐾 = (MetOpen‘(abs ∘
− ))
& ⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵)) & ⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) ⇒ ⊢ (𝜑 → (𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵)) |
|
Theorem | limccoap 12816* |
Composition of two limits. This theorem is only usable in the case
where 𝑥 # 𝑋 implies R(x) #
𝐶 so it is less
general than
might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.)
(Revised by Jim Kingdon, 18-Dec-2023.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋}) → 𝑅 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶}) & ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶}) → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋} ↦ 𝑅) limℂ 𝑋)) & ⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶} ↦ 𝑆) limℂ 𝐶)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋} ↦ 𝑇) limℂ 𝑋)) |
|
Theorem | reldvg 12817 |
The derivative function is a relation. (Contributed by Mario Carneiro,
7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm
𝑆)) → Rel (𝑆 D 𝐹)) |
|
Theorem | dvlemap 12818* |
Closure for a difference quotient. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝐷 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑤 ∈ 𝐷 ∣ 𝑤 # 𝐵}) → (((𝐹‘𝐴) − (𝐹‘𝐵)) / (𝐴 − 𝐵)) ∈ ℂ) |
|
Theorem | dvfvalap 12819* |
Value and set bounds on the derivative operator. (Contributed by Mario
Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
⊢ 𝑇 = (𝐾 ↾t 𝑆)
& ⊢ 𝐾 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → ((𝑆 D 𝐹) = ∪
𝑥 ∈ ((int‘𝑇)‘𝐴)({𝑥} × ((𝑧 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑥} ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) ∧ (𝑆 D 𝐹) ⊆ (((int‘𝑇)‘𝐴) × ℂ))) |
|
Theorem | eldvap 12820* |
The differentiable predicate. A function 𝐹 is differentiable at
𝐵 with derivative 𝐶 iff
𝐹
is defined in a neighborhood of
𝐵 and the difference quotient has
limit 𝐶 at 𝐵.
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon,
27-Jun-2023.)
|
⊢ 𝑇 = (𝐾 ↾t 𝑆)
& ⊢ 𝐾 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐺 = (𝑧 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝐵} ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐵(𝑆 D 𝐹)𝐶 ↔ (𝐵 ∈ ((int‘𝑇)‘𝐴) ∧ 𝐶 ∈ (𝐺 limℂ 𝐵)))) |
|
Theorem | dvcl 12821 |
The derivative function takes values in the complex numbers.
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario
Carneiro, 9-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝐵(𝑆 D 𝐹)𝐶) → 𝐶 ∈ ℂ) |
|
Theorem | dvbssntrcntop 12822 |
The set of differentiable points is a subset of the interior of the
domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.)
(Revised by Jim Kingdon, 27-Jun-2023.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
& ⊢ 𝐽 = (𝐾 ↾t 𝑆)
& ⊢ 𝐾 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ ((int‘𝐽)‘𝐴)) |
|
Theorem | dvbss 12823 |
The set of differentiable points is a subset of the domain of the
function. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by
Mario Carneiro, 9-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝐴) |
|
Theorem | dvbsssg 12824 |
The set of differentiable points is a subset of the ambient topology.
(Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon,
28-Jun-2023.)
|
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm
𝑆)) → dom (𝑆 D 𝐹) ⊆ 𝑆) |
|
Theorem | recnprss 12825 |
Both ℝ and ℂ are
subsets of ℂ. (Contributed by Mario
Carneiro, 10-Feb-2015.)
|
⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆
ℂ) |
|
Theorem | dvfgg 12826 |
Explicitly write out the functionality condition on derivative for
𝑆 =
ℝ and ℂ. (Contributed by Mario
Carneiro, 9-Feb-2015.)
(Revised by Jim Kingdon, 28-Jun-2023.)
|
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
|
Theorem | dvfpm 12827 |
The derivative is a function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
⊢ (𝐹 ∈ (ℂ ↑pm
ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ) |
|
Theorem | dvfcnpm 12828 |
The derivative is a function. (Contributed by Mario Carneiro,
9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
⊢ (𝐹 ∈ (ℂ ↑pm
ℂ) → (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ) |
|
Theorem | dvidlemap 12829* |
Lemma for dvid 12831 and dvconst 12830. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)
& ⊢ 𝐵 ∈ ℂ
⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ × {𝐵})) |
|
Theorem | dvconst 12830 |
Derivative of a constant function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
⊢ (𝐴 ∈ ℂ → (ℂ D (ℂ
× {𝐴})) = (ℂ
× {0})) |
|
Theorem | dvid 12831 |
Derivative of the identity function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
⊢ (ℂ D ( I ↾ ℂ)) = (ℂ
× {1}) |
|
Theorem | dvcnp2cntop 12832 |
A function is continuous at each point for which it is differentiable.
(Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario
Carneiro, 28-Dec-2016.)
|
⊢ 𝐽 = (𝐾 ↾t 𝐴)
& ⊢ 𝐾 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) |
|
Theorem | dvcn 12833 |
A differentiable function is continuous. (Contributed by Mario
Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ dom (𝑆 D 𝐹) = 𝐴) → 𝐹 ∈ (𝐴–cn→ℂ)) |
|
Theorem | dvaddxxbr 12834 |
The sum rule for derivatives at a point. That is, if the derivative
of 𝐹 at 𝐶 is 𝐾 and the
derivative of 𝐺 at 𝐶 is
𝐿, then the derivative of the
pointwise sum of those two
functions at 𝐶 is 𝐾 + 𝐿. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
& ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
& ⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿)) |
|
Theorem | dvmulxxbr 12835 |
The product rule for derivatives at a point. For the (simpler but
more limited) function version, see dvmulxx 12837. (Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
|
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
& ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
& ⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶)))) |
|
Theorem | dvaddxx 12836 |
The sum rule for derivatives at a point. For the (more general)
relation version, see dvaddxxbr 12834. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺)) ⇒ ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝐶) = (((𝑆 D 𝐹)‘𝐶) + ((𝑆 D 𝐺)‘𝐶))) |
|
Theorem | dvmulxx 12837 |
The product rule for derivatives at a point. For the (more general)
relation version, see dvmulxxbr 12835. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
|
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) & ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺)) ⇒ ⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶)))) |
|
Theorem | dviaddf 12838 |
The sum rule for everywhere-differentiable functions. (Contributed by
Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
& ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 + 𝐺)) = ((𝑆 D 𝐹) ∘𝑓 + (𝑆 D 𝐺))) |
|
Theorem | dvimulf 12839 |
The product rule for everywhere-differentiable functions. (Contributed
by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
& ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 · 𝐺)) = (((𝑆 D 𝐹) ∘𝑓 ·
𝐺)
∘𝑓 + ((𝑆 D 𝐺) ∘𝑓 ·
𝐹))) |
|
Theorem | dvcoapbr 12840* |
The chain rule for derivatives at a point. The
𝑢
# 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶) hypothesis constrains what
functions work for 𝐺. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
|
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ (𝜑 → 𝐺:𝑌⟶𝑋)
& ⊢ (𝜑 → 𝑌 ⊆ 𝑇)
& ⊢ (𝜑 → ∀𝑢 ∈ 𝑌 (𝑢 # 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶))) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑇 ⊆ ℂ) & ⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾)
& ⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿)
& ⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿)) |
|
Theorem | dvcjbr 12841 |
The derivative of the conjugate of a function. For the (simpler but
more limited) function version, see dvcj 12842. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹)) ⇒ ⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D
𝐹)‘𝐶))) |
|
Theorem | dvcj 12842 |
The derivative of the conjugate of a function. For the (more general)
relation version, see dvcjbr 12841. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → (ℝ D
(∗ ∘ 𝐹)) =
(∗ ∘ (ℝ D 𝐹))) |
|
Theorem | dvfre 12843 |
The derivative of a real function is real. (Contributed by Mario
Carneiro, 1-Sep-2014.)
|
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
|
Theorem | dvexp 12844* |
Derivative of a power function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
⊢ (𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) |
|
Theorem | dvexp2 12845* |
Derivative of an exponential, possibly zero power. (Contributed by
Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
⊢ (𝑁 ∈ ℕ0 → (ℂ
D (𝑥 ∈ ℂ
↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))) |
|
Theorem | dvrecap 12846* |
Derivative of the reciprocal function. (Contributed by Mario Carneiro,
25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|
⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ↦ (𝐴 / 𝑥))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ↦ -(𝐴 / (𝑥↑2)))) |
|
Theorem | dvmptidcn 12847 |
Function-builder for derivative: derivative of the identity.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
⊢ (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1) |
|
Theorem | dvmptccn 12848* |
Function-builder for derivative: derivative of a constant. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 0)) |
|
Theorem | dvmptclx 12849* |
Closure lemma for dvmptmulx 12851 and other related theorems. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro,
11-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) |
|
Theorem | dvmptaddx 12850* |
Function-builder for derivative, addition rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)
& ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐶))) = (𝑥 ∈ 𝑋 ↦ (𝐵 + 𝐷))) |
|
Theorem | dvmptmulx 12851* |
Function-builder for derivative, product rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ 𝑊)
& ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐶)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐶))) = (𝑥 ∈ 𝑋 ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴)))) |
|
Theorem | dvmptcmulcn 12852* |
Function-builder for derivative, product rule for constant multiplier.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐶 · 𝐴))) = (𝑥 ∈ ℂ ↦ (𝐶 · 𝐵))) |
|
Theorem | dvmptnegcn 12853* |
Function-builder for derivative, product rule for negatives.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵)) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ -𝐴)) = (𝑥 ∈ ℂ ↦ -𝐵)) |
|
Theorem | dvmptsubcn 12854* |
Function-builder for derivative, subtraction rule. (Contributed by
Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐷 ∈ 𝑊)
& ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐶)) = (𝑥 ∈ ℂ ↦ 𝐷)) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 − 𝐶))) = (𝑥 ∈ ℂ ↦ (𝐵 − 𝐷))) |
|
Theorem | dveflem 12855 |
Derivative of the exponential function at 0. The key step in the proof
is eftlub 11396, to show that
abs(exp(𝑥) − 1 − 𝑥) ≤ abs(𝑥)↑2 · (3 / 4).
(Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario
Carneiro, 28-Dec-2016.)
|
⊢ 0(ℂ D exp)1 |
|
Theorem | dvef 12856 |
Derivative of the exponential function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
|
⊢ (ℂ D exp) = exp |
|
PART 9 BASIC REAL AND COMPLEX
FUNCTIONS
|
|
9.1 Basic trigonometry
|
|
9.1.1 The exponential, sine, and cosine
functions (cont.)
|
|
Theorem | efcn 12857 |
The exponential function is continuous. (Contributed by Paul Chapman,
15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
|
⊢ exp ∈ (ℂ–cn→ℂ) |
|
Theorem | sincn 12858 |
Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
⊢ sin ∈ (ℂ–cn→ℂ) |
|
Theorem | coscn 12859 |
Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
⊢ cos ∈ (ℂ–cn→ℂ) |
|
9.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 12860 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧
(sin‘𝐴) =
0)) |
|
Theorem | cosz12 12861 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
⊢ ∃𝑝 ∈ (1(,)2)(cos‘𝑝) = 0 |
|
Theorem | sin0pilem1 12862* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
⊢ ∃𝑝 ∈ (1(,)2)((cos‘𝑝) = 0 ∧ ∀𝑥 ∈ (𝑝(,)(2 · 𝑝))0 < (sin‘𝑥)) |
|
Theorem | sin0pilem2 12863* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
⊢ ∃𝑞 ∈ (2(,)4)((sin‘𝑞) = 0 ∧ ∀𝑥 ∈ (0(,)𝑞)0 < (sin‘𝑥)) |
|
Theorem | pilem3 12864 |
Lemma for pi related theorems. (Contributed by Jim Kingdon,
9-Mar-2024.)
|
⊢ (π ∈ (2(,)4) ∧ (sin‘π)
= 0) |
|
Theorem | pigt2lt4 12865 |
π is between 2 and 4. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
⊢ (2 < π ∧ π <
4) |
|
Theorem | sinpi 12866 |
The sine of π is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (sin‘π) = 0 |
|
Theorem | pire 12867 |
π is a real number. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ π ∈ ℝ |
|
Theorem | picn 12868 |
π is a complex number. (Contributed by David A.
Wheeler,
6-Dec-2018.)
|
⊢ π ∈ ℂ |
|
Theorem | pipos 12869 |
π is positive. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
⊢ 0 < π |
|
Theorem | pirp 12870 |
π is a positive real. (Contributed by Glauco
Siliprandi,
11-Dec-2019.)
|
⊢ π ∈
ℝ+ |
|
Theorem | negpicn 12871 |
-π is a real number. (Contributed by David A.
Wheeler,
8-Dec-2018.)
|
⊢ -π ∈ ℂ |
|
Theorem | sinhalfpilem 12872 |
Lemma for sinhalfpi 12877 and coshalfpi 12878. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ ((sin‘(π / 2)) = 1 ∧
(cos‘(π / 2)) = 0) |
|
Theorem | halfpire 12873 |
π / 2 is real. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (π / 2) ∈ ℝ |
|
Theorem | neghalfpire 12874 |
-π / 2 is real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ -(π / 2) ∈ ℝ |
|
Theorem | neghalfpirx 12875 |
-π / 2 is an extended real. (Contributed by David
A. Wheeler,
8-Dec-2018.)
|
⊢ -(π / 2) ∈
ℝ* |
|
Theorem | pidiv2halves 12876 |
Adding π / 2 to itself gives π. See 2halves 8949.
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ ((π / 2) + (π / 2)) =
π |
|
Theorem | sinhalfpi 12877 |
The sine of π / 2 is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (sin‘(π / 2)) = 1 |
|
Theorem | coshalfpi 12878 |
The cosine of π / 2 is 0. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (cos‘(π / 2)) = 0 |
|
Theorem | cosneghalfpi 12879 |
The cosine of -π / 2 is zero. (Contributed by David
Moews,
28-Feb-2017.)
|
⊢ (cos‘-(π / 2)) = 0 |
|
Theorem | efhalfpi 12880 |
The exponential of iπ / 2 is i. (Contributed by Mario
Carneiro, 9-May-2014.)
|
⊢ (exp‘(i · (π / 2))) =
i |
|
Theorem | cospi 12881 |
The cosine of π is -1.
(Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (cos‘π) = -1 |
|
Theorem | efipi 12882 |
The exponential of i · π is -1. (Contributed by Paul
Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ (exp‘(i · π)) =
-1 |
|
Theorem | eulerid 12883 |
Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised
by Mario Carneiro, 9-May-2014.)
|
⊢ ((exp‘(i · π)) + 1) =
0 |
|
Theorem | sin2pi 12884 |
The sine of 2π is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (sin‘(2 · π)) =
0 |
|
Theorem | cos2pi 12885 |
The cosine of 2π is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (cos‘(2 · π)) =
1 |
|
Theorem | ef2pi 12886 |
The exponential of 2πi is 1.
(Contributed by Mario
Carneiro, 9-May-2014.)
|
⊢ (exp‘(i · (2 · π))) =
1 |
|
Theorem | ef2kpi 12887 |
If 𝐾 is an integer, then the exponential
of 2𝐾πi is 1.
(Contributed by Mario Carneiro, 9-May-2014.)
|
⊢ (𝐾 ∈ ℤ → (exp‘((i
· (2 · π)) · 𝐾)) = 1) |
|
Theorem | efper 12888 |
The exponential function is periodic. (Contributed by Paul Chapman,
21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (exp‘(𝐴 + ((i · (2 ·
π)) · 𝐾))) =
(exp‘𝐴)) |
|
Theorem | sinperlem 12889 |
Lemma for sinper 12890 and cosper 12891. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐹‘𝐴) = (((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷)) & ⊢ ((𝐴 + (𝐾 · (2 · π))) ∈
ℂ → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) =
(((exp‘(i · (𝐴 + (𝐾 · (2 · π)))))𝑂(exp‘(-i · (𝐴 + (𝐾 · (2 · π)))))) / 𝐷))
⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (𝐹‘𝐴)) |
|
Theorem | sinper 12890 |
The sine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) =
(sin‘𝐴)) |
|
Theorem | cosper 12891 |
The cosine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) =
(cos‘𝐴)) |
|
Theorem | sin2kpi 12892 |
If 𝐾 is an integer, then the sine of
2𝐾π is 0. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · (2 · π))) =
0) |
|
Theorem | cos2kpi 12893 |
If 𝐾 is an integer, then the cosine of
2𝐾π is 1. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · (2 · π))) =
1) |
|
Theorem | sin2pim 12894 |
Sine of a number subtracted from 2 · π.
(Contributed by Paul
Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((2
· π) − 𝐴))
= -(sin‘𝐴)) |
|
Theorem | cos2pim 12895 |
Cosine of a number subtracted from 2 · π.
(Contributed by Paul
Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((2
· π) − 𝐴))
= (cos‘𝐴)) |
|
Theorem | sinmpi 12896 |
Sine of a number less π. (Contributed by Paul
Chapman,
15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) =
-(sin‘𝐴)) |
|
Theorem | cosmpi 12897 |
Cosine of a number less π. (Contributed by Paul
Chapman,
15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) =
-(cos‘𝐴)) |
|
Theorem | sinppi 12898 |
Sine of a number plus π. (Contributed by NM,
10-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) |
|
Theorem | cosppi 12899 |
Cosine of a number plus π. (Contributed by NM,
18-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) |
|
Theorem | efimpi 12900 |
The exponential function at i times a real number less
π.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(i
· (𝐴 −
π))) = -(exp‘(i · 𝐴))) |