Home Intuitionistic Logic ExplorerTheorem List (p. 90 of 110) < 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 - 8901-9000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremltdiv1dd 8901 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶))

Theoremlediv1dd 8902 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴𝐵)       (𝜑 → (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))

Theoremlediv12ad 8903 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴𝐵)    &   (𝜑𝐶𝐷)       (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))

Theoremltdiv23d 8904 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) < 𝐶)       (𝜑 → (𝐴 / 𝐶) < 𝐵)

Theoremlediv23d 8905 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) ≤ 𝐶)       (𝜑 → (𝐴 / 𝐶) ≤ 𝐵)

Theoremlt2mul2divd 8906 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))

Theoremnnledivrp 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 ≤ 𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐴))

Theoremnn0ledivnn 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𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≤ 𝐴)

Theoremaddlelt 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.)

Syntaxcxne 8910 Extend class notation to include the negative of an extended real.
class -𝑒𝐴

Syntaxcxad 8911 Extend class notation to include addition of extended reals.
class +𝑒

Syntaxcxmu 8912 Extend class notation to include multiplication of extended reals.
class ·e

Definitiondf-xneg 8913 Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))

Definitiondf-xadd 8914* Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
+𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))

Definitiondf-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 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))

Theoremltxr 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.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ)))))

Theoremelxr 8917 Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Theoremxrnemnf 8918 An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))

Theoremxrnepnf 8919 An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞))

Theoremxrltnr 8920 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)

Theoremltpnf 8921 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → 𝐴 < +∞)

Theorem0ltpnf 8922 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 < +∞

Theoremmnflt 8923 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → -∞ < 𝐴)

Theoremmnflt0 8924 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ < 0

Theoremmnfltpnf 8925 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
-∞ < +∞

Theoremmnfltxr 8926 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴)

Theorempnfnlt 8927 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)

Theoremnltmnf 8928 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)

Theorempnfge 8929 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ*𝐴 ≤ +∞)

Theorem0lepnf 8930 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
0 ≤ +∞

Theoremnn0pnfge0 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 ≤ 𝑁)

Theoremmnfle 8932 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
(𝐴 ∈ ℝ* → -∞ ≤ 𝐴)

Theoremxrltnsym 8933 Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))

Theoremxrltnsym2 8934 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵𝐵 < 𝐴))

Theoremxrlttr 8935 Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremxrltso 8936 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
< Or ℝ*

Theoremxrlttri3 8937 Extended real version of lttri3 7247. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))

Theoremxrltle 8938 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴𝐵))

Theoremxrleid 8939 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
(𝐴 ∈ ℝ*𝐴𝐴)

Theoremxrletri3 8940 Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))

Theoremxrlelttr 8941 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremxrltletr 8942 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))

Theoremxrletr 8943 Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Theoremxrlttrd 8944 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)

Theoremxrlelttrd 8945 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)

Theoremxrltletrd 8946 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴 < 𝐶)

Theoremxrletrd 8947 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)

Theoremxrltne 8948 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵𝐴)

Theoremnltpnft 8949 An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))

Theoremngtmnft 8950 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
(𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))

Theoremxrrebnd 8951 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
(𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))

Theoremxrre 8952 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)

Theoremxrre2 8953 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵𝐵 < 𝐶)) → 𝐵 ∈ ℝ)

Theoremxrre3 8954 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (𝐵𝐴𝐴 < +∞)) → 𝐴 ∈ ℝ)

Theoremge0gtmnf 8955 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)

Theoremge0nemnf 8956 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞)

Theoremxrrege0 8957 A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)

Theoremz2ge 8958* There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀𝑘𝑁𝑘))

Theoremxnegeq 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.)
(𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)

Theoremxnegpnf 8960 Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
-𝑒+∞ = -∞

Theoremxnegmnf 8961 Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
-𝑒-∞ = +∞

Theoremrexneg 8962 Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)

Theoremxneg0 8963 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
-𝑒0 = 0

Theoremxnegcl 8964 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*)

Theoremxnegneg 8965 Extended real version of negneg 7414. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴)

Theoremxneg11 8966 Extended real version of neg11 7415. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵𝐴 = 𝐵))

Theoremxltnegi 8967 Forward direction of xltneg 8968. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴)

Theoremxltneg 8968 Extended real version of ltneg 7622. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴))

Theoremxleneg 8969 Extended real version of leneg 7625. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴))

Theoremxlt0neg1 8970 Extended real version of lt0neg1 7628. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴))

Theoremxlt0neg2 8971 Extended real version of lt0neg2 7629. (Contributed by Mario Carneiro, 20-Aug-2015.)
(𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0))

Theoremxle0neg1 8972 Extended real version of le0neg1 7630. (Contributed by Mario Carneiro, 9-Sep-2015.)
(𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴))

Theoremxle0neg2 8973 Extended real version of le0neg2 7631. (Contributed by Mario Carneiro, 9-Sep-2015.)
(𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0))

Theoremxnegcld 8974 Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ*)       (𝜑 → -𝑒𝐴 ∈ ℝ*)

Theoremxrex 8975 The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
* ∈ V

3.5.3  Real number intervals

Syntaxcioo 8976 Extend class notation with the set of open intervals of extended reals.
class (,)

Syntaxcioc 8977 Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]

Syntaxcico 8978 Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)

Syntaxcicc 8979 Extend class notation with the set of closed intervals of extended reals.
class [,]

Definitiondf-ioo 8980* Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})

Definitiondf-ioc 8981* Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})

Definitiondf-ico 8982* Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})

Definitiondf-icc 8983* Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})

Theoremixxval 8984* Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧𝑧𝑆𝐵)})

Theoremelixx1 8985* Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ*𝐴𝑅𝐶𝐶𝑆𝐵)))

Theoremixxf 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.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ*

Theoremixxex 8987* The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       𝑂 ∈ V

Theoremixxssxr 8988* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       (𝐴𝑂𝐵) ⊆ ℝ*

Theoremelixx3g 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.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})       (𝐶 ∈ (𝐴𝑂𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑅𝐶𝐶𝑆𝐵)))

Theoremixxssixx 8990* An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})    &   ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐴𝑅𝑤𝐴𝑇𝑤))    &   ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑤𝑆𝐵𝑤𝑈𝐵))       (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵)

Theoremixxdisj 8991* Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})    &   ((𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵))       ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅)

Theoremixxss1 8992* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑆𝑦)})    &   ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵𝐵𝑇𝑤) → 𝐴𝑅𝑤))       ((𝐴 ∈ ℝ*𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶))

Theoremixxss2 8993* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑇𝑦)})    &   ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵𝐵𝑊𝐶) → 𝑤𝑆𝐶))       ((𝐶 ∈ ℝ*𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶))

Theoremixxss12 8994* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})    &   𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})    &   ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶𝐶𝑇𝑤) → 𝐴𝑅𝑤))    &   ((𝑤 ∈ ℝ*𝐷 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷𝐷𝑋𝐵) → 𝑤𝑆𝐵))       (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵))

Theoremiooex 8995 The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
(,) ∈ V

Theoremiooval 8996* Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥𝑥 < 𝐵)})

Theoremiooidg 8997 An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
(𝐴 ∈ ℝ* → (𝐴(,)𝐴) = ∅)

Theoremelioo3g 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.)
(𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶𝐶 < 𝐵)))

Theoremelioo1 8999 Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ*𝐴 < 𝐶𝐶 < 𝐵)))

Theoremelioore 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.)
(𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

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-10938
 Copyright terms: Public domain < Previous  Next >