Home | Metamath
Proof Explorer Theorem List (p. 421 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xlimclim2 42001 | Given a sequence of extended reals, it converges to a real number 𝐴 w.r.t. the standard topology on the reals (see climreeq 41774), if and only if it converges to 𝐴 w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴)) | ||
Theorem | xlimmnf 42002* | A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥)) | ||
Theorem | xlimpnf 42003* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))) | ||
Theorem | xlimmnfmpt 42004* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ*) & ⊢ 𝐹 = (𝑘 ∈ 𝑍 ↦ 𝐵) ⇒ ⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐵 ≤ 𝑥)) | ||
Theorem | xlimpnfmpt 42005* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ*) & ⊢ 𝐹 = (𝑘 ∈ 𝑍 ↦ 𝐵) ⇒ ⊢ (𝜑 → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ 𝐵)) | ||
Theorem | climxlim2lem 42006 | In this lemma for climxlim2 42007 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → 𝐹~~>*𝐴) | ||
Theorem | climxlim2 42007 | A sequence of extended reals, converging w.r.t. the standard topology on the complex numbers is a converging sequence w.r.t. the standard topology on the extended reals. This is non-trivial, because +∞ and -∞ could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → 𝐹~~>*𝐴) | ||
Theorem | dfxlim2v 42008* | An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))))) | ||
Theorem | dfxlim2 42009* | An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘))))) | ||
Theorem | climresd 42010 | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴)) | ||
Theorem | climresdm 42011 | A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ⇝ )) | ||
Theorem | dmclimxlim 42012 | A real valued sequence that converges w.r.t. the topology on the complex numbers, converges w.r.t. the topology on the extended reals (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ~~>*) | ||
Theorem | xlimmnflimsup2 42013 | A sequence of extended reals converges to -∞ if and only if its superior limit is also -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*-∞ ↔ (lim sup‘𝐹) = -∞)) | ||
Theorem | xlimuni 42014 | An infinite sequence converges to at most one limit (w.r.t. to the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝐹~~>*𝐴) & ⊢ (𝜑 → 𝐹~~>*𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xlimclimdm 42015 | A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) & ⊢ (𝜑 → 𝐹~~>*𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) | ||
Theorem | xlimfun 42016 | The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ Fun ~~>* | ||
Theorem | xlimmnflimsup 42017 | If a sequence of extended reals converges to -∞ then its superior limit is also -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) & ⊢ (𝜑 → 𝐹~~>*-∞) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = -∞) | ||
Theorem | xlimdm 42018 | Two ways to express that a function has a limit. (The expression (~~>*‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝐹 ∈ dom ~~>* ↔ 𝐹~~>*(~~>*‘𝐹)) | ||
Theorem | xlimpnfxnegmnf2 42019* | A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*+∞ ↔ (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))~~>*-∞)) | ||
Theorem | xlimresdm 42020 | A function converges in the extended reals iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ~~>*)) | ||
Theorem | xlimpnfliminf 42021 | If a sequence of extended reals converges to +∞ then its superior limit is also +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) & ⊢ (𝜑 → 𝐹~~>*+∞) ⇒ ⊢ (𝜑 → (lim inf‘𝐹) = +∞) | ||
Theorem | xlimpnfliminf2 42022 | A sequence of extended reals converges to +∞ if and only if its superior limit is also +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹~~>*+∞ ↔ (lim inf‘𝐹) = +∞)) | ||
Theorem | xlimliminflimsup 42023 | A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (lim inf‘𝐹) = (lim sup‘𝐹))) | ||
Theorem | xlimlimsupleliminf 42024 | A sequence of extended reals converges if and only if its superior limit is smaller than or equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Dec-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (lim sup‘𝐹) ≤ (lim inf‘𝐹))) | ||
Theorem | coseq0 42025 | A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) = 0 ↔ ((𝐴 / π) + (1 / 2)) ∈ ℤ)) | ||
Theorem | sinmulcos 42026 | Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (cos‘𝐵)) = (((sin‘(𝐴 + 𝐵)) + (sin‘(𝐴 − 𝐵))) / 2)) | ||
Theorem | coskpi2 42027 | The cosine of an integer multiple of negative π is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · π)) = if(2 ∥ 𝐾, 1, -1)) | ||
Theorem | cosnegpi 42028 | The cosine of negative π is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (cos‘-π) = -1 | ||
Theorem | sinaover2ne0 42029 | If 𝐴 in (0, 2π) then sin(𝐴 / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (0(,)(2 · π)) → (sin‘(𝐴 / 2)) ≠ 0) | ||
Theorem | cosknegpi 42030 | The cosine of an integer multiple of negative π is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)) | ||
Theorem | mulcncff 42031 | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (𝑋–cn→ℂ)) | ||
Theorem | subcncf 42032* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmptssg 42033* | A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 41748 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐸 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷)) | ||
Theorem | constcncfg 42034* | A constant function is a continuous function on ℂ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ⊆ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→𝐶)) | ||
Theorem | idcncfg 42035* | The identity function is a continuous function on ℂ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (𝐴–cn→𝐵)) | ||
Theorem | addcncf 42036* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfshift 42037* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) & ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐹‘(𝑥 − 𝑇))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→ℂ)) | ||
Theorem | resincncf 42038 | sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ) | ||
Theorem | addccncf2 42039* | Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝑥)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | 0cnf 42040 | The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ∅ ∈ ({∅} Cn {∅}) | ||
Theorem | fsumcncf 42041* | The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfperiod 42042* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} & ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) & ⊢ (𝜑 → 𝐵 ⊆ dom 𝐹) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ)) | ||
Theorem | subcncff 42043 | The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (𝑋–cn→ℂ)) | ||
Theorem | negcncfg 42044* | The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (𝐴–cn→ℂ)) | ||
Theorem | cnfdmsn 42045* | A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) ∈ (𝒫 {𝐴} Cn 𝒫 {𝐵})) | ||
Theorem | cncfcompt 42046* | Composition of continuous functions. A generalization of cncfmpt1f 23450 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→𝐶)) & ⊢ (𝜑 → 𝐹 ∈ (𝐶–cn→𝐷)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→𝐷)) | ||
Theorem | addcncff 42047 | The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (𝑋–cn→ℂ)) | ||
Theorem | ioccncflimc 42048 | Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,]𝐵)–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵)) | ||
Theorem | cncfuni 42049* | A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵) & ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴)) & ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | icccncfext 42050* | A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝐹 & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑌 = ∪ 𝐾 & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴[,]𝐵), (𝐹‘𝑥), if(𝑥 < 𝐴, (𝐹‘𝐴), (𝐹‘𝐵)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝐺 ∈ (𝐽 Cn (𝐾 ↾t ran 𝐹)) ∧ (𝐺 ↾ (𝐴[,]𝐵)) = 𝐹)) | ||
Theorem | cncficcgt0 42051* | A the absolute value of a continuous function on a closed interval, that is never 0, has a strictly positive lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0}))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) | ||
Theorem | icocncflimc 42052 | Limit at the lower bound, of a continuous function defined on a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,)𝐵)–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴)) | ||
Theorem | cncfdmsn 42053* | A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ {𝐴} ↦ 𝐵) ∈ ({𝐴}–cn→{𝐵})) | ||
Theorem | divcncff 42054 | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→(ℂ ∖ {0}))) ⇒ ⊢ (𝜑 → (𝐹 ∘f / 𝐺) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfshiftioo 42055* | A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐶 = (𝐴(,)𝐵) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ 𝐷 = ((𝐴 + 𝑇)(,)(𝐵 + 𝑇)) & ⊢ (𝜑 → 𝐹 ∈ (𝐶–cn→ℂ)) & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (𝐹‘(𝑥 − 𝑇))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐷–cn→ℂ)) | ||
Theorem | cncfiooicclem1 42056* | A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 can be complex-valued. This lemma assumes 𝐴 < 𝐵, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) | ||
Theorem | cncfiooicc 42057* | A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 can be complex-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) | ||
Theorem | cncfiooiccre 42058* | A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 is assumed to be real-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) | ||
Theorem | cncfioobdlem 42059* | 𝐺 actually extends 𝐹. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶𝑉) & ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → (𝐺‘𝐶) = (𝐹‘𝐶)) | ||
Theorem | cncfioobd 42060* | A continuous function 𝐹 on an open interval (𝐴(,)𝐵) with a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵 is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥) | ||
Theorem | jumpncnp 42061 | Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) & ⊢ (𝜑 → 𝐿 ≠ 𝑅) ⇒ ⊢ (𝜑 → ¬ 𝐹 ∈ ((𝐽 CnP (TopOpen‘ℂfld))‘𝐵)) | ||
Theorem | cncfcompt2 42062* | Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑆) ∈ (𝐶–cn→𝐸)) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑇) ∈ (𝐴–cn→𝐸)) | ||
Theorem | cxpcncf2 42063* | The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝐴 ∈ (ℂ ∖ (-∞(,]0)) → (𝑥 ∈ ℂ ↦ (𝐴↑𝑐𝑥)) ∈ (ℂ–cn→ℂ)) | ||
Theorem | fprodcncf 42064* | The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝐵 𝐶) ∈ (𝐴–cn→ℂ)) | ||
Theorem | add1cncf 42065* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | add2cncf 42066* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | sub1cncfd 42067* | Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | sub2cncfd 42068* | Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | fprodsub2cncf 42069* | 𝐹 is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 − 𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | fprodadd2cncf 42070* | 𝐹 is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | fprodsubrecnncnvlem 42071* | The sequence 𝑆 of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝐴 (𝐵 − (1 / 𝑛))) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 − 𝑥)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fprodsubrecnncnv 42072* | The sequence 𝑆 of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (𝐴 − (1 / 𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 𝐴) | ||
Theorem | fprodaddrecnncnvlem 42073* | The sequence 𝑆 of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝐴 (𝐵 + (1 / 𝑛))) & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 + 𝑥)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fprodaddrecnncnv 42074* | The sequence 𝑆 of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (𝐴 + (1 / 𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 𝐴) | ||
Theorem | dvsinexp 42075* | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))) = (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) | ||
Theorem | dvcosre 42076 | The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (ℝ D (𝑥 ∈ ℝ ↦ (cos‘𝑥))) = (𝑥 ∈ ℝ ↦ -(sin‘𝑥)) | ||
Theorem | dvsinax 42077* | Derivative exercise: the derivative with respect to y of sin(Ay), given a constant 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) | ||
Theorem | dvsubf 42078 | The subtraction rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) & ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f − 𝐺)) = ((𝑆 D 𝐹) ∘f − (𝑆 D 𝐺))) | ||
Theorem | dvmptconst 42079* | Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐴 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ 0)) | ||
Theorem | dvcnre 42080 | From compex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐹:ℂ⟶ℂ ∧ ℝ ⊆ dom (ℂ D 𝐹)) → (ℝ D (𝐹 ↾ ℝ)) = ((ℂ D 𝐹) ↾ ℝ)) | ||
Theorem | dvmptidg 42081* | Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐴 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) ⇒ ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝐴 ↦ 𝑥)) = (𝑥 ∈ 𝐴 ↦ 1)) | ||
Theorem | dvresntr 42082 | Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → ((int‘𝐽)‘𝑋) = 𝑌) ⇒ ⊢ (𝜑 → (𝑆 D 𝐹) = (𝑆 D (𝐹 ↾ 𝑌))) | ||
Theorem | fperdvper 42083* | The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = (ℝ D 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))) | ||
Theorem | dvmptresicc 42084* | Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐶[,]𝐷) ↦ 𝐴)) = (𝑥 ∈ (𝐶(,)𝐷) ↦ 𝐵)) | ||
Theorem | dvasinbx 42085* | Derivative exercise: the derivative with respect to y of A x sin(By), given two constants 𝐴 and 𝐵. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ (𝐴 · (sin‘(𝐵 · 𝑦))))) = (𝑦 ∈ ℂ ↦ ((𝐴 · 𝐵) · (cos‘(𝐵 · 𝑦))))) | ||
Theorem | dvresioo 42086 | Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:𝐴⟶ℂ) → (ℝ D (𝐹 ↾ (𝐵(,)𝐶))) = ((ℝ D 𝐹) ↾ (𝐵(,)𝐶))) | ||
Theorem | dvdivf 42087 | The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶(ℂ ∖ {0})) & ⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) & ⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f / 𝐺)) = ((((𝑆 D 𝐹) ∘f · 𝐺) ∘f − ((𝑆 D 𝐺) ∘f · 𝐹)) ∘f / (𝐺 ∘f · 𝐺))) | ||
Theorem | dvdivbd 42088* | A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑄 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘𝐶) ≤ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘𝐵) ≤ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘𝐷) ≤ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘𝐴) ≤ 𝑄) & ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐸 ≤ (abs‘𝐵)) & ⊢ 𝐹 = (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵))) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘(𝐹‘𝑥)) ≤ 𝑏) | ||
Theorem | dvsubcncf 42089 | A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → (𝑆 D 𝐹) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑆 D 𝐺) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f − 𝐺)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | dvmulcncf 42090 | A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ (𝜑 → (𝑆 D 𝐹) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑆 D 𝐺) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f · 𝐺)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | dvcosax 42091* | Derivative exercise: the derivative with respect to x of cos(Ax), given a constant 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ ℂ ↦ (cos‘(𝐴 · 𝑥)))) = (𝑥 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑥))))) | ||
Theorem | dvdivcncf 42092 | A sufficient condition for the derivative of a quotient to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) & ⊢ (𝜑 → 𝐺:𝑋⟶(ℂ ∖ {0})) & ⊢ (𝜑 → (𝑆 D 𝐹) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑆 D 𝐺) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑆 D (𝐹 ∘f / 𝐺)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | dvbdfbdioolem1 42093* | Given a function with bounded derivative, on an open interval, here is an absolute bound to the difference of the image of two points in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐾 ∈ ℝ) & ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)𝐵)) ⇒ ⊢ (𝜑 → ((abs‘((𝐹‘𝐷) − (𝐹‘𝐶))) ≤ (𝐾 · (𝐷 − 𝐶)) ∧ (abs‘((𝐹‘𝐷) − (𝐹‘𝐶))) ≤ (𝐾 · (𝐵 − 𝐴)))) | ||
Theorem | dvbdfbdioolem2 42094* | A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐾 ∈ ℝ) & ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾) & ⊢ 𝑀 = ((abs‘(𝐹‘((𝐴 + 𝐵) / 2))) + (𝐾 · (𝐵 − 𝐴))) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑀) | ||
Theorem | dvbdfbdioo 42095* | A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑎) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) | ||
Theorem | ioodvbdlimc1lem1 42096* | If 𝐹 has bounded derivative on (𝐴(,)𝐵) then a sequence of points in its image converges to its lim sup. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑅:(ℤ≥‘𝑀)⟶(𝐴(,)𝐵)) & ⊢ 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) & ⊢ (𝜑 → 𝑅 ∈ dom ⇝ ) & ⊢ 𝐾 = inf({𝑘 ∈ (ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆)) | ||
Theorem | ioodvbdlimc1lem2 42097* | Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) & ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) & ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1) & ⊢ 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) & ⊢ 𝑅 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) & ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) ⇒ ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 limℂ 𝐴)) | ||
Theorem | ioodvbdlimc1 42098* | A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐴) ≠ ∅) | ||
Theorem | ioodvbdlimc2lem 42099* | Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) & ⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) & ⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1) & ⊢ 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) & ⊢ 𝑅 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐵 − (1 / 𝑗))) & ⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) ⇒ ⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 limℂ 𝐵)) | ||
Theorem | ioodvbdlimc2 42100* | A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) ≠ ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |