Theorem List for Intuitionistic Logic Explorer - 9701-9800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ltmuldivd 9701 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | ltmuldiv2d 9702 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | lemuldivd 9703 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) |
|
Theorem | lemuldiv2d 9704 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) |
|
Theorem | ltdivmuld 9705 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) |
|
Theorem | ltdivmul2d 9706 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) |
|
Theorem | ledivmuld 9707 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵))) |
|
Theorem | ledivmul2d 9708 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶))) |
|
Theorem | ltmul1dd 9709 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶)) |
|
Theorem | ltmul2dd 9710 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · 𝐴) < (𝐶 · 𝐵)) |
|
Theorem | ltdiv1dd 9711 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶)) |
|
Theorem | lediv1dd 9712 |
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 9713 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) |
|
Theorem | ltdiv23d 9714 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵) |
|
Theorem | lediv23d 9715 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵) |
|
Theorem | mul2lt0rlt0 9716 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < 𝐴) |
|
Theorem | mul2lt0rgt0 9717 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0) |
|
Theorem | mul2lt0llt0 9718 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 𝐵) |
|
Theorem | mul2lt0lgt0 9719 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
2-Oct-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐵 < 0) |
|
Theorem | mul2lt0np 9720 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) < 0) |
|
Theorem | mul2lt0pn 9721 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) < 0) |
|
Theorem | lt2mul2divd 9722 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) |
|
Theorem | nnledivrp 9723 |
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 9724 |
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 9725 |
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.)
|
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁 → 𝑀 < 𝑁)) |
|
4.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 9726 |
Extend class notation to include the negative of an extended real.
|
class -𝑒𝐴 |
|
Syntax | cxad 9727 |
Extend class notation to include addition of extended reals.
|
class +𝑒 |
|
Syntax | cxmu 9728 |
Extend class notation to include multiplication of extended reals.
|
class ·e |
|
Definition | df-xneg 9729 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) |
|
Definition | df-xadd 9730* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if(𝑥 = +∞,
if(𝑦 = -∞, 0,
+∞), if(𝑥 =
-∞, if(𝑦 = +∞,
0, -∞), if(𝑦 =
+∞, +∞, if(𝑦 =
-∞, -∞, (𝑥 +
𝑦)))))) |
|
Definition | df-xmul 9731* |
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 9732 |
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 9733 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
|
Theorem | xrnemnf 9734 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
|
Theorem | xrnepnf 9735 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞)) |
|
Theorem | xrltnr 9736 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 < 𝐴) |
|
Theorem | ltpnf 9737 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
|
Theorem | ltpnfd 9738 |
Any (finite) real is less than plus infinity. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 𝐴 < +∞) |
|
Theorem | 0ltpnf 9739 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 < +∞ |
|
Theorem | mnflt 9740 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) |
|
Theorem | mnflt0 9741 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ -∞ < 0 |
|
Theorem | mnfltpnf 9742 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ -∞ < +∞ |
|
Theorem | mnfltxr 9743 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴) |
|
Theorem | pnfnlt 9744 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
+∞ < 𝐴) |
|
Theorem | nltmnf 9745 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 <
-∞) |
|
Theorem | pnfge 9746 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤
+∞) |
|
Theorem | 0lepnf 9747 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 ≤ +∞ |
|
Theorem | nn0pnfge0 9748 |
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 9749 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → -∞
≤ 𝐴) |
|
Theorem | xrltnsym 9750 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
|
Theorem | xrltnsym2 9751 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | xrlttr 9752 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltso 9753 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
⊢ < Or
ℝ* |
|
Theorem | xrlttri3 9754 |
Extended real version of lttri3 7999. (Contributed by NM, 9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | xrltle 9755 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
|
Theorem | xrltled 9756 |
'Less than' implies 'less than or equal to' for extended reals.
Deduction form of xrltle 9755. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | xrleid 9757 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) |
|
Theorem | xrleidd 9758 |
'Less than or equal to' is reflexive for extended reals. Deduction form
of xrleid 9757. (Contributed by Glauco Siliprandi,
26-Jun-2021.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) |
|
Theorem | xnn0dcle 9759 |
Decidability of ≤ for extended nonnegative integers.
(Contributed by
Jim Kingdon, 13-Oct-2024.)
|
⊢ ((𝐴 ∈ ℕ0*
∧ 𝐵 ∈
ℕ0*) → DECID 𝐴 ≤ 𝐵) |
|
Theorem | xnn0letri 9760 |
Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon,
13-Oct-2024.)
|
⊢ ((𝐴 ∈ ℕ0*
∧ 𝐵 ∈
ℕ0*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) |
|
Theorem | xrletri3 9761 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | xrletrid 9762 |
Trichotomy law for extended reals. (Contributed by Glauco Siliprandi,
17-Aug-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | xrlelttr 9763 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltletr 9764 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrletr 9765 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | xrlttrd 9766 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrlelttrd 9767 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrltletrd 9768 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrletrd 9769 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | xrltne 9770 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) |
|
Theorem | nltpnft 9771 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 <
+∞)) |
|
Theorem | npnflt 9772 |
An extended real is less than plus infinity iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 < +∞ ↔ 𝐴 ≠
+∞)) |
|
Theorem | xgepnf 9773 |
An extended real which is greater than plus infinity is plus infinity.
(Contributed by Thierry Arnoux, 18-Dec-2016.)
|
⊢ (𝐴 ∈ ℝ* →
(+∞ ≤ 𝐴 ↔
𝐴 =
+∞)) |
|
Theorem | ngtmnft 9774 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬
-∞ < 𝐴)) |
|
Theorem | nmnfgt 9775 |
An extended real is greater than minus infinite iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* →
(-∞ < 𝐴 ↔
𝐴 ≠
-∞)) |
|
Theorem | xrrebnd 9776 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔
(-∞ < 𝐴 ∧
𝐴 <
+∞))) |
|
Theorem | xrre 9777 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧
(-∞ < 𝐴 ∧
𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
|
Theorem | xrre2 9778 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) |
|
Theorem | xrre3 9779 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) |
|
Theorem | ge0gtmnf 9780 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → -∞ <
𝐴) |
|
Theorem | ge0nemnf 9781 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ≠
-∞) |
|
Theorem | xrrege0 9782 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
|
Theorem | z2ge 9783* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) |
|
Theorem | xnegeq 9784 |
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 9785 |
Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒+∞ =
-∞ |
|
Theorem | xnegmnf 9786 |
Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒-∞ =
+∞ |
|
Theorem | rexneg 9787 |
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 9788 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ -𝑒0 = 0 |
|
Theorem | xnegcl 9789 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒𝐴
∈ ℝ*) |
|
Theorem | xnegneg 9790 |
Extended real version of negneg 8169. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* →
-𝑒-𝑒𝐴 = 𝐴) |
|
Theorem | xneg11 9791 |
Extended real version of neg11 8170. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | xltnegi 9792 |
Forward direction of xltneg 9793. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵
< -𝑒𝐴) |
|
Theorem | xltneg 9793 |
Extended real version of ltneg 8381. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔
-𝑒𝐵
< -𝑒𝐴)) |
|
Theorem | xleneg 9794 |
Extended real version of leneg 8384. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔
-𝑒𝐵
≤ -𝑒𝐴)) |
|
Theorem | xlt0neg1 9795 |
Extended real version of lt0neg1 8387. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 <
-𝑒𝐴)) |
|
Theorem | xlt0neg2 9796 |
Extended real version of lt0neg2 8388. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 <
𝐴 ↔
-𝑒𝐴
< 0)) |
|
Theorem | xle0neg1 9797 |
Extended real version of le0neg1 8389. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤
-𝑒𝐴)) |
|
Theorem | xle0neg2 9798 |
Extended real version of le0neg2 8390. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (𝐴 ∈ ℝ* → (0 ≤
𝐴 ↔
-𝑒𝐴
≤ 0)) |
|
Theorem | xrpnfdc 9799 |
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* →
DECID 𝐴 =
+∞) |
|
Theorem | xrmnfdc 9800 |
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* →
DECID 𝐴 =
-∞) |