Home | Metamath
Proof Explorer Theorem List (p. 125 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rpaddcl 12401 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℝ+) | ||
Theorem | rpmulcl 12402 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+) | ||
Theorem | rpmtmip 12403 | "Minus times minus is plus", see also nnmtmip 11652, holds for positive reals, too (formalized to "The product of two negative reals is a positive real"). "The reason for this" in this case is that (-𝐴 · -𝐵) = (𝐴 · 𝐵) for all complex numbers 𝐴 and 𝐵 because of mul2neg 11068, 𝐴 and 𝐵 are complex numbers because of rpcn 12389, and (𝐴 · 𝐵) ∈ ℝ+ because of rpmulcl 12402. Note that the opposites -𝐴 and -𝐵 of the positive reals 𝐴 and 𝐵 are negative reals. (Contributed by AV, 23-Dec-2022.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (-𝐴 · -𝐵) ∈ ℝ+) | ||
Theorem | rpdivcl 12404 | Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+) | ||
Theorem | rpreccl 12405 | Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+) | ||
Theorem | rphalfcl 12406 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+) | ||
Theorem | rpgecl 12407 | A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ+) | ||
Theorem | rphalflt 12408 | Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴) | ||
Theorem | rerpdivcl 12409 | Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | ge0p1rp 12410 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈ ℝ+) | ||
Theorem | rpneg 12411 | Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of [Apostol] p. 20. (Contributed by NM, 7-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 ∈ ℝ+ ↔ ¬ -𝐴 ∈ ℝ+)) | ||
Theorem | negelrp 12412 | Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
⊢ (𝐴 ∈ ℝ → (-𝐴 ∈ ℝ+ ↔ 𝐴 < 0)) | ||
Theorem | negelrpd 12413 | The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℝ+) | ||
Theorem | 0nrp 12414 | Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ¬ 0 ∈ ℝ+ | ||
Theorem | ltsubrp 12415 | Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 − 𝐵) < 𝐴) | ||
Theorem | ltaddrp 12416 | Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵)) | ||
Theorem | difrp 12417 | Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℝ+)) | ||
Theorem | elrpd 12418 | Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ+) | ||
Theorem | nnrpd 12419 | A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ+) | ||
Theorem | zgt1rpn0n1 12420 | An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g. base 2, base 3 or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ (𝐵 ∈ (ℤ≥‘2) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1)) | ||
Theorem | rpred 12421 | A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rpxrd 12422 | A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | rpcnd 12423 | A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | rpgt0d 12424 | A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | rpge0d 12425 | A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
Theorem | rpne0d 12426 | A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | rpregt0d 12427 | A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | rprege0d 12428 | A positive real is real and greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | ||
Theorem | rprene0d 12429 | A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) | ||
Theorem | rpcnne0d 12430 | A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) | ||
Theorem | rpreccld 12431 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ+) | ||
Theorem | rprecred 12432 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | rphalfcld 12433 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ+) | ||
Theorem | reclt1d 12434 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 1 ↔ 1 < (1 / 𝐴))) | ||
Theorem | recgt1d 12435 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ (1 / 𝐴) < 1)) | ||
Theorem | rpaddcld 12436 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ+) | ||
Theorem | rpmulcld 12437 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ+) | ||
Theorem | rpdivcld 12438 | Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+) | ||
Theorem | ltrecd 12439 | The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) | ||
Theorem | lerecd 12440 | The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) | ||
Theorem | ltrec1d 12441 | Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (1 / 𝐴) < 𝐵) ⇒ ⊢ (𝜑 → (1 / 𝐵) < 𝐴) | ||
Theorem | lerec2d 12442 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≤ (1 / 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 ≤ (1 / 𝐴)) | ||
Theorem | lediv2ad 12443 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)) | ||
Theorem | ltdiv2d 12444 | Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) | ||
Theorem | lediv2d 12445 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) | ||
Theorem | ledivdivd 12446 | Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ (𝐶 / 𝐷)) ⇒ ⊢ (𝜑 → (𝐷 / 𝐶) ≤ (𝐵 / 𝐴)) | ||
Theorem | divge1 12447 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 1 ≤ (𝐵 / 𝐴)) | ||
Theorem | divlt1lt 12448 | A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < 𝐵)) | ||
Theorem | divle1le 12449 | A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) ≤ 1 ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | ledivge1le 12450 | If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 / 𝐶) ≤ 𝐵)) | ||
Theorem | ge0p1rpd 12451 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 + 1) ∈ ℝ+) | ||
Theorem | rerpdivcld 12452 | Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | ltsubrpd 12453 | Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) < 𝐴) | ||
Theorem | ltaddrpd 12454 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵)) | ||
Theorem | ltaddrp2d 12455 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐴)) | ||
Theorem | ltmulgt11d 12456 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴))) | ||
Theorem | ltmulgt12d 12457 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐴 · 𝐵))) | ||
Theorem | gt0divd 12458 | Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵))) | ||
Theorem | ge0divd 12459 | Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) | ||
Theorem | rpgecld 12460 | A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ+) | ||
Theorem | divge0d 12461 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵)) | ||
Theorem | ltmul1d 12462 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) | ||
Theorem | ltmul2d 12463 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) | ||
Theorem | lemul1d 12464 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) | ||
Theorem | lemul2d 12465 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) | ||
Theorem | ltdiv1d 12466 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) | ||
Theorem | lediv1d 12467 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))) | ||
Theorem | ltmuldivd 12468 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltmuldiv2d 12469 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | lemuldivd 12470 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | lemuldiv2d 12471 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | ltdivmuld 12472 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) | ||
Theorem | ltdivmul2d 12473 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) | ||
Theorem | ledivmuld 12474 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵))) | ||
Theorem | ledivmul2d 12475 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶))) | ||
Theorem | ltmul1dd 12476 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶)) | ||
Theorem | ltmul2dd 12477 | 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 12478 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶)) | ||
Theorem | lediv1dd 12479 | 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 12480 | Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) | ||
Theorem | mul2lt0rlt0 12481 | 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 12482 | 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 12483 | 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 12484 | 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 | mul2lt0bi 12485 | 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 < 𝐵) ∨ (0 < 𝐴 ∧ 𝐵 < 0)))) | ||
Theorem | prodge0rd 12486 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Revised by AV, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) ⇒ ⊢ (𝜑 → 0 ≤ 𝐵) | ||
Theorem | prodge0ld 12487 | Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by AV, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
Theorem | ltdiv23d 12488 | Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵) | ||
Theorem | lediv23d 12489 | Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵) | ||
Theorem | lt2mul2divd 12490 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) | ||
Theorem | nnledivrp 12491 | 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 12492 | 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 12493 | 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.) |
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁 → 𝑀 < 𝑁)) | ||
Syntax | cxne 12494 | Extend class notation to include the negative of an extended real. |
class -𝑒𝐴 | ||
Syntax | cxad 12495 | Extend class notation to include addition of extended reals. |
class +𝑒 | ||
Syntax | cxmu 12496 | Extend class notation to include multiplication of extended reals. |
class ·e | ||
Definition | df-xneg 12497 | Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.) |
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) | ||
Definition | df-xadd 12498* | Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦)))))) | ||
Definition | df-xmul 12499* | 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 12500 | 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.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |