Theorem List for Intuitionistic Logic Explorer - 9501-9600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xneg0 9501 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒0 = 0 |
|
Theorem | xnegcl 9502 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒𝐴
∈ ℝ*) |
|
Theorem | xnegneg 9503 |
Extended real version of negneg 7929. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒-𝑒𝐴 = 𝐴) |
|
Theorem | xneg11 9504 |
Extended real version of neg11 7930. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | xltnegi 9505 |
Forward direction of xltneg 9506. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵
< -𝑒𝐴) |
|
Theorem | xltneg 9506 |
Extended real version of ltneg 8137. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔
-𝑒𝐵
< -𝑒𝐴)) |
|
Theorem | xleneg 9507 |
Extended real version of leneg 8140. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔
-𝑒𝐵
≤ -𝑒𝐴)) |
|
Theorem | xlt0neg1 9508 |
Extended real version of lt0neg1 8143. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 <
-𝑒𝐴)) |
|
Theorem | xlt0neg2 9509 |
Extended real version of lt0neg2 8144. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 <
𝐴 ↔
-𝑒𝐴
< 0)) |
|
Theorem | xle0neg1 9510 |
Extended real version of le0neg1 8145. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤
-𝑒𝐴)) |
|
Theorem | xle0neg2 9511 |
Extended real version of le0neg2 8146. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 ≤
𝐴 ↔
-𝑒𝐴
≤ 0)) |
|
Theorem | xrpnfdc 9512 |
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* →
DECID 𝐴 =
+∞) |
|
Theorem | xrmnfdc 9513 |
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* →
DECID 𝐴 =
-∞) |
|
Theorem | xaddf 9514 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 21-Aug-2015.)
|
⊢ +𝑒 :(ℝ*
× ℝ*)⟶ℝ* |
|
Theorem | xaddval 9515 |
Value of the extended real addition operation. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞),
if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞),
if(𝐵 = +∞, +∞,
if(𝐵 = -∞, -∞,
(𝐴 + 𝐵)))))) |
|
Theorem | xaddpnf1 9516 |
Addition of positive infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒
+∞) = +∞) |
|
Theorem | xaddpnf2 9517 |
Addition of positive infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) →
(+∞ +𝑒 𝐴) = +∞) |
|
Theorem | xaddmnf1 9518 |
Addition of negative infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒
-∞) = -∞) |
|
Theorem | xaddmnf2 9519 |
Addition of negative infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) →
(-∞ +𝑒 𝐴) = -∞) |
|
Theorem | pnfaddmnf 9520 |
Addition of positive and negative infinity. This is often taken to be a
"null" value or out of the domain, but we define it (somewhat
arbitrarily)
to be zero so that the resulting function is total, which simplifies
proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (+∞ +𝑒 -∞) =
0 |
|
Theorem | mnfaddpnf 9521 |
Addition of negative and positive infinity. This is often taken to be a
"null" value or out of the domain, but we define it (somewhat
arbitrarily)
to be zero so that the resulting function is total, which simplifies
proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (-∞ +𝑒 +∞) =
0 |
|
Theorem | rexadd 9522 |
The extended real addition operation when both arguments are real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
|
Theorem | rexsub 9523 |
Extended real subtraction when both arguments are real. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒
-𝑒𝐵) =
(𝐴 − 𝐵)) |
|
Theorem | rexaddd 9524 |
The extended real addition operation when both arguments are real.
Deduction version of rexadd 9522. (Contributed by Glauco Siliprandi,
24-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
|
Theorem | xnegcld 9525 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ*) ⇒ ⊢ (𝜑 → -𝑒𝐴 ∈
ℝ*) |
|
Theorem | xrex 9526 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
⊢ ℝ* ∈
V |
|
Theorem | xaddnemnf 9527 |
Closure of extended real addition in the subset ℝ* / {-∞}.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞))
→ (𝐴
+𝑒 𝐵)
≠ -∞) |
|
Theorem | xaddnepnf 9528 |
Closure of extended real addition in the subset ℝ* / {+∞}.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞))
→ (𝐴
+𝑒 𝐵)
≠ +∞) |
|
Theorem | xnegid 9529 |
Extended real version of negid 7926. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒
-𝑒𝐴) =
0) |
|
Theorem | xaddcl 9530 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵)
∈ ℝ*) |
|
Theorem | xaddcom 9531 |
The extended real addition operation is commutative. (Contributed by NM,
26-Dec-2011.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(𝐵 +𝑒
𝐴)) |
|
Theorem | xaddid1 9532 |
Extended real version of addid1 7817. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) =
𝐴) |
|
Theorem | xaddid2 9533 |
Extended real version of addid2 7818. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0
+𝑒 𝐴) =
𝐴) |
|
Theorem | xaddid1d 9534 |
0 is a right identity for extended real addition.
(Contributed by
Glauco Siliprandi, 17-Aug-2020.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴) |
|
Theorem | xnn0lenn0nn0 9535 |
An extended nonnegative integer which is less than or equal to a
nonnegative integer is a nonnegative integer. (Contributed by AV,
24-Nov-2021.)
|
⊢ ((𝑀 ∈ ℕ0*
∧ 𝑁 ∈
ℕ0 ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) |
|
Theorem | xnn0le2is012 9536 |
An extended nonnegative integer which is less than or equal to 2 is either
0 or 1 or 2. (Contributed by AV, 24-Nov-2021.)
|
⊢ ((𝑁 ∈ ℕ0*
∧ 𝑁 ≤ 2) →
(𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2)) |
|
Theorem | xnn0xadd0 9537 |
The sum of two extended nonnegative integers is 0 iff
each of the two
extended nonnegative integers is 0. (Contributed
by AV,
14-Dec-2020.)
|
⊢ ((𝐴 ∈ ℕ0*
∧ 𝐵 ∈
ℕ0*) → ((𝐴 +𝑒 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
|
Theorem | xnegdi 9538 |
Extended real version of negdi 7936. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |
|
Theorem | xaddass 9539 |
Associativity of extended real addition. The correct condition here is
"it is not the case that both +∞ and
-∞ appear as one of
𝐴,
𝐵, 𝐶, i.e. ¬
{+∞, -∞} ⊆ {𝐴, 𝐵, 𝐶}", but this
condition is difficult to work with, so we break the theorem into two
parts: this one, where -∞ is not present in
𝐴, 𝐵, 𝐶, and
xaddass2 9540, where +∞ is
not present. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
∧ (𝐶 ∈
ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
|
Theorem | xaddass2 9540 |
Associativity of extended real addition. See xaddass 9539 for notes on the
hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
∧ (𝐶 ∈
ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
|
Theorem | xpncan 9541 |
Extended real version of pncan 7885. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒
-𝑒𝐵) =
𝐴) |
|
Theorem | xnpcan 9542 |
Extended real version of npcan 7888. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
𝐴) |
|
Theorem | xleadd1a 9543 |
Extended real version of leadd1 8105; note that the converse implication is
not true, unlike the real version (for example 0 <
1 but
(1 +𝑒 +∞) ≤ (0
+𝑒 +∞)). (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
|
Theorem | xleadd2a 9544 |
Commuted form of xleadd1a 9543. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵)) |
|
Theorem | xleadd1 9545 |
Weakened version of xleadd1a 9543 under which the reverse implication is
true. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))) |
|
Theorem | xltadd1 9546 |
Extended real version of ltadd1 8104. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))) |
|
Theorem | xltadd2 9547 |
Extended real version of ltadd2 8094. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵))) |
|
Theorem | xaddge0 9548 |
The sum of nonnegative extended reals is nonnegative. (Contributed by
Mario Carneiro, 21-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (0 ≤ 𝐴 ∧ 0
≤ 𝐵)) → 0 ≤
(𝐴 +𝑒
𝐵)) |
|
Theorem | xle2add 9549 |
Extended real version of le2add 8119. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐷 ∈ ℝ*)) →
((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷))) |
|
Theorem | xlt2add 9550 |
Extended real version of lt2add 8120. Note that ltleadd 8121, which has
weaker assumptions, is not true for the extended reals (since
0 + +∞ < 1 + +∞ fails).
(Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐷 ∈ ℝ*)) →
((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))) |
|
Theorem | xsubge0 9551 |
Extended real version of subge0 8150. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) |
|
Theorem | xposdif 9552 |
Extended real version of posdif 8130. (Contributed by Mario Carneiro,
24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒
-𝑒𝐴))) |
|
Theorem | xlesubadd 9553 |
Under certain conditions, the conclusion of lesubadd 8109 is true even in the
extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒
-𝑒𝐵)
≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵))) |
|
Theorem | xaddcld 9554 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈
ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
|
Theorem | xadd4d 9555 |
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 7848. (Contributed by Alexander van der Vekens,
21-Dec-2017.)
|
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) & ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) & ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) & ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠
-∞)) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) |
|
Theorem | xnn0add4d 9556 |
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9555. (Contributed by AV,
12-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐵 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐶 ∈
ℕ0*)
& ⊢ (𝜑 → 𝐷 ∈
ℕ0*) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) |
|
Theorem | xleaddadd 9557 |
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.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐴) ≤ (𝐵 +𝑒 𝐵))) |
|
3.5.3 Real number intervals
|
|
Syntax | cioo 9558 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 9559 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 9560 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 9561 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 9562* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-ioc 9563* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Definition | df-ico 9564* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-icc 9565* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Theorem | ixxval 9566* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) |
|
Theorem | elixx1 9567* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) |
|
Theorem | ixxf 9568* |
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 9569* |
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 9570* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆
ℝ* |
|
Theorem | elixx3g 9571* |
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 9572* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) |
|
Theorem | ixxdisj 9573* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) |
|
Theorem | ixxss1 9574* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss2 9575* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss12 9576* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) |
|
Theorem | iooex 9577 |
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 9578* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooidg 9579 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅) |
|
Theorem | elioo3g 9580 |
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 9581 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioore 9582 |
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 9583 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐴 ∈
(𝐴(,)𝐵)) |
|
Theorem | ubioog 9584 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ 𝐵 ∈
(𝐴(,)𝐵)) |
|
Theorem | iooval2 9585* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooss1 9586 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iooss2 9587 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
|
Theorem | iocval 9588* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | icoval 9589* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iccval 9590* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
|
Theorem | elioo2 9591 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioc1 9592 |
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 9593 |
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 9594 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
|
Theorem | iccid 9595 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) |
|
Theorem | icc0r 9596 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐵 < 𝐴 → (𝐴[,]𝐵) = ∅)) |
|
Theorem | eliooxr 9597 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈
ℝ*)) |
|
Theorem | eliooord 9598 |
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 9599 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 9655. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) |
|
Theorem | lbico1 9600 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 9654. (Contributed by FL, 29-May-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) |