Theorem List for Intuitionistic Logic Explorer - 9801-9900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xleadd2a 9801 |
Commuted form of xleadd1a 9800. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵)) |
|
Theorem | xleadd1 9802 |
Weakened version of xleadd1a 9800 under which the reverse implication is
true. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))) |
|
Theorem | xltadd1 9803 |
Extended real version of ltadd1 8318. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))) |
|
Theorem | xltadd2 9804 |
Extended real version of ltadd2 8308. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵))) |
|
Theorem | xaddge0 9805 |
The sum of nonnegative extended reals is nonnegative. (Contributed by
Mario Carneiro, 21-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (0 ≤ 𝐴 ∧ 0
≤ 𝐵)) → 0 ≤
(𝐴 +𝑒
𝐵)) |
|
Theorem | xle2add 9806 |
Extended real version of le2add 8333. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐷 ∈ ℝ*)) →
((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷))) |
|
Theorem | xlt2add 9807 |
Extended real version of lt2add 8334. Note that ltleadd 8335, which has
weaker assumptions, is not true for the extended reals (since
0 + +∞ < 1 + +∞ fails).
(Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐷 ∈ ℝ*)) →
((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))) |
|
Theorem | xsubge0 9808 |
Extended real version of subge0 8364. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) |
|
Theorem | xposdif 9809 |
Extended real version of posdif 8344. (Contributed by Mario Carneiro,
24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒
-𝑒𝐴))) |
|
Theorem | xlesubadd 9810 |
Under certain conditions, the conclusion of lesubadd 8323 is true even in the
extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒
-𝑒𝐵)
≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵))) |
|
Theorem | xaddcld 9811 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈
ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
|
Theorem | xadd4d 9812 |
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 8058. (Contributed by Alexander van der Vekens,
21-Dec-2017.)
|
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) & ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) & ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) & ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠
-∞)) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) |
|
Theorem | xnn0add4d 9813 |
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9812. (Contributed by AV,
12-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐵 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐶 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐷 ∈
ℕ0*) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) |
|
Theorem | xleaddadd 9814 |
Cancelling a factor of two in ≤ (expressed as
addition rather than
as a factor to avoid extended real multiplication). (Contributed by Jim
Kingdon, 18-Apr-2023.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐴) ≤ (𝐵 +𝑒 𝐵))) |
|
4.5.3 Real number intervals
|
|
Syntax | cioo 9815 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 9816 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 9817 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 9818 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 9819* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-ioc 9820* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Definition | df-ico 9821* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-icc 9822* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Theorem | ixxval 9823* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) |
|
Theorem | elixx1 9824* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) |
|
Theorem | ixxf 9825* |
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 9826* |
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 9827* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆
ℝ* |
|
Theorem | elixx3g 9828* |
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 9829* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) |
|
Theorem | ixxdisj 9830* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) |
|
Theorem | ixxss1 9831* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss2 9832* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss12 9833* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) |
|
Theorem | iooex 9834 |
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 9835* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooidg 9836 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅) |
|
Theorem | elioo3g 9837 |
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 9838 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioore 9839 |
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 9840 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐴 ∈
(𝐴(,)𝐵)) |
|
Theorem | ubioog 9841 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐵 ∈
(𝐴(,)𝐵)) |
|
Theorem | iooval2 9842* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooss1 9843 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iooss2 9844 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iocval 9845* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | icoval 9846* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iccval 9847* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | elioo2 9848 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioc1 9849 |
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 9850 |
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 9851 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | iccid 9852 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) |
|
Theorem | icc0r 9853 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐵 < 𝐴 → (𝐴[,]𝐵) = ∅)) |
|
Theorem | eliooxr 9854 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈
ℝ*)) |
|
Theorem | eliooord 9855 |
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 9856 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 9912. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) |
|
Theorem | lbico1 9857 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 9911. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) |
|
Theorem | iccleub 9858 |
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14-Jul-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |
|
Theorem | iccgelb 9859 |
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23-Dec-2016.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
|
Theorem | elioo5 9860 |
Membership in an open interval of extended reals. (Contributed by NM,
17-Aug-2008.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioo4g 9861 |
Membership in an open interval of extended reals. (Contributed by NM,
8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | ioossre 9862 |
An open interval is a set of reals. (Contributed by NM,
31-May-2007.)
|
⊢ (𝐴(,)𝐵) ⊆ ℝ |
|
Theorem | elioc2 9863 |
Membership in an open-below, closed-above real interval. (Contributed by
Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | elico2 9864 |
Membership in a closed-below, open-above real interval. (Contributed by
Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elicc2 9865 |
Membership in a closed real interval. (Contributed by Paul Chapman,
21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | elicc2i 9866 |
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3-Jun-2013.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
|
Theorem | elicc4 9867 |
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | iccss 9868 |
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.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,]𝐵)) |
|
Theorem | iccssioo 9869 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 < 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | icossico 9870 |
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.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴[,)𝐵)) |
|
Theorem | iccss2 9871 |
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.)
|
⊢ ((𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐷 ∈ (𝐴[,]𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,]𝐵)) |
|
Theorem | iccssico 9872 |
Condition for a closed interval to be a subset of a half-open interval.
(Contributed by Mario Carneiro, 9-Sep-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) |
|
Theorem | iccssioo2 9873 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | iccssico2 9874 |
Condition for a closed interval to be a subset of a closed-below,
open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐶 ∈ (𝐴[,)𝐵) ∧ 𝐷 ∈ (𝐴[,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) |
|
Theorem | ioomax 9875 |
The open interval from minus to plus infinity. (Contributed by NM,
6-Feb-2007.)
|
⊢ (-∞(,)+∞) =
ℝ |
|
Theorem | iccmax 9876 |
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4-Jul-2014.)
|
⊢ (-∞[,]+∞) =
ℝ* |
|
Theorem | ioopos 9877 |
The set of positive reals expressed as an open interval. (Contributed by
NM, 7-May-2007.)
|
⊢ (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥} |
|
Theorem | ioorp 9878 |
The set of positive reals expressed as an open interval. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
⊢ (0(,)+∞) =
ℝ+ |
|
Theorem | iooshf 9879 |
Shift the arguments of the open interval function. (Contributed by NM,
17-Aug-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐵) ∈ (𝐶(,)𝐷) ↔ 𝐴 ∈ ((𝐶 + 𝐵)(,)(𝐷 + 𝐵)))) |
|
Theorem | iocssre 9880 |
A closed-above interval with real upper bound is a set of reals.
(Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) |
|
Theorem | icossre 9881 |
A closed-below interval with real lower bound is a set of reals.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ) |
|
Theorem | iccssre 9882 |
A closed real interval is a set of reals. (Contributed by FL,
6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
|
Theorem | iccssxr 9883 |
A closed interval is a set of extended reals. (Contributed by FL,
28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|
⊢ (𝐴[,]𝐵) ⊆
ℝ* |
|
Theorem | iocssxr 9884 |
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.)
|
⊢ (𝐴(,]𝐵) ⊆
ℝ* |
|
Theorem | icossxr 9885 |
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.)
|
⊢ (𝐴[,)𝐵) ⊆
ℝ* |
|
Theorem | ioossicc 9886 |
An open interval is a subset of its closure. (Contributed by Paul
Chapman, 18-Oct-2007.)
|
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
|
Theorem | icossicc 9887 |
A closed-below, open-above interval is a subset of its closure.
(Contributed by Thierry Arnoux, 25-Oct-2016.)
|
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
|
Theorem | iocssicc 9888 |
A closed-above, open-below interval is a subset of its closure.
(Contributed by Thierry Arnoux, 1-Apr-2017.)
|
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) |
|
Theorem | ioossico 9889 |
An open interval is a subset of its closure-below. (Contributed by
Thierry Arnoux, 3-Mar-2017.)
|
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵) |
|
Theorem | iocssioo 9890 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | icossioo 9891 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | ioossioo 9892 |
Condition for an open interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 26-Sep-2017.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | iccsupr 9893* |
A nonempty subset of a closed real interval satisfies the conditions for
the existence of its supremum. To be useful without excluded middle,
we'll probably need to change not equal to apart, and perhaps make other
changes, but the theorem does hold as stated here. (Contributed by Paul
Chapman, 21-Jan-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
|
Theorem | elioopnf 9894 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))) |
|
Theorem | elioomnf 9895 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))) |
|
Theorem | elicopnf 9896 |
Membership in a closed unbounded interval of reals. (Contributed by
Mario Carneiro, 16-Sep-2014.)
|
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵))) |
|
Theorem | repos 9897 |
Two ways of saying that a real number is positive. (Contributed by NM,
7-May-2007.)
|
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | ioof 9898 |
The set of open intervals of extended reals maps to subsets of reals.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
16-Nov-2013.)
|
⊢ (,):(ℝ* ×
ℝ*)⟶𝒫 ℝ |
|
Theorem | iccf 9899 |
The set of closed intervals of extended reals maps to subsets of
extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario
Carneiro, 3-Nov-2013.)
|
⊢ [,]:(ℝ* ×
ℝ*)⟶𝒫 ℝ* |
|
Theorem | unirnioo 9900 |
The union of the range of the open interval function. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|
⊢ ℝ = ∪ ran
(,) |