Theorem List for Intuitionistic Logic Explorer - 8701-8800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xrltnr 8701 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 < 𝐴) |
|
Theorem | ltpnf 8702 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
|
Theorem | 0ltpnf 8703 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 < +∞ |
|
Theorem | mnflt 8704 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) |
|
Theorem | mnflt0 8705 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ -∞ < 0 |
|
Theorem | mnfltpnf 8706 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ -∞ < +∞ |
|
Theorem | mnfltxr 8707 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴) |
|
Theorem | pnfnlt 8708 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
+∞ < 𝐴) |
|
Theorem | nltmnf 8709 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 <
-∞) |
|
Theorem | pnfge 8710 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤
+∞) |
|
Theorem | 0lepnf 8711 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 ≤ +∞ |
|
Theorem | nn0pnfge0 8712 |
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 ≤
𝑁) |
|
Theorem | mnfle 8713 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → -∞
≤ 𝐴) |
|
Theorem | xrltnsym 8714 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
|
Theorem | xrltnsym2 8715 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | xrlttr 8716 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltso 8717 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
⊢ < Or
ℝ* |
|
Theorem | xrlttri3 8718 |
Extended real version of lttri3 7098. (Contributed by NM, 9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | xrltle 8719 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
|
Theorem | xrleid 8720 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) |
|
Theorem | xrletri3 8721 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | xrlelttr 8722 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltletr 8723 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrletr 8724 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | xrlttrd 8725 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrlelttrd 8726 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrltletrd 8727 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrletrd 8728 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | xrltne 8729 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) |
|
Theorem | nltpnft 8730 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 <
+∞)) |
|
Theorem | ngtmnft 8731 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬
-∞ < 𝐴)) |
|
Theorem | xrrebnd 8732 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔
(-∞ < 𝐴 ∧
𝐴 <
+∞))) |
|
Theorem | xrre 8733 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧
(-∞ < 𝐴 ∧
𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
|
Theorem | xrre2 8734 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) |
|
Theorem | xrre3 8735 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) |
|
Theorem | ge0gtmnf 8736 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → -∞ <
𝐴) |
|
Theorem | ge0nemnf 8737 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ≠
-∞) |
|
Theorem | xrrege0 8738 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
|
Theorem | z2ge 8739* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) |
|
Theorem | xnegeq 8740 |
Equality of two extended numbers with -𝑒 in front of them.
(Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵) |
|
Theorem | xnegpnf 8741 |
Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒+∞ =
-∞ |
|
Theorem | xnegmnf 8742 |
Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒-∞ =
+∞ |
|
Theorem | rexneg 8743 |
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴 =
-𝐴) |
|
Theorem | xneg0 8744 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒0 = 0 |
|
Theorem | xnegcl 8745 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒𝐴
∈ ℝ*) |
|
Theorem | xnegneg 8746 |
Extended real version of negneg 7261. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒-𝑒𝐴 = 𝐴) |
|
Theorem | xneg11 8747 |
Extended real version of neg11 7262. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | xltnegi 8748 |
Forward direction of xltneg 8749. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵
< -𝑒𝐴) |
|
Theorem | xltneg 8749 |
Extended real version of ltneg 7457. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔
-𝑒𝐵
< -𝑒𝐴)) |
|
Theorem | xleneg 8750 |
Extended real version of leneg 7460. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔
-𝑒𝐵
≤ -𝑒𝐴)) |
|
Theorem | xlt0neg1 8751 |
Extended real version of lt0neg1 7463. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 <
-𝑒𝐴)) |
|
Theorem | xlt0neg2 8752 |
Extended real version of lt0neg2 7464. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 <
𝐴 ↔
-𝑒𝐴
< 0)) |
|
Theorem | xle0neg1 8753 |
Extended real version of le0neg1 7465. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤
-𝑒𝐴)) |
|
Theorem | xle0neg2 8754 |
Extended real version of le0neg2 7466. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 ≤
𝐴 ↔
-𝑒𝐴
≤ 0)) |
|
Theorem | xnegcld 8755 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ*) ⇒ ⊢ (𝜑 → -𝑒𝐴 ∈
ℝ*) |
|
Theorem | xrex 8756 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
⊢ ℝ* ∈
V |
|
3.5.3 Real number intervals
|
|
Syntax | cioo 8757 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 8758 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 8759 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 8760 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 8761* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-ioc 8762* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Definition | df-ico 8763* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-icc 8764* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Theorem | ixxval 8765* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) |
|
Theorem | elixx1 8766* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) |
|
Theorem | ixxf 8767* |
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.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ 𝑂:(ℝ* ×
ℝ*)⟶𝒫 ℝ* |
|
Theorem | ixxex 8768* |
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ 𝑂 ∈ V |
|
Theorem | ixxssxr 8769* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆
ℝ* |
|
Theorem | elixx3g 8770* |
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.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐶 ∈ (𝐴𝑂𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) |
|
Theorem | ixxssixx 8771* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) |
|
Theorem | ixxdisj 8772* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) |
|
Theorem | ixxss1 8773* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss2 8774* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss12 8775* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) |
|
Theorem | iooex 8776 |
The set of open intervals of extended reals exists. (Contributed by NM,
6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (,) ∈ V |
|
Theorem | iooval 8777* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooidg 8778 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅) |
|
Theorem | elioo3g 8779 |
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.)
|
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioo1 8780 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioore 8781 |
A member of an open interval of reals is a real. (Contributed by NM,
17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ) |
|
Theorem | lbioog 8782 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐴 ∈
(𝐴(,)𝐵)) |
|
Theorem | ubioog 8783 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐵 ∈
(𝐴(,)𝐵)) |
|
Theorem | iooval2 8784* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooss1 8785 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iooss2 8786 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iocval 8787* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | icoval 8788* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iccval 8789* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | elioo2 8790 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioc1 8791 |
Membership in an open-below, closed-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | elico1 8792 |
Membership in a closed-below, open-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elicc1 8793 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | iccid 8794 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) |
|
Theorem | icc0r 8795 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐵 < 𝐴 → (𝐴[,]𝐵) = ∅)) |
|
Theorem | eliooxr 8796 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈
ℝ*)) |
|
Theorem | eliooord 8797 |
Ordering implied by a member of an open interval of reals. (Contributed
by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
|
Theorem | ubioc1 8798 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 8853. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) |
|
Theorem | lbico1 8799 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 8852. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) |
|
Theorem | iccleub 8800 |
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14-Jul-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |