Home Metamath Proof ExplorerTheorem List (p. 107 of 327) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-22411) Hilbert Space Explorer (22412-23934) Users' Mathboxes (23935-32663)

Theorem List for Metamath Proof Explorer - 10601-10700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremmulex 10601 The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)

5.5  Order sets

5.5.1  Positive reals (as a subset of complex numbers)

Syntaxcrp 10602 Extend class notation to include the class of positive reals.

Definitiondf-rp 10603 Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)

Theoremelrp 10604 Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)

Theoremelrpii 10605 Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)

Theorem1rp 10606 1 is a positive real. (Contributed by Jeffrey Hankins, 23-Nov-2008.)

Theorem2rp 10607 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpre 10608 A positive real is a real. (Contributed by NM, 27-Oct-2007.)

Theoremrpxr 10609 A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)

Theoremrpcn 10610 A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)

Theoremnnrp 10611 A natural number is a positive real. (Contributed by NM, 28-Nov-2008.)

Theoremrpssre 10612 The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)

Theoremrpgt0 10613 A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

Theoremrpge0 10614 A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)

Theoremrpregt0 10615 A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremrprege0 10616 A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremrpne0 10617 A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)

Theoremrprene0 10618 A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)

Theoremrpcnne0 10619 A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)

Theoremralrp 10620 Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)

Theoremrexrp 10621 Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)

Theoremrpaddcl 10622 Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)

Theoremrpmulcl 10623 Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)

Theoremrpdivcl 10624 Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)

Theoremrpreccl 10625 Closure law for reciprocation of positive reals. (Contributed by Jeffrey Hankins, 23-Nov-2008.)

Theoremrphalfcl 10626 Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremrpgecl 10627 A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrphalflt 10628 Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)

Theoremrerpdivcl 10629 Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)

Theoremge0p1rp 10630 A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)

Theoremrpneg 10631 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.)

Theorem0nrp 10632 Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)

Theoremltsubrp 10633 Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.)

Theoremltaddrp 10634 Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)

Theoremdifrp 10635 Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.)

Theoremelrpd 10636 Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremnnrpd 10637 A natural number is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpred 10638 A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpxrd 10639 A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpcnd 10640 A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpgt0d 10641 A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpge0d 10642 A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpne0d 10643 A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpregt0d 10644 A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrprege0d 10645 A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrprene0d 10646 A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpcnne0d 10647 A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpreccld 10648 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrprecred 10649 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrphalfcld 10650 Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremreclt1d 10651 The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrecgt1d 10652 The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpaddcld 10653 Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpmulcld 10654 Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpdivcld 10655 Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltrecd 10656 The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlerecd 10657 The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltrec1d 10658 Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlerec2d 10659 Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlediv2ad 10660 Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltdiv2d 10661 Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlediv2d 10662 Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremledivdivd 10663 Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremge0p1rpd 10664 A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrerpdivcld 10665 Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltsubrpd 10666 Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltaddrpd 10667 Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltaddrp2d 10668 Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmulgt11d 10669 Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmulgt12d 10670 Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremgt0divd 10671 Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremge0divd 10672 Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremrpgecld 10673 A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremdivge0d 10674 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmul1d 10675 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmul2d 10676 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.)

Theoremlemul1d 10677 Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlemul2d 10678 Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltdiv1d 10679 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlediv1d 10680 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmuldivd 10681 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmuldiv2d 10682 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlemuldivd 10683 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)

Theoremlemuldiv2d 10684 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)

Theoremltdivmuld 10685 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltdivmul2d 10686 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremledivmuld 10687 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremledivmul2d 10688 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltmul1dd 10689 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)

Theoremltmul2dd 10690 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.)

Theoremltdiv1dd 10691 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)

Theoremlediv1dd 10692 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)

Theoremlediv12ad 10693 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremltdiv23d 10694 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlediv23d 10695 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)

Theoremlt2mul2divd 10696 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)

5.5.2  Infinity and the extended real number system (cont.)

Syntaxcxne 10697 Extend class notation to include the negative of an extended real.