Theorem List for Intuitionistic Logic Explorer - 10801-10900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | absnegd 10801 |
Absolute value of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
              |
|
Theorem | abscjd 10802 |
The absolute value of a number and its conjugate are the same.
Proposition 10-3.7(b) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                 |
|
Theorem | releabsd 10803 |
The real part of a number is less than or equal to its absolute value.
Proposition 10-3.7(d) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
             |
|
Theorem | absexpd 10804 |
Absolute value of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                       |
|
Theorem | abssubd 10805 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by Mario Carneiro,
29-May-2016.)
|
                   |
|
Theorem | absmuld 10806 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                       |
|
Theorem | absdivapd 10807 |
Absolute value distributes over division. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
     #
                    |
|
Theorem | abstrid 10808 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
               
       |
|
Theorem | abs2difd 10809 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
              
        |
|
Theorem | abs2dif2d 10810 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
               
       |
|
Theorem | abs2difabsd 10811 |
Absolute value of difference of absolute values. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                           |
|
Theorem | abs3difd 10812 |
Absolute value of differences around common element. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                             |
|
Theorem | abs3lemd 10813 |
Lemma involving absolute value of differences. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                                     |
|
Theorem | qdenre 10814* |
The rational numbers are dense in : any real number can be
approximated with arbitrary precision by a rational number. For order
theoretic density, see qbtwnre 9875. (Contributed by BJ, 15-Oct-2021.)
|
            |
|
3.7.5 The maximum of two real
numbers
|
|
Theorem | maxcom 10815 |
The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10.
(Contributed by Jim Kingdon, 21-Dec-2021.)
|
            
  |
|
Theorem | maxabsle 10816 |
An upper bound for    . (Contributed by Jim Kingdon,
20-Dec-2021.)
|
      
          |
|
Theorem | maxleim 10817 |
Value of maximum when we know which number is larger. (Contributed by
Jim Kingdon, 21-Dec-2021.)
|
              |
|
Theorem | maxabslemab 10818 |
Lemma for maxabs 10821. A variation of maxleim 10817- that is, if we know
which of two real numbers is larger, we know the maximum of the two.
(Contributed by Jim Kingdon, 21-Dec-2021.)
|
          
          |
|
Theorem | maxabslemlub 10819 |
Lemma for maxabs 10821. A least upper bound for    .
(Contributed by Jim Kingdon, 20-Dec-2021.)
|
                    
    |
|
Theorem | maxabslemval 10820* |
Lemma for maxabs 10821. Value of the supremum. (Contributed by
Jim
Kingdon, 22-Dec-2021.)
|
       
          
            
              
        |
|
Theorem | maxabs 10821 |
Maximum of two real numbers in terms of absolute value. (Contributed by
Jim Kingdon, 20-Dec-2021.)
|
             
          |
|
Theorem | maxcl 10822 |
The maximum of two real numbers is a real number. (Contributed by Jim
Kingdon, 22-Dec-2021.)
|
            |
|
Theorem | maxle1 10823 |
The maximum of two reals is no smaller than the first real. Lemma 3.10 of
[Geuvers], p. 10. (Contributed by Jim
Kingdon, 21-Dec-2021.)
|
            |
|
Theorem | maxle2 10824 |
The maximum of two reals is no smaller than the second real. Lemma 3.10
of [Geuvers], p. 10. (Contributed by Jim
Kingdon, 21-Dec-2021.)
|
            |
|
Theorem | maxleast 10825 |
The maximum of two reals is a least upper bound. Lemma 3.11 of
[Geuvers], p. 10. (Contributed by Jim
Kingdon, 22-Dec-2021.)
|
   
            |
|
Theorem | maxleastb 10826 |
Two ways of saying the maximum of two numbers is less than or equal to a
third. (Contributed by Jim Kingdon, 31-Jan-2022.)
|
       
        |
|
Theorem | maxleastlt 10827 |
The maximum as a least upper bound, in terms of less than. (Contributed
by Jim Kingdon, 9-Feb-2022.)
|
    
             |
|
Theorem | maxleb 10828 |
Equivalence of
and being equal to the maximum of two reals. Lemma
3.12 of [Geuvers], p. 10. (Contributed by
Jim Kingdon, 21-Dec-2021.)
|
              |
|
Theorem | dfabsmax 10829 |
Absolute value of a real number in terms of maximum. Definition 3.13 of
[Geuvers], p. 11. (Contributed by BJ and
Jim Kingdon, 21-Dec-2021.)
|
    
   
      |
|
Theorem | maxltsup 10830 |
Two ways of saying the maximum of two numbers is less than a third.
(Contributed by Jim Kingdon, 10-Feb-2022.)
|
       
        |
|
Theorem | max0addsup 10831 |
The sum of the positive and negative part functions is the absolute value
function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
|
     
                  |
|
Theorem | rexanre 10832* |
Combine two different upper real properties into one. (Contributed by
Mario Carneiro, 8-May-2016.)
|
    
      
         |
|
Theorem | rexico 10833* |
Restrict the base of an upper real quantifier to an upper real set.
(Contributed by Mario Carneiro, 12-May-2016.)
|
          
   
    |
|
Theorem | maxclpr 10834 |
The maximum of two real numbers is one of those numbers if and only if
dichotomy (
) holds. For example, this
can be
combined with zletric 8950 if one is dealing with integers, but real
number
dichotomy in general does not follow from our axioms. (Contributed by Jim
Kingdon, 1-Feb-2022.)
|
              
    |
|
Theorem | zmaxcl 10835 |
The maximum of two integers is an integer. (Contributed by Jim Kingdon,
27-Sep-2022.)
|
            |
|
Theorem | 2zsupmax 10836 |
Two ways to express the maximum of two integers. Because order of
integers is decidable, we have more flexibility than for real numbers.
(Contributed by Jim Kingdon, 22-Jan-2023.)
|
           
 
   |
|
Theorem | fimaxre2 10837* |
A nonempty finite set of real numbers has an upper bound. (Contributed
by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro,
13-Feb-2014.)
|
       |
|
Theorem | negfi 10838* |
The negation of a finite set of real numbers is finite. (Contributed by
AV, 9-Aug-2020.)
|
        |
|
3.7.6 The minimum of two real
numbers
|
|
Theorem | mincom 10839 |
The minimum of two reals is commutative. (Contributed by Jim Kingdon,
8-Feb-2021.)
|
inf      inf  
    |
|
Theorem | minmax 10840 |
Minimum expressed in terms of maximum. (Contributed by Jim Kingdon,
8-Feb-2021.)
|
   inf                  |
|
Theorem | mincl 10841 |
The minumum of two real numbers is a real number. (Contributed by Jim
Kingdon, 25-Apr-2023.)
|
   inf        |
|
Theorem | min1inf 10842 |
The minimum of two numbers is less than or equal to the first.
(Contributed by Jim Kingdon, 8-Feb-2021.)
|
   inf        |
|
Theorem | min2inf 10843 |
The minimum of two numbers is less than or equal to the second.
(Contributed by Jim Kingdon, 9-Feb-2021.)
|
   inf        |
|
Theorem | lemininf 10844 |
Two ways of saying a number is less than or equal to the minimum of two
others. (Contributed by NM, 3-Aug-2007.)
|
    inf  
   
    |
|
Theorem | ltmininf 10845 |
Two ways of saying a number is less than the minimum of two others.
(Contributed by Jim Kingdon, 10-Feb-2022.)
|
    inf           |
|
Theorem | minabs 10846 |
The minimum of two real numbers in terms of absolute value. (Contributed
by Jim Kingdon, 15-May-2023.)
|
   inf         
          |
|
Theorem | minclpr 10847 |
The minimum of two real numbers is one of those numbers if and only if
dichotomy (
) holds. For example, this
can be
combined with zletric 8950 if one is dealing with integers, but real
number
dichotomy in general does not follow from our axioms. (Contributed by Jim
Kingdon, 23-May-2023.)
|
   inf  
      
    |
|
Theorem | rpmincl 10848 |
The minumum of two positive real numbers is a positive real number.
(Contributed by Jim Kingdon, 25-Apr-2023.)
|
   inf        |
|
Theorem | bdtrilem 10849 |
Lemma for bdtri 10850. (Contributed by Steven Nguyen and Jim
Kingdon,
17-May-2023.)
|
    
                            |
|
Theorem | bdtri 10850 |
Triangle inequality for bounded values. (Contributed by Jim Kingdon,
15-May-2023.)
|
    
  inf    
   inf      inf         |
|
Theorem | mul0inf 10851 |
Equality of a product with zero. A bit of a curiosity, in the sense that
theorems like abs00ap 10674 and mulap0bd 8279 may better express the ideas behind
it. (Contributed by Jim Kingdon, 31-Jul-2023.)
|
      inf                 |
|
3.7.7 The maximum of two extended
reals
|
|
Theorem | xrmaxleim 10852 |
Value of maximum when we know which extended real is larger.
(Contributed by Jim Kingdon, 25-Apr-2023.)
|
              |
|
Theorem | xrmaxiflemcl 10853 |
Lemma for xrmaxif 10859. Closure. (Contributed by Jim Kingdon,
29-Apr-2023.)
|
        
   
           
       |
|
Theorem | xrmaxifle 10854 |
An upper bound for    in the extended reals. (Contributed by
Jim Kingdon, 26-Apr-2023.)
|
  
 
       
                   |
|
Theorem | xrmaxiflemab 10855 |
Lemma for xrmaxif 10859. A variation of xrmaxleim 10852- that is, if we know
which of two real numbers is larger, we know the maximum of the two.
(Contributed by Jim Kingdon, 26-Apr-2023.)
|
                    
               |
|
Theorem | xrmaxiflemlub 10856 |
Lemma for xrmaxif 10859. A least upper bound for    .
(Contributed by Jim Kingdon, 28-Apr-2023.)
|
                
                       |
|
Theorem | xrmaxiflemcom 10857 |
Lemma for xrmaxif 10859. Commutativity of an expression which we
will
later show to be the supremum. (Contributed by Jim Kingdon,
29-Apr-2023.)
|
        
   
           
              
                   |
|
Theorem | xrmaxiflemval 10858* |
Lemma for xrmaxif 10859. Value of the supremum. (Contributed by
Jim
Kingdon, 29-Apr-2023.)
|
 
       
                       
       
    |
|
Theorem | xrmaxif 10859 |
Maximum of two extended reals in terms of expressions.
(Contributed by Jim Kingdon, 26-Apr-2023.)
|
           
           
               |
|
Theorem | xrmaxcl 10860 |
The maximum of two extended reals is an extended real. (Contributed by
Jim Kingdon, 29-Apr-2023.)
|
            |
|
Theorem | xrmax1sup 10861 |
An extended real is less than or equal to the maximum of it and another.
(Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon,
30-Apr-2023.)
|
  
   
     |
|
Theorem | xrmax2sup 10862 |
An extended real is less than or equal to the maximum of it and another.
(Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon,
30-Apr-2023.)
|
  
   
     |
|
Theorem | xrmaxrecl 10863 |
The maximum of two real numbers is the same when taken as extended reals
or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.)
|
               
   |
|
Theorem | xrmaxleastlt 10864 |
The maximum as a least upper bound, in terms of less than. (Contributed
by Jim Kingdon, 9-Feb-2022.)
|
  
 
             |
|
Theorem | xrltmaxsup 10865 |
The maximum as a least upper bound. (Contributed by Jim Kingdon,
10-May-2023.)
|
                |
|
Theorem | xrmaxltsup 10866 |
Two ways of saying the maximum of two numbers is less than a third.
(Contributed by Jim Kingdon, 30-Apr-2023.)
|
                |
|
Theorem | xrmaxlesup 10867 |
Two ways of saying the maximum of two numbers is less than or equal to a
third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim
Kingdon, 10-May-2023.)
|
                |
|
Theorem | xrmaxaddlem 10868 |
Lemma for xrmaxadd 10869. The case where is real. (Contributed by
Jim Kingdon, 11-May-2023.)
|
                   
         
    |
|
Theorem | xrmaxadd 10869 |
Distributing addition over maximum. (Contributed by Jim Kingdon,
11-May-2023.)
|
                                  |
|
3.7.8 The minimum of two extended
reals
|
|
Theorem | xrnegiso 10870 |
Negation is an order anti-isomorphism of the extended reals, which is
its own inverse. (Contributed by Jim Kingdon, 2-May-2023.)
|

          |
|
Theorem | infxrnegsupex 10871* |
The infimum of a set of extended reals is the negative of the
supremum of the negatives of its elements. (Contributed by Jim Kingdon,
2-May-2023.)
|
   
         inf       
   
   |
|
Theorem | xrnegcon1d 10872 |
Contraposition law for extended real unary minus. (Contributed by Jim
Kingdon, 2-May-2023.)
|
        
   |
|
Theorem | xrminmax 10873 |
Minimum expressed in terms of maximum. (Contributed by Jim Kingdon,
2-May-2023.)
|
   inf         
          |
|
Theorem | xrmincl 10874 |
The minumum of two extended reals is an extended real. (Contributed by
Jim Kingdon, 3-May-2023.)
|
   inf        |
|
Theorem | xrmin1inf 10875 |
The minimum of two extended reals is less than or equal to the first.
(Contributed by Jim Kingdon, 3-May-2023.)
|
   inf        |
|
Theorem | xrmin2inf 10876 |
The minimum of two extended reals is less than or equal to the second.
(Contributed by Jim Kingdon, 3-May-2023.)
|
   inf        |
|
Theorem | xrmineqinf 10877 |
The minimum of two extended reals is equal to the second if the first is
bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim
Kingdon, 3-May-2023.)
|
   inf  
     |
|
Theorem | xrltmininf 10878 |
Two ways of saying an extended real is less than the minimum of two
others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon,
3-May-2023.)
|
    inf           |
|
Theorem | xrlemininf 10879 |
Two ways of saying a number is less than or equal to the minimum of two
others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim
Kingdon, 4-May-2023.)
|
    inf           |
|
Theorem | xrminltinf 10880 |
Two ways of saying an extended real is greater than the minimum of two
others. (Contributed by Jim Kingdon, 19-May-2023.)
|
   inf    
      |
|
Theorem | xrminrecl 10881 |
The minimum of two real numbers is the same when taken as extended reals
or as reals. (Contributed by Jim Kingdon, 18-May-2023.)
|
   inf      inf        |
|
Theorem | xrminrpcl 10882 |
The minimum of two positive reals is a positive real. (Contributed by Jim
Kingdon, 4-May-2023.)
|
   inf        |
|
Theorem | xrminadd 10883 |
Distributing addition over minimum. (Contributed by Jim Kingdon,
10-May-2023.)
|
   inf                   inf         |
|
Theorem | xrbdtri 10884 |
Triangle inequality for bounded values. (Contributed by Jim Kingdon,
15-May-2023.)
|
  
 
 
  inf         
 inf        inf    
    |
|
Theorem | iooinsup 10885 |
Intersection of two open intervals of extended reals. (Contributed by
NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.)
|
  
 
                     inf         |
|
3.8 Elementary limits and
convergence
|
|
3.8.1 Limits
|
|
Syntax | cli 10886 |
Extend class notation with convergence relation for limits.
|
 |
|
Definition | df-clim 10887* |
Define the limit relation for complex number sequences. See clim 10889
for
its relational expression. (Contributed by NM, 28-Aug-2005.)
|
    
                           |
|
Theorem | climrel 10888 |
The limit relation is a relation. (Contributed by NM, 28-Aug-2005.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
 |
|
Theorem | clim 10889* |
Express the predicate: The limit of complex number sequence is
, or converges to . This means that for any
real
, no matter how
small, there always exists an integer such
that the absolute difference of any later complex number in the sequence
and the limit is less than . (Contributed by NM, 28-Aug-2005.)
(Revised by Mario Carneiro, 28-Apr-2015.)
|
          
    
                 |
|
Theorem | climcl 10890 |
Closure of the limit of a sequence of complex numbers. (Contributed by
NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|

  |
|
Theorem | clim2 10891* |
Express the predicate: The limit of complex number sequence is
, or converges to , with more general
quantifier
restrictions than clim 10889. (Contributed by NM, 6-Jan-2007.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
                                       |
|
Theorem | clim2c 10892* |
Express the predicate
converges to .
(Contributed by NM,
24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                   
      
          
   |
|
Theorem | clim0 10893* |
Express the predicate
converges to .
(Contributed by NM,
24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                 
  
              |
|
Theorem | clim0c 10894* |
Express the predicate
converges to .
(Contributed by NM,
24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                     
  
            |
|
Theorem | climi 10895* |
Convergence of a sequence of complex numbers. (Contributed by NM,
11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                                    |
|
Theorem | climi2 10896* |
Convergence of a sequence of complex numbers. (Contributed by NM,
11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                                  |
|
Theorem | climi0 10897* |
Convergence of a sequence of complex numbers to zero. (Contributed by
NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                                |
|
Theorem | climconst 10898* |
An (eventually) constant sequence converges to its value. (Contributed
by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
                  
  |
|
Theorem | climconst2 10899 |
A constant sequence converges to its value. (Contributed by NM,
6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
          
  |
|
Theorem | climz 10900 |
The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
   
 |