Home | Metamath
Proof Explorer Theorem List (p. 417 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 | infxrpnf 41601 | Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∪ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < )) | ||
Theorem | infxrrnmptcl 41602* | The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ∈ ℝ*) | ||
Theorem | leneg2d 41603 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) | ||
Theorem | supxrltinfxr 41604 | The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ sup(∅, ℝ*, < ) < inf(∅, ℝ*, < ) | ||
Theorem | max1d 41605 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | ceilcld 41606 | Closure of the ceiling function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (⌈‘𝐴) ∈ ℤ) | ||
Theorem | supxrleubrnmptf 41607 | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | nleltd 41608 | 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | zxrd 41609 | An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | infxrgelbrnmpt 41610* | The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐶 ≤ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵)) | ||
Theorem | rphalfltd 41611 | Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 2) < 𝐴) | ||
Theorem | uzssz2 41612 | An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℤ | ||
Theorem | leneg3d 41613 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) | ||
Theorem | max2d 41614 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | uzn0bi 41615 | The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((ℤ≥‘𝑀) ≠ ∅ ↔ 𝑀 ∈ ℤ) | ||
Theorem | xnegrecl2 41616 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((𝐴 ∈ ℝ* ∧ -𝑒𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) | ||
Theorem | nfxneg 41617 | Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥-𝑒𝐴 | ||
Theorem | uzxrd 41618 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | infxrpnf2 41619 | Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∖ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < )) | ||
Theorem | supminfxr 41620* | The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = -𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ*, < )) | ||
Theorem | infrpgernmpt 41621* | The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐵 ≤ (inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) +𝑒 𝐶)) | ||
Theorem | xnegre 41622 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ -𝑒𝐴 ∈ ℝ)) | ||
Theorem | xnegrecl2d 41623 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | uzxr 41624 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ (ℤ≥‘𝑀) → 𝐴 ∈ ℝ*) | ||
Theorem | supminfxr2 41625* | The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = -𝑒inf({𝑥 ∈ ℝ* ∣ -𝑒𝑥 ∈ 𝐴}, ℝ*, < )) | ||
Theorem | xnegred 41626 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ↔ -𝑒𝐴 ∈ ℝ)) | ||
Theorem | supminfxrrnmpt 41627* | The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -𝑒inf(ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵), ℝ*, < )) | ||
Theorem | min1d 41628 | The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
Theorem | min2d 41629 | The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
Theorem | pnfged 41630 | Plus infinity is an upper bound for extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ +∞) | ||
Theorem | xrnpnfmnf 41631 | An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ +∞) ⇒ ⊢ (𝜑 → 𝐴 = -∞) | ||
Theorem | uzsscn 41632 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (ℤ≥‘𝑀) ⊆ ℂ | ||
Theorem | absimnre 41633 | The absolute value of the imaginary part of a non-real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+) | ||
Theorem | uzsscn2 41634 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℂ | ||
Theorem | xrtgcntopre 41635 | The standard topologies on the extended reals and on the complex numbers, coincide when restricted to the reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ ((ordTop‘ ≤ ) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ) | ||
Theorem | absimlere 41636 | The absolute value of the imaginary part of a complex number is a lower bound of the distance to any real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝐵 − 𝐴))) | ||
Theorem | rpssxr 41637 | The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ ℝ+ ⊆ ℝ* | ||
Theorem | monoordxrv 41638* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁)) | ||
Theorem | monoordxr 41639* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁)) | ||
Theorem | monoord2xrv 41640* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) | ||
Theorem | monoord2xr 41641* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) | ||
Theorem | xrpnf 41642* | An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴)) | ||
Theorem | xlenegcon1 41643 | Extended real version of lenegcon1 11133. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ 𝐴)) | ||
Theorem | xlenegcon2 41644 | Extended real version of lenegcon2 11134. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ -𝑒𝐵 ↔ 𝐵 ≤ -𝑒𝐴)) | ||
Theorem | gtnelioc 41645 | A real number larger than the upper bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | ioossioc 41646 | An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵) | ||
Theorem | ioondisj2 41647 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅) | ||
Theorem | ioondisj1 41648 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅) | ||
Theorem | ioosscn 41649 | An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴(,)𝐵) ⊆ ℂ | ||
Theorem | ioogtlb 41650 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝐶) | ||
Theorem | evthiccabs 41651* | Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑤)))) | ||
Theorem | ltnelicc 41652 | A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 < 𝐴) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | eliood 41653 | Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) | ||
Theorem | iooabslt 41654 | An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − 𝐵)(,)(𝐴 + 𝐵))) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < 𝐵) | ||
Theorem | gtnelicc 41655 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | iooinlbub 41656 | An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅ | ||
Theorem | iocgtlb 41657 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐶) | ||
Theorem | iocleub 41658 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ≤ 𝐵) | ||
Theorem | eliccd 41659 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | iccssred 41660 | A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | ||
Theorem | eliccre 41661 | A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | eliooshift 41662 | Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)(,)(𝐶 + 𝐷)))) | ||
Theorem | eliocd 41663 | Membership in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | icoltub 41664 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵) | ||
Theorem | eliocre 41665 | A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | iooltub 41666 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵) | ||
Theorem | ioontr 41667 | The interior of an interval in the standard topology on ℝ is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵) | ||
Theorem | snunioo1 41668 | The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵)) | ||
Theorem | lbioc 41669 | A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ¬ 𝐴 ∈ (𝐴(,]𝐵) | ||
Theorem | ioomidp 41670 | The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) | ||
Theorem | iccdifioo 41671 | If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,]𝐵) ∖ (𝐴(,)𝐵)) = {𝐴, 𝐵}) | ||
Theorem | iccdifprioo 41672 | An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) ∖ {𝐴, 𝐵}) = (𝐴(,)𝐵)) | ||
Theorem | ioossioobi 41673 | Biconditional form of ioossioo 12819. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → ((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵))) | ||
Theorem | iccshift 41674* | A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) | ||
Theorem | iccsuble 41675 | An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵)) ⇒ ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐵 − 𝐴)) | ||
Theorem | iocopn 41676 | A left-open right-closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝐽 = (𝐾 ↾t (𝐴(,]𝐵)) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶(,]𝐵) ∈ 𝐽) | ||
Theorem | eliccelioc 41677 | Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐶 ≠ 𝐴))) | ||
Theorem | iooshift 41678* | An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝑇)(,)(𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴(,)𝐵)𝑤 = (𝑧 + 𝑇)}) | ||
Theorem | iccintsng 41679 | Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) = {𝐵}) | ||
Theorem | icoiccdif 41680 | Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵})) | ||
Theorem | icoopn 41681 | A left-closed right-open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝐽 = (𝐾 ↾t (𝐴[,)𝐵)) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴[,)𝐶) ∈ 𝐽) | ||
Theorem | icoub 41682 | A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ ℝ* → ¬ 𝐵 ∈ (𝐴[,)𝐵)) | ||
Theorem | eliccxrd 41683 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | pnfel0pnf 41684 | +∞ is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ +∞ ∈ (0[,]+∞) | ||
Theorem | eliccnelico 41685 | An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,)𝐵)) ⇒ ⊢ (𝜑 → 𝐶 = 𝐵) | ||
Theorem | eliccelicod 41686 | A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) | ||
Theorem | ge0xrre 41687 | A nonnegative extended real that is not +∞ is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐴 ≠ +∞) → 𝐴 ∈ ℝ) | ||
Theorem | ge0lere 41688 | A nonnegative extended Real number smaller than or equal to a Real number, is a Real number. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ ℝ) | ||
Theorem | elicores 41689* | Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦)) | ||
Theorem | inficc 41690 | The infimum of a nonempty set, included in a closed interval, is a member of the interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝑆 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑆 ≠ ∅) ⇒ ⊢ (𝜑 → inf(𝑆, ℝ*, < ) ∈ (𝐴[,]𝐵)) | ||
Theorem | qinioo 41691 | The rational numbers are dense in ℝ. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((ℚ ∩ (𝐴(,)𝐵)) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | lenelioc 41692 | A real number smaller than or equal to the lower bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ≤ 𝐴) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | ioonct 41693 | A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝐶 = (𝐴(,)𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ≼ ω) | ||
Theorem | xrgtnelicc 41694 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | iccdificc 41695 | The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶)) | ||
Theorem | iocnct 41696 | A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝐶 = (𝐴(,]𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ≼ ω) | ||
Theorem | iccnct 41697 | A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝐶 = (𝐴[,]𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ≼ ω) | ||
Theorem | iooiinicc 41698* | A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ ((𝐴 − (1 / 𝑛))(,)(𝐵 + (1 / 𝑛))) = (𝐴[,]𝐵)) | ||
Theorem | iccgelbd 41699 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
Theorem | iooltubd 41700 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) ⇒ ⊢ (𝜑 → 𝐶 < 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |