Theorem List for Intuitionistic Logic Explorer - 8101-8200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lttri3d 8101 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
           |
|
Theorem | letri3d 8102 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
           |
|
Theorem | eqleltd 8103 |
Equality in terms of 'less than or equal to', 'less than'. (Contributed
by NM, 7-Apr-2001.)
|
      
    |
|
Theorem | lenltd 8104 |
'Less than or equal to' in terms of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
     
   |
|
Theorem | ltled 8105 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
         |
|
Theorem | ltnsymd 8106 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
         |
|
Theorem | nltled 8107 |
'Not less than ' implies 'less than or equal to'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
    
    |
|
Theorem | lensymd 8108 |
'Less than or equal to' implies 'not less than'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
         |
|
Theorem | mulgt0d 8109 |
The product of two positive numbers is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
             |
|
Theorem | letrd 8110 |
Transitive law deduction for 'less than or equal to'. (Contributed by
NM, 20-May-2005.)
|
             |
|
Theorem | lelttrd 8111 |
Transitive law deduction for 'less than or equal to', 'less than'.
(Contributed by NM, 8-Jan-2006.)
|
             |
|
Theorem | lttrd 8112 |
Transitive law deduction for 'less than'. (Contributed by NM,
9-Jan-2006.)
|
             |
|
Theorem | 0lt1 8113 |
0 is less than 1. Theorem I.21 of [Apostol] p.
20. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 17-Jan-1997.)
|
 |
|
Theorem | ltntri 8114 |
Negative trichotomy property for real numbers. It is well known that we
cannot prove real number trichotomy,
. Does
that mean there is a pair of real numbers where none of those hold (that
is, where we can refute each of those three relationships)? Actually, no,
as shown here. This is another example of distinguishing between being
unable to prove something, or being able to refute it. (Contributed by
Jim Kingdon, 13-Aug-2023.)
|
  

   |
|
4.2.5 Initial properties of the complex
numbers
|
|
Theorem | mul12 8115 |
Commutative/associative law for multiplication. (Contributed by NM,
30-Apr-2005.)
|
        
    |
|
Theorem | mul32 8116 |
Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|
     

      |
|
Theorem | mul31 8117 |
Commutative/associative law. (Contributed by Scott Fenton,
3-Jan-2013.)
|
     

      |
|
Theorem | mul4 8118 |
Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|
    
    
           |
|
Theorem | muladd11 8119 |
A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|
        
  
       |
|
Theorem | 1p1times 8120 |
Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario
Carneiro, 27-May-2016.)
|
    
    |
|
Theorem | peano2cn 8121 |
A theorem for complex numbers analogous the second Peano postulate
peano2 4612. (Contributed by NM, 17-Aug-2005.)
|
     |
|
Theorem | peano2re 8122 |
A theorem for reals analogous the second Peano postulate peano2 4612.
(Contributed by NM, 5-Jul-2005.)
|
     |
|
Theorem | addcom 8123 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
    

   |
|
Theorem | addrid 8124 |
is an additive identity.
(Contributed by Jim Kingdon,
16-Jan-2020.)
|
     |
|
Theorem | addlid 8125 |
is a left identity for
addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
  
  |
|
Theorem | readdcan 8126 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
     

    |
|
Theorem | 00id 8127 |
is its own additive
identity. (Contributed by Scott Fenton,
3-Jan-2013.)
|
   |
|
Theorem | addid1i 8128 |
is an additive identity.
(Contributed by NM, 23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
 
 |
|
Theorem | addid2i 8129 |
is a left identity for
addition. (Contributed by NM,
3-Jan-2013.)
|
   |
|
Theorem | addcomi 8130 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
 
   |
|
Theorem | addcomli 8131 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
 

  |
|
Theorem | mul12i 8132 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew
Salmon, 19-Nov-2011.)
|
         |
|
Theorem | mul32i 8133 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
      
  |
|
Theorem | mul4i 8134 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
  
          |
|
Theorem | addridd 8135 |
is an additive identity.
(Contributed by Mario Carneiro,
27-May-2016.)
|
   
   |
|
Theorem | addlidd 8136 |
is a left identity for
addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
       |
|
Theorem | addcomd 8137 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
           |
|
Theorem | mul12d 8138 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
                 |
|
Theorem | mul32d 8139 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
             
   |
|
Theorem | mul31d 8140 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
             
   |
|
Theorem | mul4d 8141 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
                 
     |
|
Theorem | muladd11r 8142 |
A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|
            

     |
|
Theorem | comraddd 8143 |
Commute RHS addition, in deduction form. (Contributed by David A.
Wheeler, 11-Oct-2018.)
|
             |
|
4.3 Real and complex numbers - basic
operations
|
|
4.3.1 Addition
|
|
Theorem | add12 8144 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
    
        |
|
Theorem | add32 8145 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
     

 
    |
|
Theorem | add32r 8146 |
Commutative/associative law that swaps the last two terms in a triple sum,
rearranging the parentheses. (Contributed by Paul Chapman,
18-May-2007.)
|
    
        |
|
Theorem | add4 8147 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
    
    

          |
|
Theorem | add42 8148 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
    
    

          |
|
Theorem | add12i 8149 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|

    
   |
|
Theorem | add32i 8150 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
  
   
  |
|
Theorem | add4i 8151 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
  

         |
|
Theorem | add42i 8152 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
  

         |
|
Theorem | add12d 8153 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
       
    
    |
|
Theorem | add32d 8154 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
         
   
   |
|
Theorem | add4d 8155 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
           
     

    |
|
Theorem | add42d 8156 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
           
     

    |
|
4.3.2 Subtraction
|
|
Syntax | cmin 8157 |
Extend class notation to include subtraction.
|
 |
|
Syntax | cneg 8158 |
Extend class notation to include unary minus. The symbol is not a
class by itself but part of a compound class definition. We do this
rather than making it a formal function since it is so commonly used.
Note: We use different symbols for unary minus ( ) and subtraction
cmin 8157 ( ) to prevent syntax ambiguity. For example, looking at the
syntax definition co 5895, if we used the same symbol
then "  " could
mean either "
" minus
" ", or
it could represent the (meaningless) operation of
classes "
" and "
" connected with
"operation" " ".
On the other hand, "  
" is unambiguous.
|
  |
|
Definition | df-sub 8159* |
Define subtraction. Theorem subval 8178 shows its value (and describes how
this definition works), Theorem subaddi 8273 relates it to addition, and
Theorems subcli 8262 and resubcli 8249 prove its closure laws. (Contributed
by NM, 26-Nov-1994.)
|
     
   |
|
Definition | df-neg 8160 |
Define the negative of a number (unary minus). We use different symbols
for unary minus ( ) and subtraction ( ) to prevent syntax
ambiguity. See cneg 8158 for a discussion of this. (Contributed by
NM,
10-Feb-1995.)
|

   |
|
Theorem | cnegexlem1 8161 |
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 8164. (Contributed by Eric Schmidt, 22-May-2007.)
|
     

    |
|
Theorem | cnegexlem2 8162 |
Existence of a real number which produces a real number when multiplied
by . (Hint:
zero is such a number, although we don't need to
prove that yet). Lemma for cnegex 8164. (Contributed by Eric Schmidt,
22-May-2007.)
|
 
  |
|
Theorem | cnegexlem3 8163* |
Existence of real number difference. Lemma for cnegex 8164. (Contributed
by Eric Schmidt, 22-May-2007.)
|
 

  
  |
|
Theorem | cnegex 8164* |
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21-May-2007.)
|
  

  |
|
Theorem | cnegex2 8165* |
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
  

  |
|
Theorem | addcan 8166 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
     

    |
|
Theorem | addcan2 8167 |
Cancellation law for addition. (Contributed by NM, 30-Jul-2004.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
     

    |
|
Theorem | addcani 8168 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton,
3-Jan-2013.)
|
  
 
  |
|
Theorem | addcan2i 8169 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 14-May-2003.) (Revised by Scott Fenton,
3-Jan-2013.)
|
  
 
  |
|
Theorem | addcand 8170 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
         
 
   |
|
Theorem | addcan2d 8171 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
         
 
   |
|
Theorem | addcanad 8172 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 8170. (Contributed by David Moews,
28-Feb-2017.)
|
       
       |
|
Theorem | addcan2ad 8173 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 8171. (Contributed by David Moews,
28-Feb-2017.)
|
       
       |
|
Theorem | addneintrd 8174 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 8172. Consequence of addcand 8170.
(Contributed by David Moews, 28-Feb-2017.)
|
         
     |
|
Theorem | addneintr2d 8175 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 8173. Consequence of
addcan2d 8171. (Contributed by David Moews, 28-Feb-2017.)
|
         
     |
|
Theorem | 0cnALT 8176 |
Alternate proof of 0cn 7978. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
 |
|
Theorem | negeu 8177* |
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 8178* |
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 8179 |
Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|
     |
|
Theorem | negeqi 8180 |
Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|
   |
|
Theorem | negeqd 8181 |
Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|
       |
|
Theorem | nfnegd 8182 |
Deduction version of nfneg 8183. (Contributed by NM, 29-Feb-2008.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
          |
|
Theorem | nfneg 8183 |
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 8184 |
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 8185 |
Closure law for subtraction. (Contributed by NM, 10-May-1999.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
    
  |
|
Theorem | negcl 8186 |
Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|
    |
|
Theorem | negicn 8187 |
 is a complex number
(common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
  |
|
Theorem | subf 8188 |
Subtraction is an operation on the complex numbers. (Contributed by NM,
4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
      |
|
Theorem | subadd 8189 |
Relationship between subtraction and addition. (Contributed by NM,
20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
     
     |
|
Theorem | subadd2 8190 |
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
     
     |
|
Theorem | subsub23 8191 |
Swap subtrahend and result of subtraction. (Contributed by NM,
14-Dec-2007.)
|
     
     |
|
Theorem | pncan 8192 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
      
  |
|
Theorem | pncan2 8193 |
Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|
      
  |
|
Theorem | pncan3 8194 |
Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|
    
 
  |
|
Theorem | npcan 8195 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
      
  |
|
Theorem | addsubass 8196 |
Associative-type law for addition and subtraction. (Contributed by NM,
6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|
     

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

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

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

        |