Home | Metamath
Proof Explorer Theorem List (p. 399 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsumclf 39801* | Closure of a finite sum of complex numbers 𝐴(𝑘). A version of fsumcl 14464 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | ||
Theorem | fsummulc1f 39802* | Closure of a finite sum of complex numbers 𝐴(𝑘). A version of fsummulc1 14517 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)) | ||
Theorem | fsumnncl 39803* | Closure of a non empty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ) | ||
Theorem | fsumsplit1 39804* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐷 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝑘 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (𝐷 + Σ𝑘 ∈ (𝐴 ∖ {𝐶})𝐵)) | ||
Theorem | fsumge0cl 39805* | The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
Theorem | fsumf1of 39806* | Re-index a finite sum using a bijection. Same as fsumf1o 14454, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) | ||
Theorem | fsumiunss 39807* | Sum over a disjoint indexed union, intersected with a finite set 𝐷. Similar to fsumiun 14553, but here 𝐴 and 𝐵 need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ Fin) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐷)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐷) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝐷)𝐶) | ||
Theorem | fsumreclf 39808* | Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) | ||
Theorem | fsumlessf 39809* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsumsupp0 39810* | Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝐹 supp 0)(𝐹‘𝑘) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) | ||
Theorem | fsumsermpt 39811* | A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐴) & ⊢ 𝐺 = seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | fmul01 39812* | Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑖𝐵 & ⊢ Ⅎ𝑖𝜑 & ⊢ 𝐴 = seq𝐿( · , 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿)) & ⊢ (𝜑 → 𝐾 ∈ (𝐿...𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) ⇒ ⊢ (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1)) | ||
Theorem | fmulcl 39813* | If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) & ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) & ⊢ (𝜑 → 𝑇 ∈ V) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑌) | ||
Theorem | fmuldfeqlem1 39814* | induction step for the proof of fmuldfeq 39815. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑓𝜑 & ⊢ Ⅎ𝑔𝜑 & ⊢ Ⅎ𝑡𝑌 & ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) & ⊢ (𝜑 → 𝑇 ∈ V) & ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) & ⊢ (𝜑 → 𝑁 ∈ (1...𝑀)) & ⊢ (𝜑 → (𝑁 + 1) ∈ (1...𝑀)) & ⊢ (𝜑 → ((seq1(𝑃, 𝑈)‘𝑁)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑁)) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑁 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑁 + 1))) | ||
Theorem | fmuldfeq 39815* | X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑖𝜑 & ⊢ Ⅎ𝑡𝑌 & ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) & ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) & ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀)) & ⊢ (𝜑 → 𝑇 ∈ V) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡)) | ||
Theorem | fmul01lt1lem1 39816* | Given a finite multiplication of values betweeen 0 and 1, a value larger than its frist element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑖𝐵 & ⊢ Ⅎ𝑖𝜑 & ⊢ 𝐴 = seq𝐿( · , 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐵‘𝐿) < 𝐸) ⇒ ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸) | ||
Theorem | fmul01lt1lem2 39817* | Given a finite multiplication of values betweeen 0 and 1, a value 𝐸 larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑖𝐵 & ⊢ Ⅎ𝑖𝜑 & ⊢ 𝐴 = seq𝐿( · , 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑀)) & ⊢ (𝜑 → (𝐵‘𝐽) < 𝐸) ⇒ ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸) | ||
Theorem | fmul01lt1 39818* | Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑖𝐵 & ⊢ Ⅎ𝑖𝜑 & ⊢ Ⅎ𝑗𝐴 & ⊢ 𝐴 = seq1( · , 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐵:(1...𝑀)⟶ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ (𝐵‘𝑖)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵‘𝑖) ≤ 1) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → ∃𝑗 ∈ (1...𝑀)(𝐵‘𝑗) < 𝐸) ⇒ ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸) | ||
Theorem | cncfmptss 39819* | A continuous complex function restricted to a subset is continuous, using "map to" notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ (𝐶–cn→𝐵)) | ||
Theorem | rrpsscn 39820 | The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ℝ+ ⊆ ℂ | ||
Theorem | mulc1cncfg 39821* | A version of mulc1cncf 22708 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (𝐹‘𝑥))) ∈ (𝐴–cn→ℂ)) | ||
Theorem | infrglb 39822* | The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐵 ∈ ℝ) → (inf(𝐴, ℝ, < ) < 𝐵 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝐵)) | ||
Theorem | expcnfg 39823* | If 𝐹 is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 22725. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)↑𝑁)) ∈ (𝐴–cn→ℂ)) | ||
Theorem | prodeq2ad 39824* | Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | fprodsplit1 39825* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (𝐷 · ∏𝑘 ∈ (𝐴 ∖ {𝐶})𝐵)) | ||
Theorem | fprodexp 39826* | Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵↑𝑁) = (∏𝑘 ∈ 𝐴 𝐵↑𝑁)) | ||
Theorem | fprodabs2 39827* | The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘∏𝑘 ∈ 𝐴 𝐵) = ∏𝑘 ∈ 𝐴 (abs‘𝐵)) | ||
Theorem | fprod0 39828* | A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐶 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 = 0) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0) | ||
Theorem | mccllem 39829* | * Induction step for mccl 39830. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑𝑚 (𝐶 ∪ {𝐷}))) & ⊢ (𝜑 → ∀𝑏 ∈ (ℕ0 ↑𝑚 𝐶)((!‘Σ𝑘 ∈ 𝐶 (𝑏‘𝑘)) / ∏𝑘 ∈ 𝐶 (!‘(𝑏‘𝑘))) ∈ ℕ) ⇒ ⊢ (𝜑 → ((!‘Σ𝑘 ∈ (𝐶 ∪ {𝐷})(𝐵‘𝑘)) / ∏𝑘 ∈ (𝐶 ∪ {𝐷})(!‘(𝐵‘𝑘))) ∈ ℕ) | ||
Theorem | mccl 39830* | A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑𝑚 𝐴)) ⇒ ⊢ (𝜑 → ((!‘Σ𝑘 ∈ 𝐴 (𝐵‘𝑘)) / ∏𝑘 ∈ 𝐴 (!‘(𝐵‘𝑘))) ∈ ℕ) | ||
Theorem | fprodcnlem 39831* | A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ (𝐴 ∖ 𝑍)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝑍 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ (𝑍 ∪ {𝑊})𝐵) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | fprodcn 39832* | A finite product 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 Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | clim1fr1 39833* | A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴 · 𝑛) + 𝐵) / (𝐴 · 𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
Theorem | isumneg 39834* | Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 -𝐴 = -Σ𝑘 ∈ 𝑍 𝐴) | ||
Theorem | climrec 39835* | Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘))) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴)) | ||
Theorem | climmulf 39836* | A version of climmul 14363 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵)) | ||
Theorem | climexp 39837* | The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘)↑𝑁)) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴↑𝑁)) | ||
Theorem | climinf 39838* | A bounded monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < )) | ||
Theorem | climsuselem1 39839* | The subsequence index 𝐼 has the expected properties: it belongs to the same upper integers as the original index, and it is always larger or equal than the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1))) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐼‘𝐾) ∈ (ℤ≥‘𝐾)) | ||
Theorem | climsuse 39840* | A subsequence 𝐺 of a converging sequence 𝐹, converges to the same limit. 𝐼 is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐼 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1))) & ⊢ (𝜑 → 𝐺 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐹‘(𝐼‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ 𝐴) | ||
Theorem | climrecf 39841* | A version of climrec 39835 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘))) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴)) | ||
Theorem | climneg 39842* | Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) ⇝ -𝐴) | ||
Theorem | climinff 39843* | A version of climinf 39838 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < )) | ||
Theorem | climdivf 39844* | Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 / 𝐵)) | ||
Theorem | climreeq 39845 | If 𝐹 is a real function, then 𝐹 converges to 𝐴 with respect to the standard topology on the reals if and only if it converges to 𝐴 with respect to the standard topology on complex numbers. In the theorem, 𝑅 is defined to be convergence w.r.t. the standard topology on the reals and then 𝐹𝑅𝐴 represents the statement "𝐹 converges to 𝐴, with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that 𝐴 is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.) |
⊢ 𝑅 = (⇝𝑡‘(topGen‘ran (,))) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹𝑅𝐴 ↔ 𝐹 ⇝ 𝐴)) | ||
Theorem | ellimciota 39846* | An explicit value for the limit, when the limit exists at a limit point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) & ⊢ (𝜑 → (𝐹 limℂ 𝐵) ≠ ∅) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → (℩𝑥𝑥 ∈ (𝐹 limℂ 𝐵)) ∈ (𝐹 limℂ 𝐵)) | ||
Theorem | climaddf 39847* | A version of climadd 14362 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 + 𝐵)) | ||
Theorem | mullimc 39848* | Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | ellimcabssub0 39849* | An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ 0 ∈ (𝐺 limℂ 𝐷))) | ||
Theorem | limcdm0 39850 | If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:∅⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ℂ) | ||
Theorem | islptre 39851* | An equivalence condition for a limit point w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) | ||
Theorem | limccog 39852 | Limit of the composition of two functions. If the limit of 𝐹 at 𝐴 is 𝐵 and the limit of 𝐺 at 𝐵 is 𝐶, then the limit of 𝐺 ∘ 𝐹 at 𝐴 is 𝐶. With respect to limcco 23657 and limccnp 23655, here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ran 𝐹 ⊆ (dom 𝐺 ∖ {𝐵})) & ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐵)) ⇒ ⊢ (𝜑 → 𝐶 ∈ ((𝐺 ∘ 𝐹) limℂ 𝐴)) | ||
Theorem | limciccioolb 39853 | The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴) = (𝐹 limℂ 𝐴)) | ||
Theorem | climf 39854* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 14225, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | mullimcf 39855* | Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℂ) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) & ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | constlimc 39856* | Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐶)) | ||
Theorem | rexlim2d 39857* | Inference removing two restricted quantifiers. Same as rexlimdvv 3037, but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | idlimc 39858* | Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥) & ⊢ (𝜑 → 𝑋 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋)) | ||
Theorem | divcnvg 39859* | The sequence of reciprocals of positive integers, multiplied by the factor 𝐴, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑛 ∈ (ℤ≥‘𝑀) ↦ (𝐴 / 𝑛)) ⇝ 0) | ||
Theorem | limcperiod 39860* | If 𝐹 is a periodic function with period 𝑇, the limit doesn't change if we shift the limiting point by 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} & ⊢ (𝜑 → 𝐵 ⊆ dom 𝐹) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) & ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝐷 + 𝑇))) | ||
Theorem | limcrecl 39861 | If 𝐹 is a real-valued function, 𝐵 is a limit point of its domain, and the limit of 𝐹 at 𝐵 exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘𝐴)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) ⇒ ⊢ (𝜑 → 𝐿 ∈ ℝ) | ||
Theorem | sumnnodd 39862* | A series indexed by ℕ with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵) ⇒ ⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))) | ||
Theorem | lptioo2 39863 | The upper bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | lptioo1 39864 | The lower bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | elprn1 39865 | A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐵) → 𝐴 = 𝐶) | ||
Theorem | elprn2 39866 | A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐶) → 𝐴 = 𝐵) | ||
Theorem | limcmptdm 39867* | The domain of a map-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℂ) | ||
Theorem | clim2f 39868* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 14225. Similar to clim2 14235, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | limcicciooub 39869 | The limit of a function at the upper bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐹 limℂ 𝐵)) | ||
Theorem | ltmod 39870 | A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,)𝐴)) ⇒ ⊢ (𝜑 → (𝐶 mod 𝐵) < (𝐴 mod 𝐵)) | ||
Theorem | islpcn 39871* | A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑃 ∈ ((limPt‘(TopOpen‘ℂfld))‘𝑆) ↔ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒)) | ||
Theorem | lptre2pt 39872* | If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → ((limPt‘𝐽)‘𝐴) ≠ ∅) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (abs‘(𝑥 − 𝑦)) < 𝐸)) | ||
Theorem | limsupre 39873* | If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.) |
⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → sup(𝐵, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹:𝐵⟶ℝ) & ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ) | ||
Theorem | limcresiooub 39874 | The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) | ||
Theorem | limcresioolb 39875 | The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵)) | ||
Theorem | limcleqr 39876 | If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) & ⊢ (𝜑 → 𝐿 = 𝑅) ⇒ ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) | ||
Theorem | lptioo2cn 39877 | The upper bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | lptioo1cn 39878 | The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | neglimc 39879* | Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) ⇒ ⊢ (𝜑 → -𝐶 ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | addlimc 39880* | Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | 0ellimcdiv 39881* | If the numerator converges to 0 and the denominator converges to non zero then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐸)) & ⊢ (𝜑 → 𝐷 ∈ (𝐺 limℂ 𝐸)) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → 0 ∈ (𝐻 limℂ 𝐸)) | ||
Theorem | clim2cf 39882* | Express the predicate 𝐹 converges to 𝐴. Similar to clim2 14235, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
Theorem | limclner 39883 | For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) & ⊢ (𝜑 → 𝐿 ≠ 𝑅) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅) | ||
Theorem | sublimc 39884* | Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 − 𝐼) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | reclimc 39885* | Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | clim0cf 39886* | Express the predicate 𝐹 converges to 0. Similar to clim 14225, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥)) | ||
Theorem | limclr 39887 | For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) ⇒ ⊢ (𝜑 → (((𝐹 limℂ 𝐵) ≠ ∅ ↔ 𝐿 = 𝑅) ∧ (𝐿 = 𝑅 → 𝐿 ∈ (𝐹 limℂ 𝐵)))) | ||
Theorem | divlimc 39888* | Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ≠ 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋 / 𝑌) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | expfac 39889* | Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0) | ||
Theorem | climconstmpt 39890* | A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐴) | ||
Theorem | climresmpt 39891* | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ 𝐺 = (𝑥 ∈ (ℤ≥‘𝑁) ↦ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵)) | ||
Theorem | climsubmpt 39892* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐷)) | ||
Theorem | climsubc2mpt 39893* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐵)) | ||
Theorem | climsubc1mpt 39894* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐴 − 𝐶)) | ||
Theorem | fnlimfv 39895* | The value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) | ||
Theorem | climreclf 39896* | The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | climeldmeq 39897* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ )) | ||
Theorem | climf2 39898* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 14225, but without the disjoint var constraint 𝜑𝑘 and 𝐹𝑘. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | fnlimcnv 39899* | The sequence of function values converges to the value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ (𝐺‘𝑋)) | ||
Theorem | climeldmeqmpt 39900* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |