![]() |
Metamath
Proof Explorer Theorem List (p. 131 of 479) | < 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: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rpgecl 13001 | A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง ๐ด โค ๐ต) โ ๐ต โ โ+) | ||
Theorem | rphalflt 13002 | Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.) |
โข (๐ด โ โ+ โ (๐ด / 2) < ๐ด) | ||
Theorem | rerpdivcl 13003 | Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด / ๐ต) โ โ) | ||
Theorem | ge0p1rp 13004 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (๐ด + 1) โ โ+) | ||
Theorem | rpneg 13005 | 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 13006 | Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
โข (๐ด โ โ โ (-๐ด โ โ+ โ ๐ด < 0)) | ||
Theorem | negelrpd 13007 | The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด < 0) โ โข (๐ โ -๐ด โ โ+) | ||
Theorem | 0nrp 13008 | Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
โข ยฌ 0 โ โ+ | ||
Theorem | ltsubrp 13009 | Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด โ ๐ต) < ๐ด) | ||
Theorem | ltaddrp 13010 | Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ ๐ด < (๐ด + ๐ต)) | ||
Theorem | difrp 13011 | Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ต โ ๐ด) โ โ+)) | ||
Theorem | elrpd 13012 | Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 < ๐ด) โ โข (๐ โ ๐ด โ โ+) | ||
Theorem | nnrpd 13013 | A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ+) | ||
Theorem | zgt1rpn0n1 13014 | 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 13015 | A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rpxrd 13016 | A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ ๐ด โ โ*) | ||
Theorem | rpcnd 13017 | A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rpgt0d 13018 | A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ 0 < ๐ด) | ||
Theorem | rpge0d 13019 | A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ 0 โค ๐ด) | ||
Theorem | rpne0d 13020 | A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ ๐ด โ 0) | ||
Theorem | rpregt0d 13021 | A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (๐ด โ โ โง 0 < ๐ด)) | ||
Theorem | rprege0d 13022 | A positive real is real and greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (๐ด โ โ โง 0 โค ๐ด)) | ||
Theorem | rprene0d 13023 | A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (๐ด โ โ โง ๐ด โ 0)) | ||
Theorem | rpcnne0d 13024 | A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (๐ด โ โ โง ๐ด โ 0)) | ||
Theorem | rpreccld 13025 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (1 / ๐ด) โ โ+) | ||
Theorem | rprecred 13026 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (1 / ๐ด) โ โ) | ||
Theorem | rphalfcld 13027 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) โ โข (๐ โ (๐ด / 2) โ โ+) | ||
Theorem | reclt1d 13028 | 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 13029 | 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 13030 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด + ๐ต) โ โ+) | ||
Theorem | rpmulcld 13031 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด ยท ๐ต) โ โ+) | ||
Theorem | rpdivcld 13032 | Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด / ๐ต) โ โ+) | ||
Theorem | ltrecd 13033 | The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) | ||
Theorem | lerecd 13034 | The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) | ||
Theorem | ltrec1d 13035 | Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ (1 / ๐ด) < ๐ต) โ โข (๐ โ (1 / ๐ต) < ๐ด) | ||
Theorem | lerec2d 13036 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ด โค (1 / ๐ต)) โ โข (๐ โ ๐ต โค (1 / ๐ด)) | ||
Theorem | lediv2ad 13037 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ถ / ๐ต) โค (๐ถ / ๐ด)) | ||
Theorem | ltdiv2d 13038 | Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) | ||
Theorem | lediv2d 13039 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ถ / ๐ต) โค (๐ถ / ๐ด))) | ||
Theorem | ledivdivd 13040 | Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ท โ โ+) & โข (๐ โ (๐ด / ๐ต) โค (๐ถ / ๐ท)) โ โข (๐ โ (๐ท / ๐ถ) โค (๐ต / ๐ด)) | ||
Theorem | divge1 13041 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง ๐ด โค ๐ต) โ 1 โค (๐ต / ๐ด)) | ||
Theorem | divlt1lt 13042 | 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 13043 | 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 13044 | 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 13045 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) โ โข (๐ โ (๐ด + 1) โ โ+) | ||
Theorem | rerpdivcld 13046 | Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด / ๐ต) โ โ) | ||
Theorem | ltsubrpd 13047 | Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด โ ๐ต) < ๐ด) | ||
Theorem | ltaddrpd 13048 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ ๐ด < (๐ด + ๐ต)) | ||
Theorem | ltaddrp2d 13049 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ ๐ด < (๐ต + ๐ด)) | ||
Theorem | ltmulgt11d 13050 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (1 < ๐ด โ ๐ต < (๐ต ยท ๐ด))) | ||
Theorem | ltmulgt12d 13051 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (1 < ๐ด โ ๐ต < (๐ด ยท ๐ต))) | ||
Theorem | gt0divd 13052 | Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (0 < ๐ด โ 0 < (๐ด / ๐ต))) | ||
Theorem | ge0divd 13053 | Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (0 โค ๐ด โ 0 โค (๐ด / ๐ต))) | ||
Theorem | rpgecld 13054 | A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ต โค ๐ด) โ โข (๐ โ ๐ด โ โ+) | ||
Theorem | divge0d 13055 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ 0 โค ๐ด) โ โข (๐ โ 0 โค (๐ด / ๐ต)) | ||
Theorem | ltmul1d 13056 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ))) | ||
Theorem | ltmul2d 13057 | 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 13058 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) | ||
Theorem | lemul2d 13059 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต))) | ||
Theorem | ltdiv1d 13060 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ))) | ||
Theorem | lediv1d 13061 | 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 13062 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด ยท ๐ถ) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | ltmuldiv2d 13063 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ถ ยท ๐ด) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | lemuldivd 13064 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด ยท ๐ถ) โค ๐ต โ ๐ด โค (๐ต / ๐ถ))) | ||
Theorem | lemuldiv2d 13065 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ถ ยท ๐ด) โค ๐ต โ ๐ด โค (๐ต / ๐ถ))) | ||
Theorem | ltdivmuld 13066 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) < ๐ต โ ๐ด < (๐ถ ยท ๐ต))) | ||
Theorem | ltdivmul2d 13067 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) < ๐ต โ ๐ด < (๐ต ยท ๐ถ))) | ||
Theorem | ledivmuld 13068 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) โค ๐ต โ ๐ด โค (๐ถ ยท ๐ต))) | ||
Theorem | ledivmul2d 13069 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) โค ๐ต โ ๐ด โค (๐ต ยท ๐ถ))) | ||
Theorem | ltmul1dd 13070 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ)) | ||
Theorem | ltmul2dd 13071 | 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 13072 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ (๐ด / ๐ถ) < (๐ต / ๐ถ)) | ||
Theorem | lediv1dd 13073 | 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 13074 | Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โค ๐ท) โ โข (๐ โ (๐ด / ๐ท) โค (๐ต / ๐ถ)) | ||
Theorem | mul2lt0rlt0 13075 | 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 13076 | 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 13077 | 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 13078 | 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 13079 | 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 13080 | 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 13081 | 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 13082 | Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด / ๐ต) < ๐ถ) โ โข (๐ โ (๐ด / ๐ถ) < ๐ต) | ||
Theorem | lediv23d 13083 | Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด / ๐ต) โค ๐ถ) โ โข (๐ โ (๐ด / ๐ถ) โค ๐ต) | ||
Theorem | lt2mul2divd 13084 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ+) โ โข (๐ โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ (๐ด / ๐ท) < (๐ถ / ๐ต))) | ||
Theorem | nnledivrp 13085 | 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 13086 | 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 13087 | 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 13088 | Extend class notation to include the negative of an extended real. |
class -๐๐ด | ||
Syntax | cxad 13089 | Extend class notation to include addition of extended reals. |
class +๐ | ||
Syntax | cxmu 13090 | Extend class notation to include multiplication of extended reals. |
class ยทe | ||
Definition | df-xneg 13091 | Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.) |
โข -๐๐ด = if(๐ด = +โ, -โ, if(๐ด = -โ, +โ, -๐ด)) | ||
Definition | df-xadd 13092* | Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข +๐ = (๐ฅ โ โ*, ๐ฆ โ โ* โฆ if(๐ฅ = +โ, if(๐ฆ = -โ, 0, +โ), if(๐ฅ = -โ, if(๐ฆ = +โ, 0, -โ), if(๐ฆ = +โ, +โ, if(๐ฆ = -โ, -โ, (๐ฅ + ๐ฆ)))))) | ||
Definition | df-xmul 13093* | 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 13094 | 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 13095 | Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ* โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) | ||
Theorem | xrnemnf 13096 | An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง ๐ด โ -โ) โ (๐ด โ โ โจ ๐ด = +โ)) | ||
Theorem | xrnepnf 13097 | An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง ๐ด โ +โ) โ (๐ด โ โ โจ ๐ด = -โ)) | ||
Theorem | xrltnr 13098 | The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ ๐ด < ๐ด) | ||
Theorem | ltpnf 13099 | Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ โ ๐ด < +โ) | ||
Theorem | ltpnfd 13100 | Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด < +โ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |