Theorem List for Intuitionistic Logic Explorer - 9901-10000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xaddcld 9901 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈
ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
|
Theorem | xadd4d 9902 |
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 8143. (Contributed by Alexander van der Vekens,
21-Dec-2017.)
|
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) & ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) & ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) & ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠
-∞)) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) |
|
Theorem | xnn0add4d 9903 |
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9902. (Contributed by AV,
12-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐵 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐶 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐷 ∈
ℕ0*) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) |
|
Theorem | xleaddadd 9904 |
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 9905 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 9906 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 9907 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 9908 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 9909* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-ioc 9910* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Definition | df-ico 9911* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-icc 9912* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Theorem | ixxval 9913* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) |
|
Theorem | elixx1 9914* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) |
|
Theorem | ixxf 9915* |
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 9916* |
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 9917* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆
ℝ* |
|
Theorem | elixx3g 9918* |
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 9919* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) |
|
Theorem | ixxdisj 9920* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) |
|
Theorem | ixxss1 9921* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss2 9922* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss12 9923* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) |
|
Theorem | iooex 9924 |
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 9925* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooidg 9926 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅) |
|
Theorem | elioo3g 9927 |
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 9928 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioore 9929 |
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 9930 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐴 ∈
(𝐴(,)𝐵)) |
|
Theorem | ubioog 9931 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐵 ∈
(𝐴(,)𝐵)) |
|
Theorem | iooval2 9932* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooss1 9933 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iooss2 9934 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iocval 9935* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | icoval 9936* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iccval 9937* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | elioo2 9938 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioc1 9939 |
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 9940 |
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 9941 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | iccid 9942 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) |
|
Theorem | icc0r 9943 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐵 < 𝐴 → (𝐴[,]𝐵) = ∅)) |
|
Theorem | eliooxr 9944 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈
ℝ*)) |
|
Theorem | eliooord 9945 |
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 9946 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 10002. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) |
|
Theorem | lbico1 9947 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 10001. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) |
|
Theorem | iccleub 9948 |
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14-Jul-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |
|
Theorem | iccgelb 9949 |
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23-Dec-2016.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
|
Theorem | elioo5 9950 |
Membership in an open interval of extended reals. (Contributed by NM,
17-Aug-2008.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioo4g 9951 |
Membership in an open interval of extended reals. (Contributed by NM,
8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | ioossre 9952 |
An open interval is a set of reals. (Contributed by NM,
31-May-2007.)
|
⊢ (𝐴(,)𝐵) ⊆ ℝ |
|
Theorem | elioc2 9953 |
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 9954 |
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 9955 |
Membership in a closed real interval. (Contributed by Paul Chapman,
21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | elicc2i 9956 |
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3-Jun-2013.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
|
Theorem | elicc4 9957 |
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | iccss 9958 |
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 9959 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 < 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | icossico 9960 |
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 9961 |
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 9962 |
Condition for a closed interval to be a subset of a half-open interval.
(Contributed by Mario Carneiro, 9-Sep-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) |
|
Theorem | iccssioo2 9963 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | iccssico2 9964 |
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 9965 |
The open interval from minus to plus infinity. (Contributed by NM,
6-Feb-2007.)
|
⊢ (-∞(,)+∞) =
ℝ |
|
Theorem | iccmax 9966 |
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4-Jul-2014.)
|
⊢ (-∞[,]+∞) =
ℝ* |
|
Theorem | ioopos 9967 |
The set of positive reals expressed as an open interval. (Contributed by
NM, 7-May-2007.)
|
⊢ (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥} |
|
Theorem | ioorp 9968 |
The set of positive reals expressed as an open interval. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
⊢ (0(,)+∞) =
ℝ+ |
|
Theorem | iooshf 9969 |
Shift the arguments of the open interval function. (Contributed by NM,
17-Aug-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐵) ∈ (𝐶(,)𝐷) ↔ 𝐴 ∈ ((𝐶 + 𝐵)(,)(𝐷 + 𝐵)))) |
|
Theorem | iocssre 9970 |
A closed-above interval with real upper bound is a set of reals.
(Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) |
|
Theorem | icossre 9971 |
A closed-below interval with real lower bound is a set of reals.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ) |
|
Theorem | iccssre 9972 |
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 9973 |
A closed interval is a set of extended reals. (Contributed by FL,
28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|
⊢ (𝐴[,]𝐵) ⊆
ℝ* |
|
Theorem | iocssxr 9974 |
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 9975 |
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 9976 |
An open interval is a subset of its closure. (Contributed by Paul
Chapman, 18-Oct-2007.)
|
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
|
Theorem | icossicc 9977 |
A closed-below, open-above interval is a subset of its closure.
(Contributed by Thierry Arnoux, 25-Oct-2016.)
|
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
|
Theorem | iocssicc 9978 |
A closed-above, open-below interval is a subset of its closure.
(Contributed by Thierry Arnoux, 1-Apr-2017.)
|
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) |
|
Theorem | ioossico 9979 |
An open interval is a subset of its closure-below. (Contributed by
Thierry Arnoux, 3-Mar-2017.)
|
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵) |
|
Theorem | iocssioo 9980 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | icossioo 9981 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | ioossioo 9982 |
Condition for an open interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 26-Sep-2017.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) |
|
Theorem | iccsupr 9983* |
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 9984 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))) |
|
Theorem | elioomnf 9985 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))) |
|
Theorem | elicopnf 9986 |
Membership in a closed unbounded interval of reals. (Contributed by
Mario Carneiro, 16-Sep-2014.)
|
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵))) |
|
Theorem | repos 9987 |
Two ways of saying that a real number is positive. (Contributed by NM,
7-May-2007.)
|
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | ioof 9988 |
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 9989 |
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 9990 |
The union of the range of the open interval function. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|
⊢ ℝ = ∪ ran
(,) |
|
Theorem | dfioo2 9991* |
Alternate definition of the set of open intervals of extended reals.
(Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro,
1-Sep-2015.)
|
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑤 ∈ ℝ
∣ (𝑥 < 𝑤 ∧ 𝑤 < 𝑦)}) |
|
Theorem | ioorebasg 9992 |
Open intervals are elements of the set of all open intervals.
(Contributed by Jim Kingdon, 4-Apr-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) ∈ ran
(,)) |
|
Theorem | elrege0 9993 |
The predicate "is a nonnegative real". (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
|
⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
|
Theorem | rge0ssre 9994 |
Nonnegative real numbers are real numbers. (Contributed by Thierry
Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
|
⊢ (0[,)+∞) ⊆
ℝ |
|
Theorem | elxrge0 9995 |
Elementhood in the set of nonnegative extended reals. (Contributed by
Mario Carneiro, 28-Jun-2014.)
|
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴)) |
|
Theorem | 0e0icopnf 9996 |
0 is a member of (0[,)+∞) (common case).
(Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ∈ (0[,)+∞) |
|
Theorem | 0e0iccpnf 9997 |
0 is a member of (0[,]+∞) (common case).
(Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ∈ (0[,]+∞) |
|
Theorem | ge0addcl 9998 |
The nonnegative reals are closed under addition. (Contributed by Mario
Carneiro, 19-Jun-2014.)
|
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) →
(𝐴 + 𝐵) ∈ (0[,)+∞)) |
|
Theorem | ge0mulcl 9999 |
The nonnegative reals are closed under multiplication. (Contributed by
Mario Carneiro, 19-Jun-2014.)
|
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) →
(𝐴 · 𝐵) ∈
(0[,)+∞)) |
|
Theorem | ge0xaddcl 10000 |
The nonnegative reals are closed under addition. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) →
(𝐴 +𝑒
𝐵) ∈
(0[,]+∞)) |