HomeHome Intuitionistic Logic Explorer
Theorem List (p. 85 of 94)
< 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 - 8401-8500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremltmuldiv2d 8401 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((𝐶 · A) < BA < (B / 𝐶)))
 
Theoremlemuldivd 8402 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((A · 𝐶) ≤ BA ≤ (B / 𝐶)))
 
Theoremlemuldiv2d 8403 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((𝐶 · A) ≤ BA ≤ (B / 𝐶)))
 
Theoremltdivmuld 8404 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((A / 𝐶) < BA < (𝐶 · B)))
 
Theoremltdivmul2d 8405 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((A / 𝐶) < BA < (B · 𝐶)))
 
Theoremledivmuld 8406 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((A / 𝐶) ≤ BA ≤ (𝐶 · B)))
 
Theoremledivmul2d 8407 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)       (φ → ((A / 𝐶) ≤ BA ≤ (B · 𝐶)))
 
Theoremltmul1dd 8408 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)    &   (φA < B)       (φ → (A · 𝐶) < (B · 𝐶))
 
Theoremltmul2dd 8409 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.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)    &   (φA < B)       (φ → (𝐶 · A) < (𝐶 · B))
 
Theoremltdiv1dd 8410 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)    &   (φA < B)       (φ → (A / 𝐶) < (B / 𝐶))
 
Theoremlediv1dd 8411 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)    &   (φAB)       (φ → (A / 𝐶) ≤ (B / 𝐶))
 
Theoremlediv12ad 8412 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ𝐶 +)    &   (φ𝐷 ℝ)    &   (φ → 0 ≤ A)    &   (φAB)    &   (φ𝐶𝐷)       (φ → (A / 𝐷) ≤ (B / 𝐶))
 
Theoremltdiv23d 8413 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB +)    &   (φ𝐶 +)    &   (φ → (A / B) < 𝐶)       (φ → (A / 𝐶) < B)
 
Theoremlediv23d 8414 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB +)    &   (φ𝐶 +)    &   (φ → (A / B) ≤ 𝐶)       (φ → (A / 𝐶) ≤ B)
 
Theoremlt2mul2divd 8415 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB +)    &   (φ𝐶 ℝ)    &   (φ𝐷 +)       (φ → ((A · B) < (𝐶 · 𝐷) ↔ (A / 𝐷) < (𝐶 / B)))
 
3.5.2  Infinity and the extended real number system (cont.)
 
Syntaxcxne 8416 Extend class notation to include the negative of an extended real.
class -𝑒A
 
Syntaxcxad 8417 Extend class notation to include addition of extended reals.
class +𝑒
 
Syntaxcxmu 8418 Extend class notation to include multiplication of extended reals.
class ·e
 
Definitiondf-xneg 8419 Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
-𝑒A = if(A = +∞, -∞, if(A = -∞, +∞, -A))
 
Definitiondf-xadd 8420* Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
+𝑒 = (x *, y * ↦ if(x = +∞, if(y = -∞, 0, +∞), if(x = -∞, if(y = +∞, 0, -∞), if(y = +∞, +∞, if(y = -∞, -∞, (x + y))))))
 
Definitiondf-xmul 8421* Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
·e = (x *, y * ↦ if((x = 0 y = 0), 0, if((((0 < y x = +∞) (y < 0 x = -∞)) ((0 < x y = +∞) (x < 0 y = -∞))), +∞, if((((0 < y x = -∞) (y < 0 x = +∞)) ((0 < x y = -∞) (x < 0 y = +∞))), -∞, (x · y)))))
 
Theorempnfxr 8422 Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
+∞ *
 
Theorempnfex 8423 Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
+∞ V
 
Theoremmnfxr 8424 Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
-∞ *
 
Theoremltxr 8425 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.)
((A * B *) → (A < B ↔ ((((A B ℝ) A < B) (A = -∞ B = +∞)) ((A B = +∞) (A = -∞ B ℝ)))))
 
Theoremelxr 8426 Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
(A * ↔ (A A = +∞ A = -∞))
 
Theorempnfnemnf 8427 Plus and minus infinity are different elements of *. (Contributed by NM, 14-Oct-2005.)
+∞ ≠ -∞
 
Theoremmnfnepnf 8428 Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ ≠ +∞
 
Theoremxrnemnf 8429 An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * A ≠ -∞) ↔ (A A = +∞))
 
Theoremxrnepnf 8430 An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * A ≠ +∞) ↔ (A A = -∞))
 
Theoremxrltnr 8431 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
(A * → ¬ A < A)
 
Theoremltpnf 8432 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
(A ℝ → A < +∞)
 
Theorem0ltpnf 8433 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 < +∞
 
Theoremmnflt 8434 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
(A ℝ → -∞ < A)
 
Theoremmnflt0 8435 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ < 0
 
Theoremmnfltpnf 8436 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
-∞ < +∞
 
Theoremmnfltxr 8437 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
((A A = +∞) → -∞ < A)
 
Theorempnfnlt 8438 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
(A * → ¬ +∞ < A)
 
Theoremnltmnf 8439 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
(A * → ¬ A < -∞)
 
Theorempnfge 8440 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
(A *A ≤ +∞)
 
Theorem0lepnf 8441 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
0 ≤ +∞
 
Theoremnn0pnfge0 8442 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 8443 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
(A * → -∞ ≤ A)
 
Theoremxrltnsym 8444 Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
((A * B *) → (A < B → ¬ B < A))
 
Theoremxrltnsym2 8445 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
((A * B *) → ¬ (A < B B < A))
 
Theoremxrlttr 8446 Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
((A * B * 𝐶 *) → ((A < B B < 𝐶) → A < 𝐶))
 
Theoremxrltso 8447 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
< Or ℝ*
 
Theoremxrlttri3 8448 Extended real version of lttri3 6855. (Contributed by NM, 9-Feb-2006.)
((A * B *) → (A = B ↔ (¬ A < B ¬ B < A)))
 
Theoremxrltle 8449 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
((A * B *) → (A < BAB))
 
Theoremxrleid 8450 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
(A *AA)
 
Theoremxrletri3 8451 Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
((A * B *) → (A = B ↔ (AB BA)))
 
Theoremxrlelttr 8452 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((A * B * 𝐶 *) → ((AB B < 𝐶) → A < 𝐶))
 
Theoremxrltletr 8453 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((A * B * 𝐶 *) → ((A < B B𝐶) → A < 𝐶))
 
Theoremxrletr 8454 Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
((A * B * 𝐶 *) → ((AB B𝐶) → A𝐶))
 
Theoremxrlttrd 8455 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(φA *)    &   (φB *)    &   (φ𝐶 *)    &   (φA < B)    &   (φB < 𝐶)       (φA < 𝐶)
 
Theoremxrlelttrd 8456 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(φA *)    &   (φB *)    &   (φ𝐶 *)    &   (φAB)    &   (φB < 𝐶)       (φA < 𝐶)
 
Theoremxrltletrd 8457 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(φA *)    &   (φB *)    &   (φ𝐶 *)    &   (φA < B)    &   (φB𝐶)       (φA < 𝐶)
 
Theoremxrletrd 8458 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(φA *)    &   (φB *)    &   (φ𝐶 *)    &   (φAB)    &   (φB𝐶)       (φA𝐶)
 
Theoremxrltne 8459 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
((A * B * A < B) → BA)
 
Theoremnltpnft 8460 An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
(A * → (A = +∞ ↔ ¬ A < +∞))
 
Theoremngtmnft 8461 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
(A * → (A = -∞ ↔ ¬ -∞ < A))
 
Theoremxrrebnd 8462 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
(A * → (A ℝ ↔ (-∞ < A A < +∞)))
 
Theoremxrre 8463 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
(((A * B ℝ) (-∞ < A AB)) → A ℝ)
 
Theoremxrre2 8464 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
(((A * B * 𝐶 *) (A < B B < 𝐶)) → B ℝ)
 
Theoremxrre3 8465 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
(((A * B ℝ) (BA A < +∞)) → A ℝ)
 
Theoremge0gtmnf 8466 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * 0 ≤ A) → -∞ < A)
 
Theoremge0nemnf 8467 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * 0 ≤ A) → A ≠ -∞)
 
Theoremxrrege0 8468 A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
(((A * B ℝ) (0 ≤ A AB)) → A ℝ)
 
Theoremz2ge 8469* There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
((𝑀 𝑁 ℤ) → 𝑘 ℤ (𝑀𝑘 𝑁𝑘))
 
Theoremxnegeq 8470 Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(A = B → -𝑒A = -𝑒B)
 
Theoremxnegpnf 8471 Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
-𝑒+∞ = -∞
 
Theoremxnegmnf 8472 Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
-𝑒-∞ = +∞
 
Theoremrexneg 8473 Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(A ℝ → -𝑒A = -A)
 
Theoremxneg0 8474 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
-𝑒0 = 0
 
Theoremxnegcl 8475 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → -𝑒A *)
 
Theoremxnegneg 8476 Extended real version of negneg 7017. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → -𝑒-𝑒A = A)
 
Theoremxneg11 8477 Extended real version of neg11 7018. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B *) → (-𝑒A = -𝑒BA = B))
 
Theoremxltnegi 8478 Forward direction of xltneg 8479. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B * A < B) → -𝑒B < -𝑒A)
 
Theoremxltneg 8479 Extended real version of ltneg 7212. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B *) → (A < B ↔ -𝑒B < -𝑒A))
 
Theoremxleneg 8480 Extended real version of leneg 7215. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B *) → (AB ↔ -𝑒B ≤ -𝑒A))
 
Theoremxlt0neg1 8481 Extended real version of lt0neg1 7218. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → (A < 0 ↔ 0 < -𝑒A))
 
Theoremxlt0neg2 8482 Extended real version of lt0neg2 7219. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → (0 < A ↔ -𝑒A < 0))
 
Theoremxle0neg1 8483 Extended real version of le0neg1 7220. (Contributed by Mario Carneiro, 9-Sep-2015.)
(A * → (A ≤ 0 ↔ 0 ≤ -𝑒A))
 
Theoremxle0neg2 8484 Extended real version of le0neg2 7221. (Contributed by Mario Carneiro, 9-Sep-2015.)
(A * → (0 ≤ A ↔ -𝑒A ≤ 0))
 
Theoremxnegcld 8485 Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
(φA *)       (φ → -𝑒A *)
 
Theoremxrex 8486 The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
* V
 
3.5.3  Real number intervals
 
Syntaxcioo 8487 Extend class notation with the set of open intervals of extended reals.
class (,)
 
Syntaxcioc 8488 Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
 
Syntaxcico 8489 Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
 
Syntaxcicc 8490 Extend class notation with the set of closed intervals of extended reals.
class [,]
 
Definitiondf-ioo 8491* Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,) = (x *, y * ↦ {z * ∣ (x < z z < y)})
 
Definitiondf-ioc 8492* Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,] = (x *, y * ↦ {z * ∣ (x < z zy)})
 
Definitiondf-ico 8493* Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,) = (x *, y * ↦ {z * ∣ (xz z < y)})
 
Definitiondf-icc 8494* Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,] = (x *, y * ↦ {z * ∣ (xz zy)})
 
Theoremixxval 8495* Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       ((A * B *) → (A𝑂B) = {z * ∣ (A𝑅z z𝑆B)})
 
Theoremelixx1 8496* Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       ((A * B *) → (𝐶 (A𝑂B) ↔ (𝐶 * A𝑅𝐶 𝐶𝑆B)))
 
Theoremixxf 8497* 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.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ*
 
Theoremixxex 8498* The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       𝑂 V
 
Theoremixxssxr 8499* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       (A𝑂B) ⊆ ℝ*
 
Theoremelixx3g 8500* 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 A * and B *. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       (𝐶 (A𝑂B) ↔ ((A * B * 𝐶 *) (A𝑅𝐶 𝐶𝑆B)))
    < 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-9381
  Copyright terms: Public domain < Previous  Next >