HomeHome Intuitionistic Logic Explorer
Theorem List (p. 98 of 142)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9701-9800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremltmuldivd 9701 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐶) < 𝐵𝐴 < (𝐵 / 𝐶)))
 
Theoremltmuldiv2d 9702 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐶 · 𝐴) < 𝐵𝐴 < (𝐵 / 𝐶)))
 
Theoremlemuldivd 9703 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵𝐴 ≤ (𝐵 / 𝐶)))
 
Theoremlemuldiv2d 9704 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵𝐴 ≤ (𝐵 / 𝐶)))
 
Theoremltdivmuld 9705 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) < 𝐵𝐴 < (𝐶 · 𝐵)))
 
Theoremltdivmul2d 9706 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) < 𝐵𝐴 < (𝐵 · 𝐶)))
 
Theoremledivmuld 9707 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵𝐴 ≤ (𝐶 · 𝐵)))
 
Theoremledivmul2d 9708 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵𝐴 ≤ (𝐵 · 𝐶)))
 
Theoremltmul1dd 9709 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶))
 
Theoremltmul2dd 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.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐶 · 𝐴) < (𝐶 · 𝐵))
 
Theoremltdiv1dd 9711 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶))
 
Theoremlediv1dd 9712 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴𝐵)       (𝜑 → (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))
 
Theoremlediv12ad 9713 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴𝐵)    &   (𝜑𝐶𝐷)       (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))
 
Theoremltdiv23d 9714 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) < 𝐶)       (𝜑 → (𝐴 / 𝐶) < 𝐵)
 
Theoremlediv23d 9715 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) ≤ 𝐶)       (𝜑 → (𝐴 / 𝐶) ≤ 𝐵)
 
Theoremmul2lt0rlt0 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 < 𝐴)
 
Theoremmul2lt0rgt0 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)
 
Theoremmul2lt0llt0 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 < 𝐵)
 
Theoremmul2lt0lgt0 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)
 
Theoremmul2lt0np 9720 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 0)    &   (𝜑 → 0 < 𝐵)       (𝜑 → (𝐴 · 𝐵) < 0)
 
Theoremmul2lt0pn 9721 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 0)    &   (𝜑 → 0 < 𝐵)       (𝜑 → (𝐵 · 𝐴) < 0)
 
Theoremlt2mul2divd 9722 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))
 
Theoremnnledivrp 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 ≤ 𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐴))
 
Theoremnn0ledivnn 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𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≤ 𝐴)
 
Theoremaddlelt 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.)
 
Syntaxcxne 9726 Extend class notation to include the negative of an extended real.
class -𝑒𝐴
 
Syntaxcxad 9727 Extend class notation to include addition of extended reals.
class +𝑒
 
Syntaxcxmu 9728 Extend class notation to include multiplication of extended reals.
class ·e
 
Definitiondf-xneg 9729 Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
 
Definitiondf-xadd 9730* Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
+𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
 
Definitiondf-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 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
 
Theoremltxr 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.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ)))))
 
Theoremelxr 9733 Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
 
Theoremxrnemnf 9734 An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))
 
Theoremxrnepnf 9735 An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞))
 
Theoremxrltnr 9736 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)
 
Theoremltpnf 9737 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → 𝐴 < +∞)
 
Theoremltpnfd 9738 Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 < +∞)
 
Theorem0ltpnf 9739 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 < +∞
 
Theoremmnflt 9740 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → -∞ < 𝐴)
 
Theoremmnflt0 9741 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ < 0
 
Theoremmnfltpnf 9742 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
-∞ < +∞
 
Theoremmnfltxr 9743 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴)
 
Theorempnfnlt 9744 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
 
Theoremnltmnf 9745 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
 
Theorempnfge 9746 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ*𝐴 ≤ +∞)
 
Theorem0lepnf 9747 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
0 ≤ +∞
 
Theoremnn0pnfge0 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 ≤ 𝑁)
 
Theoremmnfle 9749 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
(𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
 
Theoremxrltnsym 9750 Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
 
Theoremxrltnsym2 9751 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵𝐵 < 𝐴))
 
Theoremxrlttr 9752 Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremxrltso 9753 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
< Or ℝ*
 
Theoremxrlttri3 9754 Extended real version of lttri3 7999. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
 
Theoremxrltle 9755 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴𝐵))
 
Theoremxrltled 9756 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 9755. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)       (𝜑𝐴𝐵)
 
Theoremxrleid 9757 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
(𝐴 ∈ ℝ*𝐴𝐴)
 
Theoremxrleidd 9758 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 9757. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
(𝜑𝐴 ∈ ℝ*)       (𝜑𝐴𝐴)
 
Theoremxnn0dcle 9759 Decidability of for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝐴 ∈ ℕ0*𝐵 ∈ ℕ0*) → DECID 𝐴𝐵)
 
Theoremxnn0letri 9760 Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝐴 ∈ ℕ0*𝐵 ∈ ℕ0*) → (𝐴𝐵𝐵𝐴))
 
Theoremxrletri3 9761 Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
 
Theoremxrletrid 9762 Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵𝐴)       (𝜑𝐴 = 𝐵)
 
Theoremxrlelttr 9763 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremxrltletr 9764 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
 
Theoremxrletr 9765 Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 
Theoremxrlttrd 9766 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)
 
Theoremxrlelttrd 9767 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)
 
Theoremxrltletrd 9768 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴 < 𝐶)
 
Theoremxrletrd 9769 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremxrltne 9770 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵𝐴)
 
Theoremnltpnft 9771 An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))
 
Theoremnpnflt 9772 An extended real is less than plus infinity iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
(𝐴 ∈ ℝ* → (𝐴 < +∞ ↔ 𝐴 ≠ +∞))
 
Theoremxgepnf 9773 An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
(𝐴 ∈ ℝ* → (+∞ ≤ 𝐴𝐴 = +∞))
 
Theoremngtmnft 9774 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
(𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
 
Theoremnmnfgt 9775 An extended real is greater than minus infinite iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
(𝐴 ∈ ℝ* → (-∞ < 𝐴𝐴 ≠ -∞))
 
Theoremxrrebnd 9776 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
(𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))
 
Theoremxrre 9777 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)
 
Theoremxrre2 9778 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵𝐵 < 𝐶)) → 𝐵 ∈ ℝ)
 
Theoremxrre3 9779 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐵𝐴𝐴 < +∞)) → 𝐴 ∈ ℝ)
 
Theoremge0gtmnf 9780 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
 
Theoremge0nemnf 9781 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞)
 
Theoremxrrege0 9782 A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)
 
Theoremz2ge 9783* There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀𝑘𝑁𝑘))
 
Theoremxnegeq 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.)
(𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
 
Theoremxnegpnf 9785 Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
-𝑒+∞ = -∞
 
Theoremxnegmnf 9786 Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
-𝑒-∞ = +∞
 
Theoremrexneg 9787 Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
 
Theoremxneg0 9788 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
-𝑒0 = 0
 
Theoremxnegcl 9789 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*)
 
Theoremxnegneg 9790 Extended real version of negneg 8169. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴)
 
Theoremxneg11 9791 Extended real version of neg11 8170. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵𝐴 = 𝐵))
 
Theoremxltnegi 9792 Forward direction of xltneg 9793. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴)
 
Theoremxltneg 9793 Extended real version of ltneg 8381. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴))
 
Theoremxleneg 9794 Extended real version of leneg 8384. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴))
 
Theoremxlt0neg1 9795 Extended real version of lt0neg1 8387. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴))
 
Theoremxlt0neg2 9796 Extended real version of lt0neg2 8388. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0))
 
Theoremxle0neg1 9797 Extended real version of le0neg1 8389. (Contributed by Mario Carneiro, 9-Sep-2015.)
(𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴))
 
Theoremxle0neg2 9798 Extended real version of le0neg2 8390. (Contributed by Mario Carneiro, 9-Sep-2015.)
(𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0))
 
Theoremxrpnfdc 9799 An extended real is or is not plus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.)
(𝐴 ∈ ℝ*DECID 𝐴 = +∞)
 
Theoremxrmnfdc 9800 An extended real is or is not minus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.)
(𝐴 ∈ ℝ*DECID 𝐴 = -∞)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14113
  Copyright terms: Public domain < Previous  Next >