HomeTheorem List (p. 105 of 368)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 105 of 368) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-25499) |
Hilbert Space Explorer
(25500-27024) |
Users' Mathboxes
(27025-36800) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | divgt0 10401 | The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.) |
     ![/\](wedge.gif "/\"){kind=small}    
 | ||
| Theorem | divge0 10402 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
| ||
| Theorem | mulge0b 10403 | A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013.) |
   | ||
| Theorem | mulle0b 10404 | A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
| | ||
| Theorem | mulsuble0b 10405 | A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
 
| ||
| Theorem | ltmuldiv 10406 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | ltmuldiv2 10407 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | ltdivmul 10408 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | ledivmul 10409 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
|
| ||
| Theorem | ledivmulOLD 10410 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | ltdivmul2 10411 | 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | lt2mul2div 10412 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
| ||
| Theorem | ledivmul2 10413 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
|
| ||
| Theorem | ledivmul2OLD 10414 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | lemuldiv 10415 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
|
| ||
| Theorem | lemuldiv2 10416 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
|
| ||
| Theorem | ltrec 10417 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ||
| Theorem | lerec 10418 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | lt2msq1 10419 | Lemma for lt2msq 10420. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | lt2msq 10420 | Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | ltdiv2 10421 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
|
| ||
| Theorem | ltdiv2OLD 10422 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | ltrec1 10423 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | lerec2 10424 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | ledivdiv 10425 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
|
| ||
| Theorem | lediv2 10426 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.) |
|
| ||
| Theorem | ltdiv23 10427 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
|
| ||
| Theorem | lediv23 10428 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
|
| ||
| Theorem | lediv12a 10429 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
|
| ||
| Theorem | lediv2a 10430 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
|
| ||
| Theorem | reclt1 10431 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
|
| ||
| Theorem | recgt1 10432 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
| | ||
| Theorem | recgt1i 10433 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
|
| ||
| Theorem | recp1lt1 10434 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
| ||
| Theorem | recreclt 10435 |
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28-Dec-2005.)
|
|
| ||
| Theorem | le2msq 10436 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | msq11 10437 | 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 10438 | 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 10439* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
 
| ||
| Theorem | ltp1i 10440 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
| ||
| Theorem | recgt0i 10441 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
|
| ||
| Theorem | recgt0ii 10442 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
 | ||
| Theorem | prodgt0i 10443 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
|
| ||
| Theorem | prodge0i 10444 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) |
|
| ||
| Theorem | divgt0i 10445 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
| | ||
| Theorem | divge0i 10446 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
| | ||
| Theorem | ltreci 10447 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
| | ||
| Theorem | lereci 10448 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
| | ||
| Theorem | lt2msqi 10449 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
| | ||
| Theorem | le2msqi 10450 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
| | ||
| Theorem | msq11i 10451 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
| | ||
| Theorem | divgt0i2i 10452 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
|
| ||
| Theorem | ltrecii 10453 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
| | ||
| Theorem | divgt0ii 10454 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
| | ||
| Theorem | ltmul1i 10455 | 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 10456 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
|
| ||
| Theorem | ltmuldivi 10457 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
|
| ||
| Theorem | ltmul2i 10458 | 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 10459 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
|
| ||
| Theorem | lemul2i 10460 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
|
| ||
| Theorem | ltdiv23i 10461 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
|
| ||
| Theorem | ledivp1i 10462 | Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
|
| ||
| Theorem | ltdivp1i 10463 | Less-than and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
|
| ||
| Theorem | ltdiv23ii 10464 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
|
| ||
| Theorem | ltmul1ii 10465 | 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 10466 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
| | ||
| Theorem | ltp1d 10467 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
 | ||
| Theorem | lep1d 10468 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | ltm1d 10469 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lem1d 10470 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | recgt0d 10471 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | divgt0d 10472 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | mulgt1d 10473 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemulge11d 10474 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemulge12d 10475 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemul1ad 10476 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | lemul2ad 10477 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | ltmul12ad 10478 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemul12ad 10479 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | lemul12bd 10480 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | fimaxre 10481* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
    
 | ||
| Theorem | fimaxre2 10482* | A nonempty finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.) |
| | ||
| Theorem | fimaxre3 10483* | A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.) |
|
| ||
| Theorem | lbreu 10484* | If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.) |
 | ||
| Theorem | lbcl 10485* | If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
 | ||
| Theorem | lble 10486* | If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
| | ||
| Theorem | lbinfm 10487* | If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 16-Jun-2013.) |
   | ||
| Theorem | lbinfmcl 10488* | If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) |
|
| ||
| Theorem | lbinfmle 10489* | If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) |
| | ||
| Theorem | sup2 10490* | A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997.) |
 | ||
| Theorem | sup3 10491* | A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.) |
|
| ||
| Theorem | infm3lem 10492* | Lemma for infm3 10493. (Contributed by NM, 14-Jun-2005.) |
 | ||
| Theorem | infm3 10493* | The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 10491.) (Contributed by NM, 14-Jun-2005.) |
|
| ||
| Theorem | suprcl 10494* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.) |
|
| ||
| Theorem | suprub 10495* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004.) |
|
| ||
| Theorem | suprlub 10496* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
|
| ||
| Theorem | suprnub 10497* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
|
| ||
| Theorem | suprleub 10498* | The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.) |
|
| ||
| Theorem | supmul1 10499* |
The supremum function distributes over multiplication, in the sense that
, where
is shorthand for
  
and is defined as
below. This is the
simple version, with only one set argument; see supmul 10502 for the more
general case with two set arguments. (Contributed by Mario Carneiro,
5-Jul-2013.)
|
| ||
| Theorem | supmullem1 10500* | Lemma for supmul 10502. (Contributed by Mario Carneiro, 5-Jul-2013.) |
 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |