HomeHome Intuitionistic Logic Explorer
Theorem List (p. 89 of 105)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8801-8900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremxrltnr 8801 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)
 
Theoremltpnf 8802 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → 𝐴 < +∞)
 
Theorem0ltpnf 8803 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 < +∞
 
Theoremmnflt 8804 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → -∞ < 𝐴)
 
Theoremmnflt0 8805 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ < 0
 
Theoremmnfltpnf 8806 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
-∞ < +∞
 
Theoremmnfltxr 8807 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴)
 
Theorempnfnlt 8808 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
 
Theoremnltmnf 8809 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
 
Theorempnfge 8810 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ*𝐴 ≤ +∞)
 
Theorem0lepnf 8811 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
0 ≤ +∞
 
Theoremnn0pnfge0 8812 If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
((𝑁 ∈ ℕ0𝑁 = +∞) → 0 ≤ 𝑁)
 
Theoremmnfle 8813 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
(𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
 
Theoremxrltnsym 8814 Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
 
Theoremxrltnsym2 8815 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵𝐵 < 𝐴))
 
Theoremxrlttr 8816 Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremxrltso 8817 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
< Or ℝ*
 
Theoremxrlttri3 8818 Extended real version of lttri3 7156. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
 
Theoremxrltle 8819 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴𝐵))
 
Theoremxrleid 8820 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
(𝐴 ∈ ℝ*𝐴𝐴)
 
Theoremxrletri3 8821 Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
 
Theoremxrlelttr 8822 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremxrltletr 8823 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
 
Theoremxrletr 8824 Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 
Theoremxrlttrd 8825 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)
 
Theoremxrlelttrd 8826 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)
 
Theoremxrltletrd 8827 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴 < 𝐶)
 
Theoremxrletrd 8828 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremxrltne 8829 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵𝐴)
 
Theoremnltpnft 8830 An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))
 
Theoremngtmnft 8831 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
(𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
 
Theoremxrrebnd 8832 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
(𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))
 
Theoremxrre 8833 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)
 
Theoremxrre2 8834 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵𝐵 < 𝐶)) → 𝐵 ∈ ℝ)
 
Theoremxrre3 8835 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐵𝐴𝐴 < +∞)) → 𝐴 ∈ ℝ)
 
Theoremge0gtmnf 8836 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
 
Theoremge0nemnf 8837 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞)
 
Theoremxrrege0 8838 A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)
 
Theoremz2ge 8839* There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀𝑘𝑁𝑘))
 
Theoremxnegeq 8840 Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
 
Theoremxnegpnf 8841 Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
-𝑒+∞ = -∞
 
Theoremxnegmnf 8842 Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
-𝑒-∞ = +∞
 
Theoremrexneg 8843 Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
 
Theoremxneg0 8844 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
-𝑒0 = 0
 
Theoremxnegcl 8845 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*)
 
Theoremxnegneg 8846 Extended real version of negneg 7323. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴)
 
Theoremxneg11 8847 Extended real version of neg11 7324. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵𝐴 = 𝐵))
 
Theoremxltnegi 8848 Forward direction of xltneg 8849. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴)
 
Theoremxltneg 8849 Extended real version of ltneg 7530. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴))
 
Theoremxleneg 8850 Extended real version of leneg 7533. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴))
 
Theoremxlt0neg1 8851 Extended real version of lt0neg1 7536. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴))
 
Theoremxlt0neg2 8852 Extended real version of lt0neg2 7537. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0))
 
Theoremxle0neg1 8853 Extended real version of le0neg1 7538. (Contributed by Mario Carneiro, 9-Sep-2015.)
(𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴))
 
Theoremxle0neg2 8854 Extended real version of le0neg2 7539. (Contributed by Mario Carneiro, 9-Sep-2015.)
(𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0))
 
Theoremxnegcld 8855 Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ*)       (𝜑 → -𝑒𝐴 ∈ ℝ*)
 
Theoremxrex 8856 The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
* ∈ V
 
3.5.3  Real number intervals
 
Syntaxcioo 8857 Extend class notation with the set of open intervals of extended reals.
class (,)
 
Syntaxcioc 8858 Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
 
Syntaxcico 8859 Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
 
Syntaxcicc 8860 Extend class notation with the set of closed intervals of extended reals.
class [,]
 
Definitiondf-ioo 8861* Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
 
Definitiondf-ioc 8862* Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
 
Definitiondf-ico 8863* Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
 
Definitiondf-icc 8864* Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
 
Theoremixxval 8865* Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧𝑧𝑆𝐵)})
 
Theoremelixx1 8866* Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝑅𝐶𝐶𝑆𝐵)))
 
Theoremixxf 8867* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ*
 
Theoremixxex 8868* The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       𝑂 ∈ V
 
Theoremixxssxr 8869* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       (𝐴𝑂𝐵) ⊆ ℝ*
 
Theoremelixx3g 8870* Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show 𝐴 ∈ ℝ* and 𝐵 ∈ ℝ*. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       (𝐶 ∈ (𝐴𝑂𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑅𝐶𝐶𝑆𝐵)))
 
Theoremixxssixx 8871* An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})    &   ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐴𝑅𝑤𝐴𝑇𝑤))    &   ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑤𝑆𝐵𝑤𝑈𝐵))       (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵)
 
Theoremixxdisj 8872* Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})    &   ((𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵))       ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅)
 
Theoremixxss1 8873* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑆𝑦)})    &   ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵𝐵𝑇𝑤) → 𝐴𝑅𝑤))       ((𝐴 ∈ ℝ*𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶))
 
Theoremixxss2 8874* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑇𝑦)})    &   ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵𝐵𝑊𝐶) → 𝑤𝑆𝐶))       ((𝐶 ∈ ℝ*𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶))
 
Theoremixxss12 8875* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})    &   ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶𝐶𝑇𝑤) → 𝐴𝑅𝑤))    &   ((𝑤 ∈ ℝ*𝐷 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷𝐷𝑋𝐵) → 𝑤𝑆𝐵))       (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵))
 
Theoremiooex 8876 The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
(,) ∈ V
 
Theoremiooval 8877* Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥𝑥 < 𝐵)})
 
Theoremiooidg 8878 An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
(𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅)
 
Theoremelioo3g 8879 Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show 𝐴 ∈ ℝ* and 𝐵 ∈ ℝ*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
(𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶𝐶 < 𝐵)))
 
Theoremelioo1 8880 Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶 < 𝐵)))
 
Theoremelioore 8881 A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
(𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)
 
Theoremlbioog 8882 An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ¬ 𝐴 ∈ (𝐴(,)𝐵))
 
Theoremubioog 8883 An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ¬ 𝐵 ∈ (𝐴(,)𝐵))
 
Theoremiooval2 8884* Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥𝑥 < 𝐵)})
 
Theoremiooss1 8885 Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
((𝐴 ∈ ℝ*𝐴𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶))
 
Theoremiooss2 8886 Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐶 ∈ ℝ*𝐵𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶))
 
Theoremiocval 8887* Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥𝑥𝐵)})
 
Theoremicoval 8888* Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴𝑥𝑥 < 𝐵)})
 
Theoremiccval 8889* Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴𝑥𝑥𝐵)})
 
Theoremelioo2 8890 Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶 < 𝐵)))
 
Theoremelioc1 8891 Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵)))
 
Theoremelico1 8892 Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶 < 𝐵)))
 
Theoremelicc1 8893 Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵)))
 
Theoremiccid 8894 A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.)
(𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴})
 
Theoremicc0r 8895 An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 < 𝐴 → (𝐴[,]𝐵) = ∅))
 
Theoremeliooxr 8896 An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
(𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ*𝐶 ∈ ℝ*))
 
Theoremeliooord 8897 Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
(𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴𝐴 < 𝐶))
 
Theoremubioc1 8898 The upper bound belongs to an open-below, closed-above interval. See ubicc2 8953. (Contributed by FL, 29-May-2014.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
 
Theoremlbico1 8899 The lower bound belongs to a closed-below, open-above interval. See lbicc2 8952. (Contributed by FL, 29-May-2014.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
 
Theoremiccleub 8900 An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐶𝐵)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10490
  Copyright terms: Public domain < Previous  Next >