Home | Intuitionistic Logic Explorer Theorem List (p. 77 of 94) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lediv12a 7601 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
Theorem | lediv2a 7602 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
Theorem | reclt1 7603 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
Theorem | recgt1 7604 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
Theorem | recgt1i 7605 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
Theorem | recp1lt1 7606 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
Theorem | recreclt 7607 | Given a positive number , construct a new positive number less than both and 1. (Contributed by NM, 28-Dec-2005.) |
Theorem | le2msq 7608 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | msq11 7609 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | ledivp1 7610 | Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.) |
Theorem | squeeze0 7611* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
Theorem | ltp1i 7612 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
Theorem | recgt0i 7613 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
Theorem | recgt0ii 7614 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
Theorem | prodgt0i 7615 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
Theorem | prodge0i 7616 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) |
Theorem | divgt0i 7617 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | divge0i 7618 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
Theorem | ltreci 7619 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
Theorem | lereci 7620 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
Theorem | lt2msqi 7621 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
Theorem | le2msqi 7622 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
Theorem | msq11i 7623 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
Theorem | divgt0i2i 7624 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | ltrecii 7625 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
Theorem | divgt0ii 7626 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
Theorem | ltmul1i 7627 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
Theorem | ltdiv1i 7628 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
Theorem | ltmuldivi 7629 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
Theorem | ltmul2i 7630 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
Theorem | lemul1i 7631 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
Theorem | lemul2i 7632 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
Theorem | ltdiv23i 7633 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
Theorem | ltdiv23ii 7634 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
Theorem | ltmul1ii 7635 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.) |
Theorem | ltdiv1ii 7636 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
Theorem | ltp1d 7637 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lep1d 7638 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltm1d 7639 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lem1d 7640 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | recgt0d 7641 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | divgt0d 7642 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | mulgt1d 7643 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemulge11d 7644 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemulge12d 7645 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul1ad 7646 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul2ad 7647 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltmul12ad 7648 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul12ad 7649 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul12bd 7650 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | crap0 7651 | The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.) |
# # # | ||
Theorem | creur 7652* | The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | creui 7653* | The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | cju 7654* | The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.) |
Syntax | cn 7655 | Extend class notation to include the class of positive integers. |
Definition | df-inn 7656* | Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 7657 instead. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) (New usage is discouraged.) |
Theorem | dfnn2 7657* | Definition of the set of positive integers. Another name for df-inn 7656. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) |
Theorem | peano5nni 7658* | Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | nnssre 7659 | The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
Theorem | nnsscn 7660 | The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
Theorem | nnex 7661 | The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | nnre 7662 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
Theorem | nncn 7663 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
Theorem | nnrei 7664 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
Theorem | nncni 7665 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
Theorem | 1nn 7666 | Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) |
Theorem | peano2nn 7667 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | nnred 7668 | A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nncnd 7669 | A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | peano2nnd 7670 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nnind 7671* | Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 7675 for an example of its use. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
Theorem | nnindALT 7672* |
Principle of Mathematical Induction (inference schema). The last four
hypotheses give us the substitution instances we need; the first two are
the induction step and the basis.
This ALT version of nnind 7671 has a different hypothesis order. It may be easier to use with the metamath program's Proof Assistant, because "MM-PA> assign last" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> minimize nnind /allow". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | nn1m1nn 7673 | Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.) |
Theorem | nn1suc 7674* | If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 16-May-2014.) |
Theorem | nnaddcl 7675 | Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.) |
Theorem | nnmulcl 7676 | Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) |
Theorem | nnmulcli 7677 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | nnge1 7678 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
Theorem | nnle1eq1 7679 | A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.) |
Theorem | nngt0 7680 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
Theorem | nnnlt1 7681 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | 0nnn 7682 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) |
Theorem | nnne0 7683 | A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) |
Theorem | nnap0 7684 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# | ||
Theorem | nngt0i 7685 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
Theorem | nnne0i 7686 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
Theorem | nn2ge 7687* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
Theorem | nn1gt1 7688 | A positive integer is either one or greater than one. This is for ; 0elnn 4283 is a similar theorem for (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.) |
Theorem | nngt1ne1 7689 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
Theorem | nndivre 7690 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
Theorem | nnrecre 7691 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
Theorem | nnrecgt0 7692 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
Theorem | nnsub 7693 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
Theorem | nnsubi 7694 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
Theorem | nndiv 7695* | Two ways to express " divides " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | nndivtr 7696 | Transitive property of divisibility: if divides and divides , then divides . Typically, would be an integer, although the theorem holds for complex . (Contributed by NM, 3-May-2005.) |
Theorem | nnge1d 7697 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nngt0d 7698 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nnne0d 7699 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nnrecred 7700 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |