![]() |
Metamath
Proof Explorer Theorem List (p. 456 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elioored 45501 | A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵(,)𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | ioogtlbd 45502 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | ioofun 45503 | (,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Fun (,) | ||
Theorem | icomnfinre 45504 | A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((-∞[,)𝐴) ∩ ℝ) = (-∞(,)𝐴)) | ||
Theorem | sqrlearg 45505 | The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 ↔ 𝐴 ∈ (0[,]1))) | ||
Theorem | ressiocsup 45506 | If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑆 = sup(𝐴, ℝ*, < ) & ⊢ (𝜑 → 𝑆 ∈ 𝐴) & ⊢ 𝐼 = (-∞(,]𝑆) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐼) | ||
Theorem | ressioosup 45507 | If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑆 = sup(𝐴, ℝ*, < ) & ⊢ (𝜑 → ¬ 𝑆 ∈ 𝐴) & ⊢ 𝐼 = (-∞(,)𝑆) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐼) | ||
Theorem | iooiinioc 45508* | A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) = (𝐴(,]𝐵)) | ||
Theorem | ressiooinf 45509 | If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑆 = inf(𝐴, ℝ*, < ) & ⊢ (𝜑 → ¬ 𝑆 ∈ 𝐴) & ⊢ 𝐼 = (𝑆(,)+∞) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐼) | ||
Theorem | icogelbd 45510 | An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
Theorem | iocleubd 45511 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵)) ⇒ ⊢ (𝜑 → 𝐶 ≤ 𝐵) | ||
Theorem | uzinico 45512 | An upper interval of integers is the intersection of the integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑍 = (ℤ ∩ (𝑀[,)+∞))) | ||
Theorem | preimaiocmnf 45513* | Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≤ 𝐵}) | ||
Theorem | uzinico2 45514 | An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (ℤ≥‘𝑁) = ((ℤ≥‘𝑀) ∩ (𝑁[,)+∞))) | ||
Theorem | uzinico3 45515 | An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑍 = (𝑍 ∩ (𝑀[,)+∞))) | ||
Theorem | icossico2 45516 | Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐴[,)𝐶) ⊆ (𝐵[,)𝐶)) | ||
Theorem | dmico 45517 | The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ dom [,) = (ℝ* × ℝ*) | ||
Theorem | ndmico 45518 | The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (¬ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ∅) | ||
Theorem | uzubioo 45519* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (𝑋(,)+∞)𝑘 ∈ 𝑍) | ||
Theorem | uzubico 45520* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (𝑋[,)+∞)𝑘 ∈ 𝑍) | ||
Theorem | uzubioo2 45521* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑘 ∈ (𝑥(,)+∞)𝑘 ∈ 𝑍) | ||
Theorem | uzubico2 45522* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑘 ∈ (𝑥[,)+∞)𝑘 ∈ 𝑍) | ||
Theorem | iocgtlbd 45523 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵)) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrtgioo2 45524 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to ℝ. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t ℝ) | ||
Theorem | tgioo4 45525 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ) | ||
Theorem | fsummulc1f 45526* | Closure of a finite sum of complex numbers 𝐴(𝑘). A version of fsummulc1 15817 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)) | ||
Theorem | fsumnncl 45527* | Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ) | ||
Theorem | fsumge0cl 45528* | The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
Theorem | fsumf1of 45529* | Re-index a finite sum using a bijection. Same as fsumf1o 15755, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) | ||
Theorem | fsumiunss 45530* | Sum over a disjoint indexed union, intersected with a finite set 𝐷. Similar to fsumiun 15853, but here 𝐴 and 𝐵 need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ Fin) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐷)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐷) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝐷)𝐶) | ||
Theorem | fsumreclf 45531* | Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) | ||
Theorem | fsumlessf 45532* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | fsumsupp0 45533* | Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝐹 supp 0)(𝐹‘𝑘) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) | ||
Theorem | fsumsermpt 45534* | A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐴) & ⊢ 𝐺 = seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | fmul01 45535* | 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 45536* | 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 45537* | induction step for the proof of fmuldfeq 45538. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑓𝜑 & ⊢ Ⅎ𝑔𝜑 & ⊢ Ⅎ𝑡𝑌 & ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) & ⊢ (𝜑 → 𝑇 ∈ V) & ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) & ⊢ (𝜑 → 𝑁 ∈ (1...𝑀)) & ⊢ (𝜑 → (𝑁 + 1) ∈ (1...𝑀)) & ⊢ (𝜑 → ((seq1(𝑃, 𝑈)‘𝑁)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑁)) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑁 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑁 + 1))) | ||
Theorem | fmuldfeq 45538* | 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 45539* | Given a finite multiplication of values between 0 and 1, a value larger than its first element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑖𝐵 & ⊢ Ⅎ𝑖𝜑 & ⊢ 𝐴 = seq𝐿( · , 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐵‘𝐿) < 𝐸) ⇒ ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸) | ||
Theorem | fmul01lt1lem2 45540* | Given a finite multiplication of values between 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 45541* | Given a finite multiplication of values between 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 45542* | A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ (𝐶–cn→𝐵)) | ||
Theorem | rrpsscn 45543 | The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ℝ+ ⊆ ℂ | ||
Theorem | mulc1cncfg 45544* | A version of mulc1cncf 24944 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (𝐹‘𝑥))) ∈ (𝐴–cn→ℂ)) | ||
Theorem | infrglb 45545* | 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 45546* | If 𝐹 is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 24966. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)↑𝑁)) ∈ (𝐴–cn→ℂ)) | ||
Theorem | prodeq2ad 45547* | Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | fprodsplit1 45548* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (𝐷 · ∏𝑘 ∈ (𝐴 ∖ {𝐶})𝐵)) | ||
Theorem | fprodexp 45549* | Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵↑𝑁) = (∏𝑘 ∈ 𝐴 𝐵↑𝑁)) | ||
Theorem | fprodabs2 45550* | The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘∏𝑘 ∈ 𝐴 𝐵) = ∏𝑘 ∈ 𝐴 (abs‘𝐵)) | ||
Theorem | fprod0 45551* | A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐶 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 = 0) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0) | ||
Theorem | mccllem 45552* | * Induction step for mccl 45553. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m (𝐶 ∪ {𝐷}))) & ⊢ (𝜑 → ∀𝑏 ∈ (ℕ0 ↑m 𝐶)((!‘Σ𝑘 ∈ 𝐶 (𝑏‘𝑘)) / ∏𝑘 ∈ 𝐶 (!‘(𝑏‘𝑘))) ∈ ℕ) ⇒ ⊢ (𝜑 → ((!‘Σ𝑘 ∈ (𝐶 ∪ {𝐷})(𝐵‘𝑘)) / ∏𝑘 ∈ (𝐶 ∪ {𝐷})(!‘(𝐵‘𝑘))) ∈ ℕ) | ||
Theorem | mccl 45553* | A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m 𝐴)) ⇒ ⊢ (𝜑 → ((!‘Σ𝑘 ∈ 𝐴 (𝐵‘𝑘)) / ∏𝑘 ∈ 𝐴 (!‘(𝐵‘𝑘))) ∈ ℕ) | ||
Theorem | fprodcnlem 45554* | A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.) Avoid ax-mulf 11232. (Revised by GG, 19-Apr-2025.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ (𝐴 ∖ 𝑍)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝑍 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ (𝑍 ∪ {𝑊})𝐵) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | fprodcn 45555* | 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 45556* | A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴 · 𝑛) + 𝐵) / (𝐴 · 𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
Theorem | isumneg 45557* | Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 -𝐴 = -Σ𝑘 ∈ 𝑍 𝐴) | ||
Theorem | climrec 45558* | Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘))) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴)) | ||
Theorem | climmulf 45559* | A version of climmul 15665 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵)) | ||
Theorem | climexp 45560* | The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘)↑𝑁)) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴↑𝑁)) | ||
Theorem | climinf 45561* | A bounded monotonic nonincreasing 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 45562* | The subsequence index 𝐼 has the expected properties: it belongs to the same upper integers as the original index, and it is always greater than or equal to the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1))) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐼‘𝐾) ∈ (ℤ≥‘𝐾)) | ||
Theorem | climsuse 45563* | 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 45564* | A version of climrec 45558 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘))) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴)) | ||
Theorem | climneg 45565* | Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) ⇝ -𝐴) | ||
Theorem | climinff 45566* | A version of climinf 45561 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 45567* | Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0})) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 / 𝐵)) | ||
Theorem | climreeq 45568 | 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 45569* | 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 45570* | A version of climadd 15664 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ Ⅎ𝑘𝐻 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 + 𝐵)) | ||
Theorem | mullimc 45571* | Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | ellimcabssub0 45572* | An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ 0 ∈ (𝐺 limℂ 𝐷))) | ||
Theorem | limcdm0 45573 | If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:∅⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ℂ) | ||
Theorem | islptre 45574* | 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 45575 | 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 25942 and limccnp 25940, here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ran 𝐹 ⊆ (dom 𝐺 ∖ {𝐵})) & ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐵)) ⇒ ⊢ (𝜑 → 𝐶 ∈ ((𝐺 ∘ 𝐹) limℂ 𝐴)) | ||
Theorem | limciccioolb 45576 | 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 45577* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 15526, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | mullimcf 45578* | Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℂ) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) & ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | constlimc 45579* | Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐶)) | ||
Theorem | rexlim2d 45580* | Inference removing two restricted quantifiers. Same as rexlimdvv 3209, but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | idlimc 45581* | Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥) & ⊢ (𝜑 → 𝑋 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋)) | ||
Theorem | divcnvg 45582* | The sequence of reciprocals of positive integers, multiplied by the factor 𝐴, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑛 ∈ (ℤ≥‘𝑀) ↦ (𝐴 / 𝑛)) ⇝ 0) | ||
Theorem | limcperiod 45583* | 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 45584 | 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 45585* | 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 45586 | 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 45587 | 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 45588 | A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐵) → 𝐴 = 𝐶) | ||
Theorem | elprn2 45589 | A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐶) → 𝐴 = 𝐵) | ||
Theorem | limcmptdm 45590* | The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℂ) | ||
Theorem | clim2f 45591* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15526. Similar to clim2 15536, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | limcicciooub 45592 | 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 45593 | A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,)𝐴)) ⇒ ⊢ (𝜑 → (𝐶 mod 𝐵) < (𝐴 mod 𝐵)) | ||
Theorem | islpcn 45594* | 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 45595* | 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 45596* | 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 45597 | 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 45598 | 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 45599 | 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 45600 | 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‘𝐽)‘(𝐴(,)𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |