Theorem List for Intuitionistic Logic Explorer - 8001-8100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ltneg 8001 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
         |
|
Theorem | ltnegcon1 8002 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
         |
|
Theorem | ltnegcon2 8003 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
    
    |
|
Theorem | leneg 8004 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
    
    |
|
Theorem | lenegcon1 8005 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
         |
|
Theorem | lenegcon2 8006 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
    
    |
|
Theorem | lt0neg1 8007 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
      |
|
Theorem | lt0neg2 8008 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
      |
|
Theorem | le0neg1 8009 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
      |
|
Theorem | le0neg2 8010 |
Comparison of a number and its negative to zero. (Contributed by NM,
24-Aug-1999.)
|
      |
|
Theorem | addge01 8011 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21-Feb-2005.)
|
   
     |
|
Theorem | addge02 8012 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27-Jul-2005.)
|
   
     |
|
Theorem | add20 8013 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
    
    

    |
|
Theorem | subge0 8014 |
Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
    

   |
|
Theorem | suble0 8015 |
Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
     
   |
|
Theorem | leaddle0 8016 |
The sum of a real number and a second real number is less then the real
number iff the second real number is negative. (Contributed by Alexander
van der Vekens, 30-May-2018.)
|
     
   |
|
Theorem | subge02 8017 |
Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|
         |
|
Theorem | lesub0 8018 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
       
   |
|
Theorem | mullt0 8019 |
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8-Jun-2009.)
|
    
 
    |
|
Theorem | 0le1 8020 |
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29-Apr-2015.)
|
 |
|
Theorem | ltordlem 8021* |
Lemma for eqord1 8022. (Contributed by Mario Carneiro,
14-Jun-2014.)
|
  
 
      
   
    
 

   |
|
Theorem | eqord1 8022* |
A strictly increasing real function on a subset of is
one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised
by Jim Kingdon, 20-Dec-2022.)
|
  
 
      
   
    
 

   |
|
Theorem | eqord2 8023* |
A strictly decreasing real function on a subset of is one-to-one.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
  
 
      
   
    
 

   |
|
Theorem | leidi 8024 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
 |
|
Theorem | gt0ne0i 8025 |
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16-Sep-1999.)
|
   |
|
Theorem | gt0ne0ii 8026 |
Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|
 |
|
Theorem | addgt0i 8027 |
Addition of 2 positive numbers is positive. (Contributed by NM,
16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
   
   |
|
Theorem | addge0i 8028 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
   
   |
|
Theorem | addgegt0i 8029 |
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
   
   |
|
Theorem | addgt0ii 8030 |
Addition of 2 positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
   |
|
Theorem | add20i 8031 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28-Jul-1999.)
|
           |
|
Theorem | ltnegi 8032 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
     |
|
Theorem | lenegi 8033 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1-Aug-1999.)
|
     |
|
Theorem | ltnegcon2i 8034 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
     |
|
Theorem | lesub0i 8035 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
    
  |
|
Theorem | ltaddposi 8036 |
Adding a positive number to another number increases it. (Contributed
by NM, 25-Aug-1999.)
|
     |
|
Theorem | posdifi 8037 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19-Aug-2001.)
|
     |
|
Theorem | ltnegcon1i 8038 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
     |
|
Theorem | lenegcon1i 8039 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 6-Apr-2005.)
|
     |
|
Theorem | subge0i 8040 |
Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|
  
  |
|
Theorem | ltadd1i 8041 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
  
    |
|
Theorem | leadd1i 8042 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
  
    |
|
Theorem | leadd2i 8043 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
  
    |
|
Theorem | ltsubaddi 8044 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
  
    |
|
Theorem | lesubaddi 8045 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
  
    |
|
Theorem | ltsubadd2i 8046 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
  
    |
|
Theorem | lesubadd2i 8047 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3-Aug-1999.)
|
  
    |
|
Theorem | ltaddsubi 8048 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 14-May-1999.)
|
  
    |
|
Theorem | lt2addi 8049 |
Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
    
    |
|
Theorem | le2addi 8050 |
Adding both side of two inequalities. (Contributed by NM,
16-Sep-1999.)
|
    
    |
|
Theorem | gt0ne0d 8051 |
Positive implies nonzero. (Contributed by Mario Carneiro,
27-May-2016.)
|
     |
|
Theorem | lt0ne0d 8052 |
Something less than zero is not zero. Deduction form. (Contributed by
David Moews, 28-Feb-2017.)
|
     |
|
Theorem | leidd 8053 |
'Less than or equal to' is reflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
     |
|
Theorem | lt0neg1d 8054 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 27-May-2016.)
|
        |
|
Theorem | lt0neg2d 8055 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
   
    |
|
Theorem | le0neg1d 8056 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
        |
|
Theorem | le0neg2d 8057 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
   
    |
|
Theorem | addgegt0d 8058 |
Addition of nonnegative and positive numbers is positive.
(Contributed by Mario Carneiro, 27-May-2016.)
|
             |
|
Theorem | addgt0d 8059 |
Addition of 2 positive numbers is positive. (Contributed by Mario
Carneiro, 27-May-2016.)
|
             |
|
Theorem | addge0d 8060 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27-May-2016.)
|
             |
|
Theorem | ltnegd 8061 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by Mario Carneiro, 27-May-2016.)
|
           |
|
Theorem | lenegd 8062 |
Negative of both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | ltnegcon1d 8063 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
           |
|
Theorem | ltnegcon2d 8064 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
           |
|
Theorem | lenegcon1d 8065 |
Contraposition of negative in 'less than or equal to'. (Contributed
by Mario Carneiro, 27-May-2016.)
|
           |
|
Theorem | lenegcon2d 8066 |
Contraposition of negative in 'less than or equal to'. (Contributed
by Mario Carneiro, 27-May-2016.)
|
           |
|
Theorem | ltaddposd 8067 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | ltaddpos2d 8068 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | ltsubposd 8069 |
Subtracting a positive number from another number decreases it.
(Contributed by Mario Carneiro, 27-May-2016.)
|
       
   |
|
Theorem | posdifd 8070 |
Comparison of two numbers whose difference is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
           |
|
Theorem | addge01d 8071 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | addge02d 8072 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | subge0d 8073 |
Nonnegative subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
     
 
   |
|
Theorem | suble0d 8074 |
Nonpositive subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
       
   |
|
Theorem | subge02d 8075 |
Nonnegative subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
     
 
   |
|
Theorem | ltadd1d 8076 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | leadd1d 8077 |
Addition to both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | leadd2d 8078 |
Addition to both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltsubaddd 8079 |
'Less than' relationship between subtraction and addition. (Contributed
by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | lesubaddd 8080 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltsubadd2d 8081 |
'Less than' relationship between subtraction and addition. (Contributed
by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | lesubadd2d 8082 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltaddsubd 8083 |
'Less than' relationship between subtraction and addition. (Contributed
by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltaddsub2d 8084 |
'Less than' relationship between subtraction and addition. (Contributed
by Mario Carneiro, 29-Dec-2016.)
|
         
     |
|
Theorem | leaddsub2d 8085 |
'Less than or equal to' relationship between and addition and
subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | subled 8086 |
Swap subtrahends in an inequality. (Contributed by Mario Carneiro,
27-May-2016.)
|
               |
|
Theorem | lesubd 8087 |
Swap subtrahends in an inequality. (Contributed by Mario Carneiro,
27-May-2016.)
|
               |
|
Theorem | ltsub23d 8088 |
'Less than' relationship between subtraction and addition.
(Contributed by Mario Carneiro, 27-May-2016.)
|
               |
|
Theorem | ltsub13d 8089 |
'Less than' relationship between subtraction and addition.
(Contributed by Mario Carneiro, 27-May-2016.)
|
               |
|
Theorem | lesub1d 8090 |
Subtraction from both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | lesub2d 8091 |
Subtraction of both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltsub1d 8092 |
Subtraction from both sides of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltsub2d 8093 |
Subtraction of both sides of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
         
     |
|
Theorem | ltadd1dd 8094 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol]
p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
|
         
     |
|
Theorem | ltsub1dd 8095 |
Subtraction from both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
               |
|
Theorem | ltsub2dd 8096 |
Subtraction of both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
               |
|
Theorem | leadd1dd 8097 |
Addition to both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 30-May-2016.)
|
         
     |
|
Theorem | leadd2dd 8098 |
Addition to both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 30-May-2016.)
|
         
     |
|
Theorem | lesub1dd 8099 |
Subtraction from both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 30-May-2016.)
|
           
   |
|
Theorem | lesub2dd 8100 |
Subtraction of both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 30-May-2016.)
|
           
   |