Theorem List for Intuitionistic Logic Explorer - 9801-9900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xnegeq 9801 |
Equality of two extended numbers with  in front of them.
(Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro,
20-Aug-2015.)
|
       |
|
Theorem | xnegpnf 9802 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.)
|

 |
|
Theorem | xnegmnf 9803 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|

 |
|
Theorem | rexneg 9804 |
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|
      |
|
Theorem | xneg0 9805 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
   |
|
Theorem | xnegcl 9806 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
     |
|
Theorem | xnegneg 9807 |
Extended real version of negneg 8184. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
      |
|
Theorem | xneg11 9808 |
Extended real version of neg11 8185. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
      
   |
|
Theorem | xltnegi 9809 |
Forward direction of xltneg 9810. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
         |
|
Theorem | xltneg 9810 |
Extended real version of ltneg 8396. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
     
     |
|
Theorem | xleneg 9811 |
Extended real version of leneg 8399. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
     
     |
|
Theorem | xlt0neg1 9812 |
Extended real version of lt0neg1 8402. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
 
     |
|
Theorem | xlt0neg2 9813 |
Extended real version of lt0neg2 8403. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
   
   |
|
Theorem | xle0neg1 9814 |
Extended real version of le0neg1 8404. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
 
     |
|
Theorem | xle0neg2 9815 |
Extended real version of le0neg2 8405. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
   
   |
|
Theorem | xrpnfdc 9816 |
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13-Apr-2023.)
|
 DECID   |
|
Theorem | xrmnfdc 9817 |
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13-Apr-2023.)
|
 DECID   |
|
Theorem | xaddf 9818 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 21-Aug-2015.)
|
   
    |
|
Theorem | xaddval 9819 |
Value of the extended real addition operation. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
       
 
      
 
  
         
          |
|
Theorem | xaddpnf1 9820 |
Addition of positive infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
      
  |
|
Theorem | xaddpnf2 9821 |
Addition of positive infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
      
  |
|
Theorem | xaddmnf1 9822 |
Addition of negative infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
      
  |
|
Theorem | xaddmnf2 9823 |
Addition of negative infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
      
  |
|
Theorem | pnfaddmnf 9824 |
Addition of positive and negative infinity. This is often taken to be a
"null" value or out of the domain, but we define it (somewhat
arbitrarily)
to be zero so that the resulting function is total, which simplifies
proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
  
 |
|
Theorem | mnfaddpnf 9825 |
Addition of negative and positive infinity. This is often taken to be a
"null" value or out of the domain, but we define it (somewhat
arbitrarily)
to be zero so that the resulting function is total, which simplifies
proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
  
 |
|
Theorem | rexadd 9826 |
The extended real addition operation when both arguments are real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
            |
|
Theorem | rexsub 9827 |
Extended real subtraction when both arguments are real. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
             |
|
Theorem | rexaddd 9828 |
The extended real addition operation when both arguments are real.
Deduction version of rexadd 9826. (Contributed by Glauco Siliprandi,
24-Dec-2020.)
|
              |
|
Theorem | xnegcld 9829 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
    
  |
|
Theorem | xrex 9830 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
 |
|
Theorem | xaddnemnf 9831 |
Closure of extended real addition in the subset
 .
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
  
 
         |
|
Theorem | xaddnepnf 9832 |
Closure of extended real addition in the subset
 .
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
  
 
         |
|
Theorem | xnegid 9833 |
Extended real version of negid 8181. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
         |
|
Theorem | xaddcl 9834 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
       
  |
|
Theorem | xaddcom 9835 |
The extended real addition operation is commutative. (Contributed by NM,
26-Dec-2011.)
|
       
       |
|
Theorem | xaddid1 9836 |
Extended real version of addid1 8072. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
        |
|
Theorem | xaddid2 9837 |
Extended real version of addid2 8073. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
     
  |
|
Theorem | xaddid1d 9838 |
is a right identity for
extended real addition. (Contributed by
Glauco Siliprandi, 17-Aug-2020.)
|
          |
|
Theorem | xnn0lenn0nn0 9839 |
An extended nonnegative integer which is less than or equal to a
nonnegative integer is a nonnegative integer. (Contributed by AV,
24-Nov-2021.)
|
  NN0*    |
|
Theorem | xnn0le2is012 9840 |
An extended nonnegative integer which is less than or equal to 2 is either
0 or 1 or 2. (Contributed by AV, 24-Nov-2021.)
|
  NN0*
     |
|
Theorem | xnn0xadd0 9841 |
The sum of two extended nonnegative integers is iff each of the two
extended nonnegative integers is . (Contributed by AV,
14-Dec-2020.)
|
  NN0* NN0*            |
|
Theorem | xnegdi 9842 |
Extended real version of negdi 8191. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                   |
|
Theorem | xaddass 9843 |
Associativity of extended real addition. The correct condition here is
"it is not the case that both and appear as one of
  ,
i.e.       ", but this
condition is difficult to work with, so we break the theorem into two
parts: this one, where is not present in   , and
xaddass2 9844, where is not present. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
  
 
 
           
            |
|
Theorem | xaddass2 9844 |
Associativity of extended real addition. See xaddass 9843 for notes on the
hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
  
 
 
           
            |
|
Theorem | xpncan 9845 |
Extended real version of pncan 8140. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                |
|
Theorem | xnpcan 9846 |
Extended real version of npcan 8143. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                |
|
Theorem | xleadd1a 9847 |
Extended real version of leadd1 8364; note that the converse implication is
not true, unlike the real version (for example but
  
     ).
(Contributed by Mario Carneiro,
20-Aug-2015.)
|
  

     
       |
|
Theorem | xleadd2a 9848 |
Commuted form of xleadd1a 9847. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
  

     
       |
|
Theorem | xleadd1 9849 |
Weakened version of xleadd1a 9847 under which the reverse implication is
true. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
                 |
|
Theorem | xltadd1 9850 |
Extended real version of ltadd1 8363. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
|
                 |
|
Theorem | xltadd2 9851 |
Extended real version of ltadd2 8353. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
                 |
|
Theorem | xaddge0 9852 |
The sum of nonnegative extended reals is nonnegative. (Contributed by
Mario Carneiro, 21-Aug-2015.)
|
  
   
       |
|
Theorem | xle2add 9853 |
Extended real version of le2add 8378. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
  
 
   
     
        |
|
Theorem | xlt2add 9854 |
Extended real version of lt2add 8379. Note that ltleadd 8380, which has
weaker assumptions, is not true for the extended reals (since
fails). (Contributed by Mario
Carneiro,
23-Aug-2015.)
|
  
 
         
        |
|
Theorem | xsubge0 9855 |
Extended real version of subge0 8409. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
         
   |
|
Theorem | xposdif 9856 |
Extended real version of posdif 8389. (Contributed by Mario Carneiro,
24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|
             |
|
Theorem | xlesubadd 9857 |
Under certain conditions, the conclusion of lesubadd 8368 is true even in the
extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
  
          
        |
|
Theorem | xaddcld 9858 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28-May-2016.)
|
            |
|
Theorem | xadd4d 9859 |
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 8103. (Contributed by Alexander van der Vekens,
21-Dec-2017.)
|
 
       
                                       |
|
Theorem | xnn0add4d 9860 |
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9859. (Contributed by AV,
12-Dec-2020.)
|
 NN0*  NN0*  NN0*  NN0*                                  |
|
Theorem | xleaddadd 9861 |
Cancelling a factor of two in (expressed as addition rather than
as a factor to avoid extended real multiplication). (Contributed by Jim
Kingdon, 18-Apr-2023.)
|
        
        |
|
4.5.3 Real number intervals
|
|
Syntax | cioo 9862 |
Extend class notation with the set of open intervals of extended reals.
|
 |
|
Syntax | cioc 9863 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
![(,] (,]](_ioc.gif) |
|
Syntax | cico 9864 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
 |
|
Syntax | cicc 9865 |
Extend class notation with the set of closed intervals of extended
reals.
|
![[,] [,]](_icc.gif) |
|
Definition | df-ioo 9866* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
   
    |
|
Definition | df-ioc 9867* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
   
    |
|
Definition | df-ico 9868* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
   
    |
|
Definition | df-icc 9869* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
   
    |
|
Theorem | ixxval 9870* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
            

              |
|
Theorem | elixx1 9871* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
            

              |
|
Theorem | ixxf 9872* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro,
16-Nov-2013.)
|
             
     |
|
Theorem | ixxex 9873* |
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
            |
|
Theorem | ixxssxr 9874* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
              
 |
|
Theorem | elixx3g 9875* |
Membership in a set of open intervals of extended reals. We use the
fact that an operation's value is empty outside of its domain to show
and .
(Contributed by Mario Carneiro,
3-Nov-2013.)
|
                            |
|
Theorem | ixxssixx 9876* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
                       
         

  
       
     |
|
Theorem | ixxdisj 9877* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
                       
                       |
|
Theorem | ixxss1 9878* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
                                                   |
|
Theorem | ixxss2 9879* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
                               
     
  
          |
|
Theorem | ixxss12 9880* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
                                     
       
                         |
|
Theorem | iooex 9881 |
The set of open intervals of extended reals exists. (Contributed by NM,
6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
 |
|
Theorem | iooval 9882* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
      
      |
|
Theorem | iooidg 9883 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
       |
|
Theorem | elioo3g 9884 |
Membership in a set of open intervals of extended reals. We use the
fact that an operation's value is empty outside of its domain to show
and .
(Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
      
      |
|
Theorem | elioo1 9885 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
             |
|
Theorem | elioore 9886 |
A member of an open interval of reals is a real. (Contributed by NM,
17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
    
  |
|
Theorem | lbioog 9887 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
         |
|
Theorem | ubioog 9888 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
         |
|
Theorem | iooval2 9889* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
      
      |
|
Theorem | iooss1 9890 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
 
           |
|
Theorem | iooss2 9891 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
 
           |
|
Theorem | iocval 9892* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
     ![(,] (,]](_ioc.gif) 
      |
|
Theorem | icoval 9893* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
      
 
    |
|
Theorem | iccval 9894* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
     ![[,] [,]](_icc.gif) 
 
    |
|
Theorem | elioo2 9895 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
             |
|
Theorem | elioc1 9896 |
Membership in an open-below, closed-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
      ![(,] (,]](_ioc.gif)       |
|
Theorem | elico1 9897 |
Membership in a closed-below, open-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
        
    |
|
Theorem | elicc1 9898 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
      ![[,] [,]](_icc.gif)  
    |
|
Theorem | iccid 9899 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
   ![[,] [,]](_icc.gif)      |
|
Theorem | icc0r 9900 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
      ![[,] [,]](_icc.gif) 
   |