Theorem List for Intuitionistic Logic Explorer - 8901-9000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ltdiv1dd 8901 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶)) |
|
Theorem | lediv1dd 8902 |
Division of both sides of a less than or equal to relation by a
positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) ≤ (𝐵 / 𝐶)) |
|
Theorem | lediv12ad 8903 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) |
|
Theorem | ltdiv23d 8904 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵) |
|
Theorem | lediv23d 8905 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵) |
|
Theorem | lt2mul2divd 8906 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) |
|
Theorem | nnledivrp 8907 |
Division of a positive integer by a positive number is less than or equal
to the integer iff the number is greater than or equal to 1. (Contributed
by AV, 19-Jun-2021.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → (1 ≤
𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐴)) |
|
Theorem | nn0ledivnn 8908 |
Division of a nonnegative integer by a positive integer is less than or
equal to the integer. (Contributed by AV, 19-Jun-2021.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≤ 𝐴) |
|
Theorem | addlelt 8909 |
If the sum of a real number and a positive real number is less than or
equal to a third real number, the first real number is less than the third
real number. (Contributed by AV, 1-Jul-2021.)
|
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁 → 𝑀 < 𝑁)) |
|
3.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 8910 |
Extend class notation to include the negative of an extended real.
|
class -𝑒𝐴 |
|
Syntax | cxad 8911 |
Extend class notation to include addition of extended reals.
|
class +𝑒 |
|
Syntax | cxmu 8912 |
Extend class notation to include multiplication of extended reals.
|
class ·e |
|
Definition | df-xneg 8913 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) |
|
Definition | df-xadd 8914* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if(𝑥 = +∞,
if(𝑦 = -∞, 0,
+∞), if(𝑥 =
-∞, if(𝑦 = +∞,
0, -∞), if(𝑦 =
+∞, +∞, if(𝑦 =
-∞, -∞, (𝑥 +
𝑦)))))) |
|
Definition | df-xmul 8915* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if((𝑥 = 0 ∨
𝑦 = 0), 0, if((((0 <
𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))) |
|
Theorem | ltxr 8916 |
The 'less than' binary relation on the set of extended reals.
Definition 12-3.1 of [Gleason] p. 173.
(Contributed by NM,
14-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))))) |
|
Theorem | elxr 8917 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
|
Theorem | xrnemnf 8918 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
|
Theorem | xrnepnf 8919 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞)) |
|
Theorem | xrltnr 8920 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 < 𝐴) |
|
Theorem | ltpnf 8921 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
|
Theorem | 0ltpnf 8922 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 < +∞ |
|
Theorem | mnflt 8923 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) |
|
Theorem | mnflt0 8924 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ -∞ < 0 |
|
Theorem | mnfltpnf 8925 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ -∞ < +∞ |
|
Theorem | mnfltxr 8926 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴) |
|
Theorem | pnfnlt 8927 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
+∞ < 𝐴) |
|
Theorem | nltmnf 8928 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 <
-∞) |
|
Theorem | pnfge 8929 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤
+∞) |
|
Theorem | 0lepnf 8930 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 ≤ +∞ |
|
Theorem | nn0pnfge0 8931 |
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 8932 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → -∞
≤ 𝐴) |
|
Theorem | xrltnsym 8933 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
|
Theorem | xrltnsym2 8934 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | xrlttr 8935 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltso 8936 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
⊢ < Or
ℝ* |
|
Theorem | xrlttri3 8937 |
Extended real version of lttri3 7247. (Contributed by NM, 9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | xrltle 8938 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
|
Theorem | xrleid 8939 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) |
|
Theorem | xrletri3 8940 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | xrlelttr 8941 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltletr 8942 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrletr 8943 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | xrlttrd 8944 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrlelttrd 8945 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrltletrd 8946 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrletrd 8947 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | xrltne 8948 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) |
|
Theorem | nltpnft 8949 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 <
+∞)) |
|
Theorem | ngtmnft 8950 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬
-∞ < 𝐴)) |
|
Theorem | xrrebnd 8951 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔
(-∞ < 𝐴 ∧
𝐴 <
+∞))) |
|
Theorem | xrre 8952 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧
(-∞ < 𝐴 ∧
𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
|
Theorem | xrre2 8953 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) |
|
Theorem | xrre3 8954 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) |
|
Theorem | ge0gtmnf 8955 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → -∞ <
𝐴) |
|
Theorem | ge0nemnf 8956 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ≠
-∞) |
|
Theorem | xrrege0 8957 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
|
Theorem | z2ge 8958* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) |
|
Theorem | xnegeq 8959 |
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 8960 |
Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒+∞ =
-∞ |
|
Theorem | xnegmnf 8961 |
Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒-∞ =
+∞ |
|
Theorem | rexneg 8962 |
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 8963 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒0 = 0 |
|
Theorem | xnegcl 8964 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒𝐴
∈ ℝ*) |
|
Theorem | xnegneg 8965 |
Extended real version of negneg 7414. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒-𝑒𝐴 = 𝐴) |
|
Theorem | xneg11 8966 |
Extended real version of neg11 7415. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | xltnegi 8967 |
Forward direction of xltneg 8968. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵
< -𝑒𝐴) |
|
Theorem | xltneg 8968 |
Extended real version of ltneg 7622. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔
-𝑒𝐵
< -𝑒𝐴)) |
|
Theorem | xleneg 8969 |
Extended real version of leneg 7625. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔
-𝑒𝐵
≤ -𝑒𝐴)) |
|
Theorem | xlt0neg1 8970 |
Extended real version of lt0neg1 7628. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 <
-𝑒𝐴)) |
|
Theorem | xlt0neg2 8971 |
Extended real version of lt0neg2 7629. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 <
𝐴 ↔
-𝑒𝐴
< 0)) |
|
Theorem | xle0neg1 8972 |
Extended real version of le0neg1 7630. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤
-𝑒𝐴)) |
|
Theorem | xle0neg2 8973 |
Extended real version of le0neg2 7631. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 ≤
𝐴 ↔
-𝑒𝐴
≤ 0)) |
|
Theorem | xnegcld 8974 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ*) ⇒ ⊢ (𝜑 → -𝑒𝐴 ∈
ℝ*) |
|
Theorem | xrex 8975 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
⊢ ℝ* ∈
V |
|
3.5.3 Real number intervals
|
|
Syntax | cioo 8976 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 8977 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 8978 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 8979 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 8980* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-ioc 8981* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Definition | df-ico 8982* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
|
Definition | df-icc 8983* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
|
Theorem | ixxval 8984* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) |
|
Theorem | elixx1 8985* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) |
|
Theorem | ixxf 8986* |
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 8987* |
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 8988* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆
ℝ* |
|
Theorem | elixx3g 8989* |
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 8990* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) |
|
Theorem | ixxdisj 8991* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) |
|
Theorem | ixxss1 8992* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss2 8993* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) |
|
Theorem | ixxss12 8994* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤))
& ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) |
|
Theorem | iooex 8995 |
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 8996* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) |
|
Theorem | iooidg 8997 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅) |
|
Theorem | elioo3g 8998 |
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 8999 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
|
Theorem | elioore 9000 |
A member of an open interval of reals is a real. (Contributed by NM,
17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ) |