Home | Metamath
Proof Explorer Theorem List (p. 130 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rpaddcld 12901 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด + ๐ต) โ โ+) | ||
Theorem | rpmulcld 12902 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด ยท ๐ต) โ โ+) | ||
Theorem | rpdivcld 12903 | Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด / ๐ต) โ โ+) | ||
Theorem | ltrecd 12904 | The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) | ||
Theorem | lerecd 12905 | The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) | ||
Theorem | ltrec1d 12906 | Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ (1 / ๐ด) < ๐ต) โ โข (๐ โ (1 / ๐ต) < ๐ด) | ||
Theorem | lerec2d 12907 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ด โค (1 / ๐ต)) โ โข (๐ โ ๐ต โค (1 / ๐ด)) | ||
Theorem | lediv2ad 12908 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ถ / ๐ต) โค (๐ถ / ๐ด)) | ||
Theorem | ltdiv2d 12909 | Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) | ||
Theorem | lediv2d 12910 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ถ / ๐ต) โค (๐ถ / ๐ด))) | ||
Theorem | ledivdivd 12911 | Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ท โ โ+) & โข (๐ โ (๐ด / ๐ต) โค (๐ถ / ๐ท)) โ โข (๐ โ (๐ท / ๐ถ) โค (๐ต / ๐ด)) | ||
Theorem | divge1 12912 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง ๐ด โค ๐ต) โ 1 โค (๐ต / ๐ด)) | ||
Theorem | divlt1lt 12913 | 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 12914 | 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 12915 | 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 12916 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) โ โข (๐ โ (๐ด + 1) โ โ+) | ||
Theorem | rerpdivcld 12917 | Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด / ๐ต) โ โ) | ||
Theorem | ltsubrpd 12918 | Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด โ ๐ต) < ๐ด) | ||
Theorem | ltaddrpd 12919 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ ๐ด < (๐ด + ๐ต)) | ||
Theorem | ltaddrp2d 12920 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ ๐ด < (๐ต + ๐ด)) | ||
Theorem | ltmulgt11d 12921 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (1 < ๐ด โ ๐ต < (๐ต ยท ๐ด))) | ||
Theorem | ltmulgt12d 12922 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (1 < ๐ด โ ๐ต < (๐ด ยท ๐ต))) | ||
Theorem | gt0divd 12923 | Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (0 < ๐ด โ 0 < (๐ด / ๐ต))) | ||
Theorem | ge0divd 12924 | Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (0 โค ๐ด โ 0 โค (๐ด / ๐ต))) | ||
Theorem | rpgecld 12925 | A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ต โค ๐ด) โ โข (๐ โ ๐ด โ โ+) | ||
Theorem | divge0d 12926 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ 0 โค ๐ด) โ โข (๐ โ 0 โค (๐ด / ๐ต)) | ||
Theorem | ltmul1d 12927 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ))) | ||
Theorem | ltmul2d 12928 | 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 12929 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) | ||
Theorem | lemul2d 12930 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต))) | ||
Theorem | ltdiv1d 12931 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ))) | ||
Theorem | lediv1d 12932 | 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 12933 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด ยท ๐ถ) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | ltmuldiv2d 12934 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ถ ยท ๐ด) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | lemuldivd 12935 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด ยท ๐ถ) โค ๐ต โ ๐ด โค (๐ต / ๐ถ))) | ||
Theorem | lemuldiv2d 12936 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ถ ยท ๐ด) โค ๐ต โ ๐ด โค (๐ต / ๐ถ))) | ||
Theorem | ltdivmuld 12937 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) < ๐ต โ ๐ด < (๐ถ ยท ๐ต))) | ||
Theorem | ltdivmul2d 12938 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) < ๐ต โ ๐ด < (๐ต ยท ๐ถ))) | ||
Theorem | ledivmuld 12939 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) โค ๐ต โ ๐ด โค (๐ถ ยท ๐ต))) | ||
Theorem | ledivmul2d 12940 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ ((๐ด / ๐ถ) โค ๐ต โ ๐ด โค (๐ต ยท ๐ถ))) | ||
Theorem | ltmul1dd 12941 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ)) | ||
Theorem | ltmul2dd 12942 | 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 12943 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ (๐ด / ๐ถ) < (๐ต / ๐ถ)) | ||
Theorem | lediv1dd 12944 | 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 12945 | Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โค ๐ท) โ โข (๐ โ (๐ด / ๐ท) โค (๐ต / ๐ถ)) | ||
Theorem | mul2lt0rlt0 12946 | 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 12947 | 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 12948 | 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 12949 | 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 12950 | 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 12951 | 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 12952 | 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 12953 | Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด / ๐ต) < ๐ถ) โ โข (๐ โ (๐ด / ๐ถ) < ๐ต) | ||
Theorem | lediv23d 12954 | Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด / ๐ต) โค ๐ถ) โ โข (๐ โ (๐ด / ๐ถ) โค ๐ต) | ||
Theorem | lt2mul2divd 12955 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ+) โ โข (๐ โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ (๐ด / ๐ท) < (๐ถ / ๐ต))) | ||
Theorem | nnledivrp 12956 | 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 12957 | 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 12958 | 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 12959 | Extend class notation to include the negative of an extended real. |
class -๐๐ด | ||
Syntax | cxad 12960 | Extend class notation to include addition of extended reals. |
class +๐ | ||
Syntax | cxmu 12961 | Extend class notation to include multiplication of extended reals. |
class ยทe | ||
Definition | df-xneg 12962 | Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.) |
โข -๐๐ด = if(๐ด = +โ, -โ, if(๐ด = -โ, +โ, -๐ด)) | ||
Definition | df-xadd 12963* | Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข +๐ = (๐ฅ โ โ*, ๐ฆ โ โ* โฆ if(๐ฅ = +โ, if(๐ฆ = -โ, 0, +โ), if(๐ฅ = -โ, if(๐ฆ = +โ, 0, -โ), if(๐ฆ = +โ, +โ, if(๐ฆ = -โ, -โ, (๐ฅ + ๐ฆ)))))) | ||
Definition | df-xmul 12964* | 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 12965 | 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 12966 | Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ* โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) | ||
Theorem | xrnemnf 12967 | An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง ๐ด โ -โ) โ (๐ด โ โ โจ ๐ด = +โ)) | ||
Theorem | xrnepnf 12968 | An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง ๐ด โ +โ) โ (๐ด โ โ โจ ๐ด = -โ)) | ||
Theorem | xrltnr 12969 | The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ ๐ด < ๐ด) | ||
Theorem | ltpnf 12970 | Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ โ ๐ด < +โ) | ||
Theorem | ltpnfd 12971 | Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด < +โ) | ||
Theorem | 0ltpnf 12972 | Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 0 < +โ | ||
Theorem | mnflt 12973 | Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ โ -โ < ๐ด) | ||
Theorem | mnfltd 12974 | Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ -โ < ๐ด) | ||
Theorem | mnflt0 12975 | Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข -โ < 0 | ||
Theorem | mnfltpnf 12976 | Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
โข -โ < +โ | ||
Theorem | mnfltxr 12977 | Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.) |
โข ((๐ด โ โ โจ ๐ด = +โ) โ -โ < ๐ด) | ||
Theorem | pnfnlt 12978 | No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ +โ < ๐ด) | ||
Theorem | nltmnf 12979 | No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ ๐ด < -โ) | ||
Theorem | pnfge 12980 | Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.) |
โข (๐ด โ โ* โ ๐ด โค +โ) | ||
Theorem | xnn0n0n1ge2b 12981 | An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021.) |
โข (๐ โ โ0* โ ((๐ โ 0 โง ๐ โ 1) โ 2 โค ๐)) | ||
Theorem | 0lepnf 12982 | 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 0 โค +โ | ||
Theorem | xnn0ge0 12983 | An extended nonnegative integer is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 10-Dec-2020.) |
โข (๐ โ โ0* โ 0 โค ๐) | ||
Theorem | mnfle 12984 | Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.) |
โข (๐ด โ โ* โ -โ โค ๐ด) | ||
Theorem | xrltnsym 12985 | Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | xrltnsym2 12986 | 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ ยฌ (๐ด < ๐ต โง ๐ต < ๐ด)) | ||
Theorem | xrlttri 12987 | Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri 11059 or axlttri 11160. (Contributed by NM, 14-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | xrlttr 12988 | Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | xrltso 12989 | 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.) |
โข < Or โ* | ||
Theorem | xrlttri2 12990 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 10-Dec-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โ ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | xrlttri3 12991 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 9-Feb-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด = ๐ต โ (ยฌ ๐ด < ๐ต โง ยฌ ๐ต < ๐ด))) | ||
Theorem | xrleloe 12992 | 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โค ๐ต โ (๐ด < ๐ต โจ ๐ด = ๐ต))) | ||
Theorem | xrleltne 12993 | 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ด โค ๐ต) โ (๐ด < ๐ต โ ๐ต โ ๐ด)) | ||
Theorem | xrltlen 12994 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ต โ ๐ด))) | ||
Theorem | dfle2 12995 | Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
โข โค = ( < โช ( I โพ โ*)) | ||
Theorem | dflt2 12996 | Alternative definition of 'less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
โข < = ( โค โ I ) | ||
Theorem | xrltle 12997 | 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ๐ด โค ๐ต)) | ||
Theorem | xrltled 12998 | 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 12997. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | xrleid 12999 | 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.) |
โข (๐ด โ โ* โ ๐ด โค ๐ด) | ||
Theorem | xrleidd 13000 | 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 12999. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ ๐ด โค ๐ด) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |