HomeHome Intuitionistic Logic Explorer
Theorem List (p. 97 of 137)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9601-9700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremelrpd 9601 Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <  A )   =>    |-  ( ph  ->  A  e.  RR+ )
 
Theoremnnrpd 9602 A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  NN )   =>    |-  ( ph  ->  A  e.  RR+ )
 
Theoremzgt1rpn0n1 9603 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.)
 |-  ( B  e.  ( ZZ>=
 `  2 )  ->  ( B  e.  RR+  /\  B  =/=  0  /\  B  =/=  1 ) )
 
Theoremrpred 9604 A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  A  e.  RR )
 
Theoremrpxrd 9605 A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  A  e.  RR* )
 
Theoremrpcnd 9606 A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  A  e.  CC )
 
Theoremrpgt0d 9607 A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  0  <  A )
 
Theoremrpge0d 9608 A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  0  <_  A )
 
Theoremrpne0d 9609 A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  A  =/=  0 )
 
Theoremrpap0d 9610 A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  A #  0 )
 
Theoremrpregt0d 9611 A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )
 
Theoremrprege0d 9612 A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  ( A  e.  RR  /\  0  <_  A ) )
 
Theoremrprene0d 9613 A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  ( A  e.  RR  /\  A  =/=  0 ) )
 
Theoremrpcnne0d 9614 A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  ( A  e.  CC  /\  A  =/=  0 ) )
 
Theoremrpreccld 9615 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  (
 1  /  A )  e.  RR+ )
 
Theoremrprecred 9616 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  (
 1  /  A )  e.  RR )
 
Theoremrphalfcld 9617 Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  ( A  /  2 )  e.  RR+ )
 
Theoremreclt1d 9618 The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  ( A  <  1  <->  1  <  (
 1  /  A )
 ) )
 
Theoremrecgt1d 9619 The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  (
 1  <  A  <->  ( 1  /  A )  <  1 ) )
 
Theoremrpaddcld 9620 Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  +  B )  e.  RR+ )
 
Theoremrpmulcld 9621 Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  x.  B )  e.  RR+ )
 
Theoremrpdivcld 9622 Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  /  B )  e.  RR+ )
 
Theoremltrecd 9623 The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  <  B  <->  ( 1  /  B )  <  ( 1 
 /  A ) ) )
 
Theoremlerecd 9624 The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  <_  B  <->  ( 1  /  B )  <_  ( 1 
 /  A ) ) )
 
Theoremltrec1d 9625 Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  ( 1  /  A )  <  B )   =>    |-  ( ph  ->  ( 1  /  B )  <  A )
 
Theoremlerec2d 9626 Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  A 
 <_  ( 1  /  B ) )   =>    |-  ( ph  ->  B  <_  ( 1  /  A ) )
 
Theoremlediv2ad 9627 Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  0  <_  C )   &    |-  ( ph  ->  A  <_  B )   =>    |-  ( ph  ->  ( C  /  B )  <_  ( C  /  A ) )
 
Theoremltdiv2d 9628 Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <  B  <->  ( C  /  B )  <  ( C 
 /  A ) ) )
 
Theoremlediv2d 9629 Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <_  B  <->  ( C  /  B )  <_  ( C 
 /  A ) ) )
 
Theoremledivdivd 9630 Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  D  e.  RR+ )   &    |-  ( ph  ->  ( A  /  B ) 
 <_  ( C  /  D ) )   =>    |-  ( ph  ->  ( D  /  C )  <_  ( B  /  A ) )
 
Theoremdivge1 9631 The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  ( ( A  e.  RR+  /\  B  e.  RR  /\  A  <_  B )  -> 
 1  <_  ( B  /  A ) )
 
Theoremdivlt1lt 9632 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.)
 |-  ( ( A  e.  RR  /\  B  e.  RR+ )  ->  ( ( A 
 /  B )  < 
 1 
 <->  A  <  B ) )
 
Theoremdivle1le 9633 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.)
 |-  ( ( A  e.  RR  /\  B  e.  RR+ )  ->  ( ( A 
 /  B )  <_ 
 1 
 <->  A  <_  B )
 )
 
Theoremledivge1le 9634 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.)
 |-  ( ( A  e.  RR  /\  B  e.  RR+  /\  ( C  e.  RR+  /\  1  <_  C )
 )  ->  ( A  <_  B  ->  ( A  /  C )  <_  B ) )
 
Theoremge0p1rpd 9635 A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0 
 <_  A )   =>    |-  ( ph  ->  ( A  +  1 )  e.  RR+ )
 
Theoremrerpdivcld 9636 Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  /  B )  e. 
 RR )
 
Theoremltsubrpd 9637 Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  ( A  -  B )  <  A )
 
Theoremltaddrpd 9638 Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  A  <  ( A  +  B ) )
 
Theoremltaddrp2d 9639 Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  A  <  ( B  +  A ) )
 
Theoremltmulgt11d 9640 Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  (
 1  <  A  <->  B  <  ( B  x.  A ) ) )
 
Theoremltmulgt12d 9641 Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  (
 1  <  A  <->  B  <  ( A  x.  B ) ) )
 
Theoremgt0divd 9642 Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  (
 0  <  A  <->  0  <  ( A  /  B ) ) )
 
Theoremge0divd 9643 Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   =>    |-  ( ph  ->  (
 0  <_  A  <->  0  <_  ( A  /  B ) ) )
 
Theoremrpgecld 9644 A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  B 
 <_  A )   =>    |-  ( ph  ->  A  e.  RR+ )
 
Theoremdivge0d 9645 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  0 
 <_  A )   =>    |-  ( ph  ->  0  <_  ( A  /  B ) )
 
Theoremltmul1d 9646 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <  B  <->  ( A  x.  C )  <  ( B  x.  C ) ) )
 
Theoremltmul2d 9647 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.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <  B  <->  ( C  x.  A )  <  ( C  x.  B ) ) )
 
Theoremlemul1d 9648 Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <_  B  <->  ( A  x.  C )  <_  ( B  x.  C ) ) )
 
Theoremlemul2d 9649 Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <_  B  <->  ( C  x.  A )  <_  ( C  x.  B ) ) )
 
Theoremltdiv1d 9650 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <  B  <->  ( A  /  C )  <  ( B 
 /  C ) ) )
 
Theoremlediv1d 9651 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  ( A  <_  B  <->  ( A  /  C )  <_  ( B 
 /  C ) ) )
 
Theoremltmuldivd 9652 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  x.  C )  <  B  <->  A  <  ( B 
 /  C ) ) )
 
Theoremltmuldiv2d 9653 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( C  x.  A )  <  B  <->  A  <  ( B 
 /  C ) ) )
 
Theoremlemuldivd 9654 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  x.  C )  <_  B  <->  A  <_  ( B 
 /  C ) ) )
 
Theoremlemuldiv2d 9655 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( C  x.  A )  <_  B  <->  A  <_  ( B 
 /  C ) ) )
 
Theoremltdivmuld 9656 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  /  C )  <  B  <->  A  <  ( C  x.  B ) ) )
 
Theoremltdivmul2d 9657 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  /  C )  <  B  <->  A  <  ( B  x.  C ) ) )
 
Theoremledivmuld 9658 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  /  C )  <_  B  <->  A  <_  ( C  x.  B ) ) )
 
Theoremledivmul2d 9659 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  /  C )  <_  B  <->  A  <_  ( B  x.  C ) ) )
 
Theoremltmul1dd 9660 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  ( A  x.  C )  < 
 ( B  x.  C ) )
 
Theoremltmul2dd 9661 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.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  ( C  x.  A )  < 
 ( C  x.  B ) )
 
Theoremltdiv1dd 9662 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  ( A  /  C )  < 
 ( B  /  C ) )
 
Theoremlediv1dd 9663 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  <_  B )   =>    |-  ( ph  ->  ( A  /  C )  <_  ( B  /  C ) )
 
Theoremlediv12ad 9664 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  0 
 <_  A )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  C 
 <_  D )   =>    |-  ( ph  ->  ( A  /  D )  <_  ( B  /  C ) )
 
Theoremltdiv23d 9665 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  ( A  /  B )  <  C )   =>    |-  ( ph  ->  ( A  /  C )  <  B )
 
Theoremlediv23d 9666 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  ( A  /  B ) 
 <_  C )   =>    |-  ( ph  ->  ( A  /  C )  <_  B )
 
Theoremmul2lt0rlt0 9667 If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( A  x.  B )  <  0 )   =>    |-  ( ( ph  /\  B  <  0 )  ->  0  <  A )
 
Theoremmul2lt0rgt0 9668 If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( A  x.  B )  <  0 )   =>    |-  ( ( ph  /\  0  <  B )  ->  A  <  0 )
 
Theoremmul2lt0llt0 9669 If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( A  x.  B )  <  0 )   =>    |-  ( ( ph  /\  A  <  0 )  ->  0  <  B )
 
Theoremmul2lt0lgt0 9670 If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 2-Oct-2018.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( A  x.  B )  <  0 )   =>    |-  ( ( ph  /\  0  <  A )  ->  B  <  0 )
 
Theoremmul2lt0np 9671 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  0
 )   &    |-  ( ph  ->  0  <  B )   =>    |-  ( ph  ->  ( A  x.  B )  < 
 0 )
 
Theoremmul2lt0pn 9672 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  0
 )   &    |-  ( ph  ->  0  <  B )   =>    |-  ( ph  ->  ( B  x.  A )  < 
 0 )
 
Theoremlt2mul2divd 9673 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR+ )   =>    |-  ( ph  ->  (
 ( A  x.  B )  <  ( C  x.  D )  <->  ( A  /  D )  <  ( C 
 /  B ) ) )
 
Theoremnnledivrp 9674 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.)
 |-  ( ( A  e.  NN  /\  B  e.  RR+ )  ->  ( 1  <_  B 
 <->  ( A  /  B )  <_  A ) )
 
Theoremnn0ledivnn 9675 Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021.)
 |-  ( ( A  e.  NN0  /\  B  e.  NN )  ->  ( A  /  B )  <_  A )
 
Theoremaddlelt 9676 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.)
 |-  ( ( M  e.  RR  /\  N  e.  RR  /\  A  e.  RR+ )  ->  ( ( M  +  A )  <_  N  ->  M  <  N ) )
 
4.5.2  Infinity and the extended real number system (cont.)
 
Syntaxcxne 9677 Extend class notation to include the negative of an extended real.
 class  -e A
 
Syntaxcxad 9678 Extend class notation to include addition of extended reals.
 class  +e
 
Syntaxcxmu 9679 Extend class notation to include multiplication of extended reals.
 class  xe
 
Definitiondf-xneg 9680 Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
 |-  -e A  =  if ( A  = +oo , -oo ,  if ( A  = -oo , +oo ,  -u A ) )
 
Definitiondf-xadd 9681* Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
 |- 
 +e  =  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  = +oo ,  if ( y  = -oo ,  0 , +oo ) ,  if ( x  = -oo ,  if ( y  = +oo ,  0 , -oo ) ,  if ( y  = +oo , +oo ,  if ( y  = -oo , -oo ,  ( x  +  y ) ) ) ) ) )
 
Definitiondf-xmul 9682* Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
 |-  xe  =  ( x  e.  RR* ,  y  e.  RR*  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 ,  if (
 ( ( ( 0  <  y  /\  x  = +oo )  \/  (
 y  <  0  /\  x  = -oo ) )  \/  ( ( 0  <  x  /\  y  = +oo )  \/  ( x  <  0  /\  y  = -oo ) ) ) , +oo ,  if ( ( ( ( 0  <  y  /\  x  = -oo )  \/  ( y  <  0  /\  x  = +oo ) )  \/  (
 ( 0  <  x  /\  y  = -oo )  \/  ( x  < 
 0  /\  y  = +oo ) ) ) , -oo ,  ( x  x.  y ) ) ) ) )
 
Theoremltxr 9683 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.)
 |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  <->  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <RR  B )  \/  ( A  = -oo  /\  B  = +oo ) )  \/  ( ( A  e.  RR  /\  B  = +oo )  \/  ( A  = -oo  /\  B  e.  RR ) ) ) ) )
 
Theoremelxr 9684 Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
 |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
 
Theoremxrnemnf 9685 An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
 |-  ( ( A  e.  RR*  /\  A  =/= -oo )  <->  ( A  e.  RR  \/  A  = +oo ) )
 
Theoremxrnepnf 9686 An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
 |-  ( ( A  e.  RR*  /\  A  =/= +oo )  <->  ( A  e.  RR  \/  A  = -oo ) )
 
Theoremxrltnr 9687 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
 |-  ( A  e.  RR*  ->  -.  A  <  A )
 
Theoremltpnf 9688 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
 |-  ( A  e.  RR  ->  A  < +oo )
 
Theoremltpnfd 9689 Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   =>    |-  ( ph  ->  A  < +oo )
 
Theorem0ltpnf 9690 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 |-  0  < +oo
 
Theoremmnflt 9691 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
 |-  ( A  e.  RR  -> -oo  <  A )
 
Theoremmnflt0 9692 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 |- -oo  <  0
 
Theoremmnfltpnf 9693 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
 |- -oo  < +oo
 
Theoremmnfltxr 9694 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
 |-  ( ( A  e.  RR  \/  A  = +oo )  -> -oo  <  A )
 
Theorempnfnlt 9695 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
 |-  ( A  e.  RR*  ->  -. +oo  <  A )
 
Theoremnltmnf 9696 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
 |-  ( A  e.  RR*  ->  -.  A  < -oo )
 
Theorempnfge 9697 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
 |-  ( A  e.  RR*  ->  A  <_ +oo )
 
Theorem0lepnf 9698 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
 |-  0  <_ +oo
 
Theoremnn0pnfge0 9699 If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
 |-  ( ( N  e.  NN0 
 \/  N  = +oo )  ->  0  <_  N )
 
Theoremmnfle 9700 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
 |-  ( A  e.  RR*  -> -oo  <_  A )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13694
  Copyright terms: Public domain < Previous  Next >