Theorem List for Intuitionistic Logic Explorer - 9701-9800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rpne0 9701 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
   |
|
Theorem | rpap0 9702 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
 #   |
|
Theorem | rprene0 9703 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
 
   |
|
Theorem | rpreap0 9704 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
 
#    |
|
Theorem | rpcnne0 9705 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
 
   |
|
Theorem | rpcnap0 9706 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
 
#    |
|
Theorem | ralrp 9707 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
       |
|
Theorem | rexrp 9708 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
       |
|
Theorem | rpaddcl 9709 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
    
  |
|
Theorem | rpmulcl 9710 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
    
  |
|
Theorem | rpdivcl 9711 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
    
  |
|
Theorem | rpreccl 9712 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
  
  |
|
Theorem | rphalfcl 9713 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
 
   |
|
Theorem | rpgecl 9714 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
  
  |
|
Theorem | rphalflt 9715 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
 

  |
|
Theorem | rerpdivcl 9716 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
    
  |
|
Theorem | ge0p1rp 9717 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
    
  |
|
Theorem | rpnegap 9718 |
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|
  #   
   |
|
Theorem | negelrp 9719 |
Elementhood of a negation in the positive real numbers. (Contributed by
Thierry Arnoux, 19-Sep-2018.)
|
      |
|
Theorem | negelrpd 9720 |
The negation of a negative number is in the positive real numbers.
(Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
     
  |
|
Theorem | 0nrp 9721 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
 |
|
Theorem | ltsubrp 9722 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
    
  |
|
Theorem | ltaddrp 9723 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
   
   |
|
Theorem | difrp 9724 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
     
   |
|
Theorem | elrpd 9725 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
       |
|
Theorem | nnrpd 9726 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | zgt1rpn0n1 9727 |
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.)
|
     
   |
|
Theorem | rpred 9728 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpxrd 9729 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpcnd 9730 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpgt0d 9731 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpge0d 9732 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
     |
|
Theorem | rpne0d 9733 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpap0d 9734 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
   #   |
|
Theorem | rpregt0d 9735 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rprege0d 9736 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rprene0d 9737 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rpcnne0d 9738 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rpreccld 9739 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rprecred 9740 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rphalfcld 9741 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
       |
|
Theorem | reclt1d 9742 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
    
    |
|
Theorem | recgt1d 9743 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
   
 
   |
|
Theorem | rpaddcld 9744 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
     
   |
|
Theorem | rpmulcld 9745 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
         |
|
Theorem | rpdivcld 9746 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
         |
|
Theorem | ltrecd 9747 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
       
     |
|
Theorem | lerecd 9748 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
       
     |
|
Theorem | ltrec1d 9749 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
             |
|
Theorem | lerec2d 9750 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
             |
|
Theorem | lediv2ad 9751 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
             
   |
|
Theorem | ltdiv2d 9752 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | lediv2d 9753 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ledivdivd 9754 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
                 
   |
|
Theorem | divge1 9755 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
  
    |
|
Theorem | divlt1lt 9756 |
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.)
|
         |
|
Theorem | divle1le 9757 |
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.)
|
     
   |
|
Theorem | ledivge1le 9758 |
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.)
|
  
 

     |
|
Theorem | ge0p1rpd 9759 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
     
   |
|
Theorem | rerpdivcld 9760 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | ltsubrpd 9761 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | ltaddrpd 9762 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | ltaddrp2d 9763 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | ltmulgt11d 9764 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
     
     |
|
Theorem | ltmulgt12d 9765 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
     
     |
|
Theorem | gt0divd 9766 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
     
     |
|
Theorem | ge0divd 9767 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
     
     |
|
Theorem | rpgecld 9768 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | divge0d 9769 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
           |
|
Theorem | ltmul1d 9770 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ltmul2d 9771 |
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 9772 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | lemul2d 9773 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ltdiv1d 9774 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | lediv1d 9775 |
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 9776 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ltmuldiv2d 9777 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | lemuldivd 9778 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
         
     |
|
Theorem | lemuldiv2d 9779 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
         
     |
|
Theorem | ltdivmuld 9780 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ltdivmul2d 9781 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ledivmuld 9782 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ledivmul2d 9783 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ltmul1dd 9784 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
               |
|
Theorem | ltmul2dd 9785 |
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 9786 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
               |
|
Theorem | lediv1dd 9787 |
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 9788 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                 
   |
|
Theorem | ltdiv23d 9789 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
               |
|
Theorem | lediv23d 9790 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
               |
|
Theorem | mul2lt0rlt0 9791 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
      
      |
|
Theorem | mul2lt0rgt0 9792 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
      
      |
|
Theorem | mul2lt0llt0 9793 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
      
      |
|
Theorem | mul2lt0lgt0 9794 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
2-Oct-2018.)
|
      
      |
|
Theorem | mul2lt0np 9795 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
             |
|
Theorem | mul2lt0pn 9796 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
             |
|
Theorem | lt2mul2divd 9797 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
             
 
     |
|
Theorem | nnledivrp 9798 |
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.)
|
         |
|
Theorem | nn0ledivnn 9799 |
Division of a nonnegative integer by a positive integer is less than or
equal to the integer. (Contributed by AV, 19-Jun-2021.)
|
       |
|
Theorem | addlelt 9800 |
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.)
|
     
   |