Theorem List for Intuitionistic Logic Explorer - 7201-7300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 0cnALT 7201 |
Alternate proof of 0cn 7019. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
 |
|
Theorem | negeu 7202* |
Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
     
  |
|
Theorem | subval 7203* |
Value of subtraction, which is the (unique) element such that
.
(Contributed by NM, 4-Aug-2007.) (Revised by Mario
Carneiro, 2-Nov-2013.)
|
    
 

    |
|
Theorem | negeq 7204 |
Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|
     |
|
Theorem | negeqi 7205 |
Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|
   |
|
Theorem | negeqd 7206 |
Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|
       |
|
Theorem | nfnegd 7207 |
Deduction version of nfneg 7208. (Contributed by NM, 29-Feb-2008.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
          |
|
Theorem | nfneg 7208 |
Bound-variable hypothesis builder for the negative of a complex number.
(Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
      |
|
Theorem | csbnegg 7209 |
Move class substitution in and out of the negative of a number.
(Contributed by NM, 1-Mar-2008.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
   ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)   |
|
Theorem | subcl 7210 |
Closure law for subtraction. (Contributed by NM, 10-May-1999.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
    
  |
|
Theorem | negcl 7211 |
Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|
    |
|
Theorem | negicn 7212 |
 is a complex number
(common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
  |
|
Theorem | subf 7213 |
Subtraction is an operation on the complex numbers. (Contributed by NM,
4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
      |
|
Theorem | subadd 7214 |
Relationship between subtraction and addition. (Contributed by NM,
20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
     
     |
|
Theorem | subadd2 7215 |
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | subsub23 7216 |
Swap subtrahend and result of subtraction. (Contributed by NM,
14-Dec-2007.)
|
     
     |
|
Theorem | pncan 7217 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
      
  |
|
Theorem | pncan2 7218 |
Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|
      
  |
|
Theorem | pncan3 7219 |
Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|
    
 
  |
|
Theorem | npcan 7220 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
      
  |
|
Theorem | addsubass 7221 |
Associative-type law for addition and subtraction. (Contributed by NM,
6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|
     

      |
|
Theorem | addsub 7222 |
Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
     

      |
|
Theorem | subadd23 7223 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 1-Feb-2007.)
|
     

      |
|
Theorem | addsub12 7224 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 8-Feb-2005.)
|
        
    |
|
Theorem | 2addsub 7225 |
Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|
    
      

        |
|
Theorem | addsubeq4 7226 |
Relation between sums and differences. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
    
    

        |
|
Theorem | pncan3oi 7227 |
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 7288 and pncan 7217, this order happens often when
applying
"operations to both sides" so create a theorem specifically
for it. A
deduction version of this is available as pncand 7323. (Contributed by
David A. Wheeler, 11-Oct-2018.)
|
  

 |
|
Theorem | mvrraddi 7228 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
  

 |
|
Theorem | mvlladdi 7229 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
 
   |
|
Theorem | subid 7230 |
Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.)
(Revised by Mario Carneiro, 27-May-2016.)
|
  
  |
|
Theorem | subid1 7231 |
Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised
by Mario Carneiro, 27-May-2016.)
|
     |
|
Theorem | npncan 7232 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
     
       |
|
Theorem | nppcan 7233 |
Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|
       

    |
|
Theorem | nnpcan 7234 |
Cancellation law for subtraction: ((a-b)-c)+b = a-c holds for complex
numbers a,b,c. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
|
       

    |
|
Theorem | nppcan3 7235 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
     

      |
|
Theorem | subcan2 7236 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
     
 
   |
|
Theorem | subeq0 7237 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16-Nov-1999.)
|
     
   |
|
Theorem | npncan2 7238 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
21-Jun-2013.)
|
      
 
  |
|
Theorem | subsub2 7239 |
Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
        
    |
|
Theorem | nncan 7240 |
Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
    
 
  |
|
Theorem | subsub 7241 |
Law for double subtraction. (Contributed by NM, 13-May-2004.)
|
             |
|
Theorem | nppcan2 7242 |
Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|
     
 

    |
|
Theorem | subsub3 7243 |
Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|
             |
|
Theorem | subsub4 7244 |
Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
     

      |
|
Theorem | sub32 7245 |
Swap the second and third terms in a double subtraction. (Contributed by
NM, 19-Aug-2005.)
|
     

      |
|
Theorem | nnncan 7246 |
Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|
     
 

    |
|
Theorem | nnncan1 7247 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
     
       |
|
Theorem | nnncan2 7248 |
Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
|
     
       |
|
Theorem | npncan3 7249 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
     
       |
|
Theorem | pnpcan 7250 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
     

      |
|
Theorem | pnpcan2 7251 |
Cancellation law for mixed addition and subtraction. (Contributed by
Scott Fenton, 9-Jun-2006.)
|
     

      |
|
Theorem | pnncan 7252 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
     
       |
|
Theorem | ppncan 7253 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.)
|
     
       |
|
Theorem | addsub4 7254 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 4-Mar-2005.)
|
    
    

          |
|
Theorem | subadd4 7255 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 24-Aug-2006.)
|
    
    
      
    |
|
Theorem | sub4 7256 |
Rearrangement of 4 terms in a subtraction. (Contributed by NM,
23-Nov-2007.)
|
    
    
      
    |
|
Theorem | neg0 7257 |
Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|

 |
|
Theorem | negid 7258 |
Addition of a number and its negative. (Contributed by NM,
14-Mar-2005.)
|
   
  |
|
Theorem | negsub 7259 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
          |
|
Theorem | subneg 7260 |
Relationship between subtraction and negative. (Contributed by NM,
10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
          |
|
Theorem | negneg 7261 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by NM,
12-Jan-2002.) (Revised by Mario
Carneiro, 27-May-2016.)
|
     |
|
Theorem | neg11 7262 |
Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by
Mario Carneiro, 27-May-2016.)
|
     
   |
|
Theorem | negcon1 7263 |
Negative contraposition law. (Contributed by NM, 9-May-2004.)
|
    
    |
|
Theorem | negcon2 7264 |
Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|
    
    |
|
Theorem | negeq0 7265 |
A number is zero iff its negative is zero. (Contributed by NM,
12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
      |
|
Theorem | subcan 7266 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Revised by Mario Carneiro, 27-May-2016.)
|
     
 
   |
|
Theorem | negsubdi 7267 |
Distribution of negative over subtraction. (Contributed by NM,
15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | negdi 7268 |
Distribution of negative over addition. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
     
      |
|
Theorem | negdi2 7269 |
Distribution of negative over addition. (Contributed by NM,
1-Jan-2006.)
|
     
     |
|
Theorem | negsubdi2 7270 |
Distribution of negative over subtraction. (Contributed by NM,
4-Oct-1999.)
|
     
    |
|
Theorem | neg2sub 7271 |
Relationship between subtraction and negative. (Contributed by Paul
Chapman, 8-Oct-2007.)
|
           |
|
Theorem | renegcl 7272 |
Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|
    |
|
Theorem | renegcli 7273 |
Closure law for negative of reals. (Note: this inference proof style
and the deduction theorem usage in renegcl 7272 is deprecated, but is
retained for its demonstration value.) (Contributed by NM,
17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
  |
|
Theorem | resubcli 7274 |
Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.)
(Revised by Mario Carneiro, 27-May-2016.)
|
 
 |
|
Theorem | resubcl 7275 |
Closure law for subtraction of reals. (Contributed by NM,
20-Jan-1997.)
|
    
  |
|
Theorem | negreb 7276 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
      |
|
Theorem | peano2cnm 7277 |
"Reverse" second Peano postulate analog for complex numbers: A
complex
number minus 1 is a complex number. (Contributed by Alexander van der
Vekens, 18-Mar-2018.)
|
     |
|
Theorem | peano2rem 7278 |
"Reverse" second Peano postulate analog for reals. (Contributed by
NM,
6-Feb-2007.)
|
     |
|
Theorem | negcli 7279 |
Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|
  |
|
Theorem | negidi 7280 |
Addition of a number and its negative. (Contributed by NM,
26-Nov-1994.)
|
    |
|
Theorem | negnegi 7281 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by NM,
8-Feb-1995.) (Proof shortened by
Andrew Salmon, 22-Oct-2011.)
|
   |
|
Theorem | subidi 7282 |
Subtraction of a number from itself. (Contributed by NM,
26-Nov-1994.)
|
 
 |
|
Theorem | subid1i 7283 |
Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|
 
 |
|
Theorem | negne0bi 7284 |
A number is nonzero iff its negative is nonzero. (Contributed by NM,
10-Aug-1999.)
|
 
  |
|
Theorem | negrebi 7285 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|
 
  |
|
Theorem | negne0i 7286 |
The negative of a nonzero number is nonzero. (Contributed by NM,
30-Jul-2004.)
|

 |
|
Theorem | subcli 7287 |
Closure law for subtraction. (Contributed by NM, 26-Nov-1994.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
 
 |
|
Theorem | pncan3i 7288 |
Subtraction and addition of equals. (Contributed by NM,
26-Nov-1994.)
|
     |
|
Theorem | negsubi 7289 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by NM, 26-Nov-1994.) (Proof shortened by Andrew
Salmon, 22-Oct-2011.)
|
  
   |
|
Theorem | subnegi 7290 |
Relationship between subtraction and negative. (Contributed by NM,
1-Dec-2005.)
|
  
   |
|
Theorem | subeq0i 7291 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8-May-1999.)
|
  
  |
|
Theorem | neg11i 7292 |
Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|
     |
|
Theorem | negcon1i 7293 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
  
  |
|
Theorem | negcon2i 7294 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
     |
|
Theorem | negdii 7295 |
Distribution of negative over addition. (Contributed by NM,
28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
  
     |
|
Theorem | negsubdii 7296 |
Distribution of negative over subtraction. (Contributed by NM,
6-Aug-1999.)
|
  
    |
|
Theorem | negsubdi2i 7297 |
Distribution of negative over subtraction. (Contributed by NM,
1-Oct-1999.)
|
  
   |
|
Theorem | subaddi 7298 |
Relationship between subtraction and addition. (Contributed by NM,
26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
  
 
  |
|
Theorem | subadd2i 7299 |
Relationship between subtraction and addition. (Contributed by NM,
15-Dec-2006.)
|
  
 
  |
|
Theorem | subaddrii 7300 |
Relationship between subtraction and addition. (Contributed by NM,
16-Dec-2006.)
|

  
 |