Theorem List for Intuitionistic Logic Explorer - 8501-8600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ngtmnft 8501 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (A ∈ ℝ* → (A = -∞ ↔ ¬ -∞ < A)) |
|
Theorem | xrrebnd 8502 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (A ∈ ℝ* → (A ∈ ℝ
↔ (-∞ < A ∧ A <
+∞))) |
|
Theorem | xrre 8503 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧
(-∞ < A ∧ A ≤
B)) → A ∈
ℝ) |
|
Theorem | xrre2 8504 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) ∧ (A < B ∧ B < 𝐶)) → B ∈
ℝ) |
|
Theorem | xrre3 8505 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧
(B ≤ A ∧ A < +∞)) → A ∈
ℝ) |
|
Theorem | ge0gtmnf 8506 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ 0 ≤ A)
→ -∞ < A) |
|
Theorem | ge0nemnf 8507 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ 0 ≤ A)
→ A ≠ -∞) |
|
Theorem | xrrege0 8508 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (0
≤ A ∧
A ≤ B)) → A
∈ ℝ) |
|
Theorem | z2ge 8509* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → ∃𝑘 ∈ ℤ
(𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) |
|
Theorem | xnegeq 8510 |
Equality of two extended numbers with -𝑒 in front of them.
(Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro,
20-Aug-2015.)
|
⊢ (A =
B → -𝑒A = -𝑒B) |
|
Theorem | xnegpnf 8511 |
Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒+∞ =
-∞ |
|
Theorem | xnegmnf 8512 |
Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒-∞ =
+∞ |
|
Theorem | rexneg 8513 |
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|
⊢ (A ∈ ℝ → -𝑒A = -A) |
|
Theorem | xneg0 8514 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒0 = 0 |
|
Theorem | xnegcl 8515 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (A ∈ ℝ* →
-𝑒A ∈ ℝ*) |
|
Theorem | xnegneg 8516 |
Extended real version of negneg 7057. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (A ∈ ℝ* →
-𝑒-𝑒A = A) |
|
Theorem | xneg11 8517 |
Extended real version of neg11 7058. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) →
(-𝑒A =
-𝑒B ↔ A = B)) |
|
Theorem | xltnegi 8518 |
Forward direction of xltneg 8519. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A <
B) → -𝑒B < -𝑒A) |
|
Theorem | xltneg 8519 |
Extended real version of ltneg 7252. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔
-𝑒B <
-𝑒A)) |
|
Theorem | xleneg 8520 |
Extended real version of leneg 7255. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A ≤ B ↔
-𝑒B ≤
-𝑒A)) |
|
Theorem | xlt0neg1 8521 |
Extended real version of lt0neg1 7258. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (A ∈ ℝ* → (A < 0 ↔ 0 <
-𝑒A)) |
|
Theorem | xlt0neg2 8522 |
Extended real version of lt0neg2 7259. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (A ∈ ℝ* → (0 < A ↔ -𝑒A < 0)) |
|
Theorem | xle0neg1 8523 |
Extended real version of le0neg1 7260. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (A ∈ ℝ* → (A ≤ 0 ↔ 0 ≤
-𝑒A)) |
|
Theorem | xle0neg2 8524 |
Extended real version of le0neg2 7261. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (A ∈ ℝ* → (0 ≤ A ↔ -𝑒A ≤ 0)) |
|
Theorem | xnegcld 8525 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ*)
⇒ ⊢ (φ → -𝑒A ∈
ℝ*) |
|
Theorem | xrex 8526 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
⊢ ℝ* ∈ V |
|
3.5.3 Real number intervals
|
|
Syntax | cioo 8527 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 8528 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 8529 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 8530 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 8531* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
⊢ (,) = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x < z ∧ z <
y)}) |
|
Definition | df-ioc 8532* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ (,] = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x < z ∧ z ≤
y)}) |
|
Definition | df-ico 8533* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ [,) = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x ≤ z ∧ z <
y)}) |
|
Definition | df-icc 8534* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
⊢ [,] = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x ≤ z ∧ z ≤
y)}) |
|
Theorem | ixxval 8535* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)}) ⇒ ⊢ ((A ∈
ℝ* ∧ B ∈
ℝ*) → (A𝑂B) = {z ∈ ℝ* ∣ (A𝑅z ∧ z𝑆B)}) |
|
Theorem | elixx1 8536* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)}) ⇒ ⊢ ((A ∈
ℝ* ∧ B ∈
ℝ*) → (𝐶 ∈
(A𝑂B)
↔ (𝐶 ∈ ℝ* ∧ A𝑅𝐶 ∧ 𝐶𝑆B))) |
|
Theorem | ixxf 8537* |
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.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)}) ⇒ ⊢ 𝑂:(ℝ* ×
ℝ*)⟶𝒫 ℝ* |
|
Theorem | ixxex 8538* |
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)}) ⇒ ⊢ 𝑂 ∈
V |
|
Theorem | ixxssxr 8539* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)}) ⇒ ⊢ (A𝑂B)
⊆ ℝ* |
|
Theorem | elixx3g 8540* |
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
A ∈ ℝ* and B ∈ ℝ*. (Contributed by
Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)}) ⇒ ⊢ (𝐶 ∈
(A𝑂B)
↔ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) ∧ (A𝑅𝐶 ∧ 𝐶𝑆B))) |
|
Theorem | ixxssixx 8541* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})
& ⊢ 𝑃 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑈y)})
& ⊢ ((A ∈ ℝ* ∧ w ∈ ℝ*) → (A𝑅w
→ A𝑇w))
& ⊢ ((w ∈ ℝ* ∧ B ∈ ℝ*) → (w𝑆B
→ w𝑈B)) ⇒ ⊢ (A𝑂B)
⊆ (A𝑃B) |
|
Theorem | ixxdisj 8542* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})
& ⊢ 𝑃 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑈y)})
& ⊢ ((B ∈ ℝ* ∧ w ∈ ℝ*) → (B𝑇w
↔ ¬ w𝑆B)) ⇒ ⊢ ((A ∈
ℝ* ∧ B ∈
ℝ* ∧ 𝐶 ∈
ℝ*) → ((A𝑂B) ∩ (B𝑃𝐶)) = ∅) |
|
Theorem | ixxss1 8543* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})
& ⊢ 𝑃 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑆y)})
& ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ w ∈ ℝ*) → ((A𝑊B ∧ B𝑇w) → A𝑅w)) ⇒ ⊢ ((A ∈
ℝ* ∧ A𝑊B)
→ (B𝑃𝐶) ⊆ (A𝑂𝐶)) |
|
Theorem | ixxss2 8544* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})
& ⊢ 𝑃 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑇y)})
& ⊢ ((w ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → ((w𝑇B ∧ B𝑊𝐶) → w𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈
ℝ* ∧ B𝑊𝐶) → (A𝑃B)
⊆ (A𝑂𝐶)) |
|
Theorem | ixxss12 8545* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})
& ⊢ 𝑃 = (x
∈ ℝ*, y ∈
ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑈y)})
& ⊢ ((A ∈ ℝ* ∧ 𝐶 ∈
ℝ* ∧ w ∈
ℝ*) → ((A𝑊𝐶 ∧ 𝐶𝑇w)
→ A𝑅w))
& ⊢ ((w ∈ ℝ* ∧ 𝐷 ∈
ℝ* ∧ B ∈
ℝ*) → ((w𝑈𝐷 ∧ 𝐷𝑋B)
→ w𝑆B)) ⇒ ⊢ (((A ∈
ℝ* ∧ B ∈
ℝ*) ∧ (A𝑊𝐶 ∧ 𝐷𝑋B))
→ (𝐶𝑃𝐷) ⊆ (A𝑂B)) |
|
Theorem | iooex 8546 |
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 8547* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,)B) =
{x ∈
ℝ* ∣ (A <
x ∧
x < B)}) |
|
Theorem | iooidg 8548 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
⊢ (A ∈ ℝ* → (A(,)A) =
∅) |
|
Theorem | elioo3g 8549 |
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
A ∈ ℝ* and B ∈ ℝ*. (Contributed by NM,
24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝐶 ∈
(A(,)B) ↔ ((A
∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) ∧ (A < 𝐶 ∧ 𝐶 < B))) |
|
Theorem | elioo1 8550 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈
(A(,)B) ↔ (𝐶 ∈
ℝ* ∧ A < 𝐶 ∧ 𝐶 < B))) |
|
Theorem | elioore 8551 |
A member of an open interval of reals is a real. (Contributed by NM,
17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (A ∈ (B(,)𝐶) → A ∈
ℝ) |
|
Theorem | lbioog 8552 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ A ∈ (A(,)B)) |
|
Theorem | ubioog 8553 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ B ∈ (A(,)B)) |
|
Theorem | iooval2 8554* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,)B) =
{x ∈
ℝ ∣ (A < x ∧ x < B)}) |
|
Theorem | iooss1 8555 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((A ∈ ℝ* ∧ A ≤
B) → (B(,)𝐶) ⊆ (A(,)𝐶)) |
|
Theorem | iooss2 8556 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐶 ∈
ℝ* ∧ B ≤ 𝐶) → (A(,)B) ⊆
(A(,)𝐶)) |
|
Theorem | iocval 8557* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,]B) =
{x ∈
ℝ* ∣ (A <
x ∧
x ≤ B)}) |
|
Theorem | icoval 8558* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A[,)B) =
{x ∈
ℝ* ∣ (A ≤
x ∧
x < B)}) |
|
Theorem | iccval 8559* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A[,]B) =
{x ∈
ℝ* ∣ (A ≤
x ∧
x ≤ B)}) |
|
Theorem | elioo2 8560 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈
(A(,)B) ↔ (𝐶 ∈
ℝ ∧ A < 𝐶 ∧ 𝐶 < B))) |
|
Theorem | elioc1 8561 |
Membership in an open-below, closed-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈
(A(,]B) ↔ (𝐶 ∈
ℝ* ∧ A < 𝐶 ∧ 𝐶 ≤ B))) |
|
Theorem | elico1 8562 |
Membership in a closed-below, open-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈
(A[,)B) ↔ (𝐶 ∈
ℝ* ∧ A ≤ 𝐶 ∧ 𝐶 < B))) |
|
Theorem | elicc1 8563 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈
(A[,]B) ↔ (𝐶 ∈
ℝ* ∧ A ≤ 𝐶 ∧ 𝐶 ≤ B))) |
|
Theorem | iccid 8564 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
⊢ (A ∈ ℝ* → (A[,]A) =
{A}) |
|
Theorem | icc0r 8565 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (B < A →
(A[,]B) = ∅)) |
|
Theorem | eliooxr 8566 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
⊢ (A ∈ (B(,)𝐶) → (B ∈
ℝ* ∧ 𝐶 ∈
ℝ*)) |
|
Theorem | eliooord 8567 |
Ordering implied by a member of an open interval of reals. (Contributed
by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|
⊢ (A ∈ (B(,)𝐶) → (B < A ∧ A < 𝐶)) |
|
Theorem | ubioc1 8568 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 8623. (Contributed by FL, 29-May-2014.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A <
B) → B ∈ (A(,]B)) |
|
Theorem | lbico1 8569 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 8622. (Contributed by FL, 29-May-2014.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A <
B) → A ∈ (A[,)B)) |
|
Theorem | iccleub 8570 |
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14-Jul-2009.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
(A[,]B)) → 𝐶 ≤ B) |
|
Theorem | iccgelb 8571 |
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23-Dec-2016.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
(A[,]B)) → A
≤ 𝐶) |
|
Theorem | elioo5 8572 |
Membership in an open interval of extended reals. (Contributed by NM,
17-Aug-2008.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → (𝐶 ∈
(A(,)B) ↔ (A
< 𝐶 ∧ 𝐶 < B))) |
|
Theorem | elioo4g 8573 |
Membership in an open interval of extended reals. (Contributed by NM,
8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ (𝐶 ∈
(A(,)B) ↔ ((A
∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ) ∧ (A < 𝐶 ∧ 𝐶 < B))) |
|
Theorem | ioossre 8574 |
An open interval is a set of reals. (Contributed by NM,
31-May-2007.)
|
⊢ (A(,)B) ⊆
ℝ |
|
Theorem | elioc2 8575 |
Membership in an open-below, closed-above real interval. (Contributed
by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro,
14-Jun-2014.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ) → (𝐶 ∈
(A(,]B) ↔ (𝐶 ∈
ℝ ∧ A < 𝐶 ∧ 𝐶 ≤ B))) |
|
Theorem | elico2 8576 |
Membership in a closed-below, open-above real interval. (Contributed by
Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro,
14-Jun-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ*) → (𝐶 ∈
(A[,)B) ↔ (𝐶 ∈
ℝ ∧ A ≤ 𝐶 ∧ 𝐶 < B))) |
|
Theorem | elicc2 8577 |
Membership in a closed real interval. (Contributed by Paul Chapman,
21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (𝐶 ∈ (A[,]B) ↔
(𝐶 ∈ ℝ ∧
A ≤ 𝐶 ∧ 𝐶 ≤ B))) |
|
Theorem | elicc2i 8578 |
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3-Jun-2013.)
|
⊢ A ∈ ℝ & ⊢ B ∈
ℝ ⇒ ⊢ (𝐶 ∈
(A[,]B) ↔ (𝐶 ∈
ℝ ∧ A ≤ 𝐶 ∧ 𝐶 ≤ B)) |
|
Theorem | elicc4 8579 |
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → (𝐶 ∈
(A[,]B) ↔ (A
≤ 𝐶 ∧ 𝐶 ≤ B))) |
|
Theorem | iccss 8580 |
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 20-Feb-2015.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (A ≤ 𝐶 ∧ 𝐷 ≤ B)) → (𝐶[,]𝐷) ⊆ (A[,]B)) |
|
Theorem | iccssioo 8581 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A < 𝐶 ∧ 𝐷 < B)) → (𝐶[,]𝐷) ⊆ (A(,)B)) |
|
Theorem | icossico 8582 |
Condition for a closed-below, open-above interval to be a subset of a
closed-below, open-above interval. (Contributed by Thierry Arnoux,
21-Sep-2017.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A ≤ 𝐶 ∧ 𝐷 ≤ B)) → (𝐶[,)𝐷) ⊆ (A[,)B)) |
|
Theorem | iccss2 8583 |
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 28-Apr-2015.)
|
⊢ ((𝐶 ∈
(A[,]B) ∧ 𝐷 ∈ (A[,]B)) →
(𝐶[,]𝐷) ⊆ (A[,]B)) |
|
Theorem | iccssico 8584 |
Condition for a closed interval to be a subset of a half-open interval.
(Contributed by Mario Carneiro, 9-Sep-2015.)
|
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A ≤ 𝐶 ∧ 𝐷 < B)) → (𝐶[,]𝐷) ⊆ (A[,)B)) |
|
Theorem | iccssioo2 8585 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐶 ∈
(A(,)B) ∧ 𝐷 ∈ (A(,)B)) →
(𝐶[,]𝐷) ⊆ (A(,)B)) |
|
Theorem | iccssico2 8586 |
Condition for a closed interval to be a subset of a closed-below,
open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐶 ∈
(A[,)B) ∧ 𝐷 ∈ (A[,)B)) →
(𝐶[,]𝐷) ⊆ (A[,)B)) |
|
Theorem | ioomax 8587 |
The open interval from minus to plus infinity. (Contributed by NM,
6-Feb-2007.)
|
⊢ (-∞(,)+∞) =
ℝ |
|
Theorem | iccmax 8588 |
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4-Jul-2014.)
|
⊢ (-∞[,]+∞) =
ℝ* |
|
Theorem | ioopos 8589 |
The set of positive reals expressed as an open interval. (Contributed by
NM, 7-May-2007.)
|
⊢ (0(,)+∞) = {x ∈ ℝ
∣ 0 < x} |
|
Theorem | ioorp 8590 |
The set of positive reals expressed as an open interval. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
⊢ (0(,)+∞) =
ℝ+ |
|
Theorem | iooshf 8591 |
Shift the arguments of the open interval function. (Contributed by NM,
17-Aug-2008.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈
ℝ ∧ 𝐷 ∈
ℝ)) → ((A − B) ∈ (𝐶(,)𝐷) ↔ A ∈ ((𝐶 + B)(,)(𝐷 + B)))) |
|
Theorem | iocssre 8592 |
A closed-above interval with real upper bound is a set of reals.
(Contributed by FL, 29-May-2014.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ) → (A(,]B) ⊆
ℝ) |
|
Theorem | icossre 8593 |
A closed-below interval with real lower bound is a set of reals.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ*) → (A[,)B) ⊆ ℝ) |
|
Theorem | iccssre 8594 |
A closed real interval is a set of reals. (Contributed by FL,
6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A[,]B) ⊆ ℝ) |
|
Theorem | iccssxr 8595 |
A closed interval is a set of extended reals. (Contributed by FL,
28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|
⊢ (A[,]B) ⊆
ℝ* |
|
Theorem | iocssxr 8596 |
An open-below, closed-above interval is a subset of the extended reals.
(Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro,
4-Jul-2014.)
|
⊢ (A(,]B) ⊆
ℝ* |
|
Theorem | icossxr 8597 |
A closed-below, open-above interval is a subset of the extended reals.
(Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro,
4-Jul-2014.)
|
⊢ (A[,)B) ⊆
ℝ* |
|
Theorem | ioossicc 8598 |
An open interval is a subset of its closure. (Contributed by Paul
Chapman, 18-Oct-2007.)
|
⊢ (A(,)B) ⊆
(A[,]B) |
|
Theorem | icossicc 8599 |
A closed-below, open-above interval is a subset of its closure.
(Contributed by Thierry Arnoux, 25-Oct-2016.)
|
⊢ (A[,)B) ⊆
(A[,]B) |
|
Theorem | iocssicc 8600 |
A closed-above, open-below interval is a subset of its closure.
(Contributed by Thierry Arnoux, 1-Apr-2017.)
|
⊢ (A(,]B) ⊆
(A[,]B) |