Theorem List for Intuitionistic Logic Explorer - 11101-11200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | absgt0ap 11101 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
  #        |
|
Theorem | nnabscl 11102 |
The absolute value of a nonzero integer is a positive integer.
(Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Andrew
Salmon, 25-May-2011.)
|
  
      |
|
Theorem | abssub 11103 |
Swapping order of subtraction doesn't change the absolute value.
(Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro,
29-May-2016.)
|
                 |
|
Theorem | abssubge0 11104 |
Absolute value of a nonnegative difference. (Contributed by NM,
14-Feb-2008.)
|
 
           |
|
Theorem | abssuble0 11105 |
Absolute value of a nonpositive difference. (Contributed by FL,
3-Jan-2008.)
|
 
           |
|
Theorem | abstri 11106 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by NM,
7-Mar-2005.) (Proof shortened by
Mario Carneiro, 29-May-2016.)
|
      
 
            |
|
Theorem | abs3dif 11107 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
                         |
|
Theorem | abs2dif 11108 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
                     |
|
Theorem | abs2dif2 11109 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
             
       |
|
Theorem | abs2difabs 11110 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
                         |
|
Theorem | recan 11111* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
        
 
     
   |
|
Theorem | absf 11112 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
     |
|
Theorem | abs3lem 11113 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
    
         
                    |
|
Theorem | fzomaxdiflem 11114 |
Lemma for fzomaxdif 11115. (Contributed by Stefan O'Rear,
6-Sep-2015.)
|
    ..^  ..^          ..^     |
|
Theorem | fzomaxdif 11115 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
   ..^
 ..^         ..^     |
|
Theorem | cau3lem 11116* |
Lemma for cau3 11117. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
          
                

                                  
                                   
    
                                                         
 
                           
                                |
|
Theorem | cau3 11117* |
Convert between three-quantifier and four-quantifier versions of the
Cauchy criterion. (In particular, the four-quantifier version has no
occurrence of in
the assertion, so it can be used with rexanuz 10990
and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
|
                                   
          
            
         |
|
Theorem | cau4 11118* |
Change the base of a Cauchy criterion. (Contributed by Mario
Carneiro, 18-Mar-2014.)
|
                      
               
           
                  |
|
Theorem | caubnd2 11119* |
A Cauchy sequence of complex numbers is eventually bounded.
(Contributed by Mario Carneiro, 14-Feb-2014.)
|
                                   
               |
|
Theorem | amgm2 11120 |
Arithmetic-geometric mean inequality for
. (Contributed by
Mario Carneiro, 2-Jul-2014.)
|
    
          
   |
|
Theorem | sqrtthi 11121 |
Square root theorem. Theorem I.35 of [Apostol]
p. 29. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
             |
|
Theorem | sqrtcli 11122 |
The square root of a nonnegative real is a real. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
    
  |
|
Theorem | sqrtgt0i 11123 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
       |
|
Theorem | sqrtmsqi 11124 |
Square root of square. (Contributed by NM, 2-Aug-1999.)
|
         |
|
Theorem | sqrtsqi 11125 |
Square root of square. (Contributed by NM, 11-Aug-1999.)
|
           |
|
Theorem | sqsqrti 11126 |
Square of square root. (Contributed by NM, 11-Aug-1999.)
|
           |
|
Theorem | sqrtge0i 11127 |
The square root of a nonnegative real is nonnegative. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
       |
|
Theorem | absidi 11128 |
A nonnegative number is its own absolute value. (Contributed by NM,
2-Aug-1999.)
|
    
  |
|
Theorem | absnidi 11129 |
A negative number is the negative of its own absolute value.
(Contributed by NM, 2-Aug-1999.)
|
    
   |
|
Theorem | leabsi 11130 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 2-Aug-1999.)
|
     |
|
Theorem | absrei 11131 |
Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|
   
         |
|
Theorem | sqrtpclii 11132 |
The square root of a positive real is a real. (Contributed by Mario
Carneiro, 6-Sep-2013.)
|
   
 |
|
Theorem | sqrtgt0ii 11133 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
     |
|
Theorem | sqrt11i 11134 |
The square root function is one-to-one. (Contributed by NM,
27-Jul-1999.)
|
               |
|
Theorem | sqrtmuli 11135 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
                     |
|
Theorem | sqrtmulii 11136 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
                 |
|
Theorem | sqrtmsq2i 11137 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.)
|
             |
|
Theorem | sqrtlei 11138 |
Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|
               |
|
Theorem | sqrtlti 11139 |
Square root is strictly monotonic. (Contributed by Roy F. Longton,
8-Aug-2005.)
|
               |
|
Theorem | abslti 11140 |
Absolute value and 'less than' relation. (Contributed by NM,
6-Apr-2005.)
|
          |
|
Theorem | abslei 11141 |
Absolute value and 'less than or equal to' relation. (Contributed by
NM, 6-Apr-2005.)
|
          |
|
Theorem | absvalsqi 11142 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
               |
|
Theorem | absvalsq2i 11143 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
                           |
|
Theorem | abscli 11144 |
Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|
   
 |
|
Theorem | absge0i 11145 |
Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|
     |
|
Theorem | absval2i 11146 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 2-Oct-1999.)
|
   
                       |
|
Theorem | abs00i 11147 |
The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of [Gleason] p.
133. (Contributed by NM,
28-Jul-1999.)
|
    
  |
|
Theorem | absgt0api 11148 |
The absolute value of a nonzero number is positive. Remark in [Apostol]
p. 363. (Contributed by NM, 1-Oct-1999.)
|
 #       |
|
Theorem | absnegi 11149 |
Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|
    
     |
|
Theorem | abscji 11150 |
The absolute value of a number and its conjugate are the same.
Proposition 10-3.7(b) of [Gleason] p.
133. (Contributed by NM,
2-Oct-1999.)
|
             |
|
Theorem | releabsi 11151 |
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 NM,
2-Oct-1999.)
|
   
     |
|
Theorem | abssubi 11152 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by NM, 1-Oct-1999.)
|
             |
|
Theorem | absmuli 11153 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
NM, 1-Oct-1999.)
|
                 |
|
Theorem | sqabsaddi 11154 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 2-Oct-1999.)
|
    
                                      |
|
Theorem | sqabssubi 11155 |
Square of absolute value of difference. (Contributed by Steve
Rodriguez, 20-Jan-2007.)
|
                                           |
|
Theorem | absdivapzi 11156 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
 #                   |
|
Theorem | abstrii 11157 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. This is Metamath 100
proof #91. (Contributed by NM,
2-Oct-1999.)
|
   
 
           |
|
Theorem | abs3difi 11158 |
Absolute value of differences around common element. (Contributed by
NM, 2-Oct-1999.)
|
                     |
|
Theorem | abs3lemi 11159 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
       
                   |
|
Theorem | rpsqrtcld 11160 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
         |
|
Theorem | sqrtgt0d 11161 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
         |
|
Theorem | absnidd 11162 |
A negative number is the negative of its own absolute value.
(Contributed by Mario Carneiro, 29-May-2016.)
|
            |
|
Theorem | leabsd 11163 |
A real number is less than or equal to its absolute value. (Contributed
by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | absred 11164 |
Absolute value of a real number. (Contributed by Mario Carneiro,
29-May-2016.)
|
                 |
|
Theorem | resqrtcld 11165 |
The square root of a nonnegative real is a real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
           |
|
Theorem | sqrtmsqd 11166 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
             |
|
Theorem | sqrtsqd 11167 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
               |
|
Theorem | sqrtge0d 11168 |
The square root of a nonnegative real is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
           |
|
Theorem | absidd 11169 |
A nonnegative number is its own absolute value. (Contributed by Mario
Carneiro, 29-May-2016.)
|
           |
|
Theorem | sqrtdivd 11170 |
Square root distributes over division. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                         |
|
Theorem | sqrtmuld 11171 |
Square root distributes over multiplication. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                           |
|
Theorem | sqrtsq2d 11172 |
Relationship between square root and squares. (Contributed by Mario
Carneiro, 29-May-2016.)
|
             
       |
|
Theorem | sqrtled 11173 |
Square root is monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
                     |
|
Theorem | sqrtltd 11174 |
Square root is strictly monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
                     |
|
Theorem | sqr11d 11175 |
The square root function is one-to-one. (Contributed by Mario Carneiro,
29-May-2016.)
|
                     |
|
Theorem | absltd 11176 |
Absolute value and 'less than' relation. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                |
|
Theorem | absled 11177 |
Absolute value and 'less than or equal to' relation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                |
|
Theorem | abssubge0d 11178 |
Absolute value of a nonnegative difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                 |
|
Theorem | abssuble0d 11179 |
Absolute value of a nonpositive difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                 |
|
Theorem | absdifltd 11180 |
The absolute value of a difference and 'less than' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
                
      |
|
Theorem | absdifled 11181 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
                
      |
|
Theorem | icodiamlt 11182 |
Two elements in a half-open interval have separation strictly less than
the difference between the endpoints. (Contributed by Stefan O'Rear,
12-Sep-2014.)
|
    
                    |
|
Theorem | abscld 11183 |
Real closure of absolute value. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | absvalsqd 11184 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                   |
|
Theorem | absvalsq2d 11185 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                               |
|
Theorem | absge0d 11186 |
Absolute value is nonnegative. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | absval2d 11187 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by Mario Carneiro, 29-May-2016.)
|
                               |
|
Theorem | abs00d 11188 |
The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
           |
|
Theorem | absne0d 11189 |
The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
           |
|
Theorem | absrpclapd 11190 |
The absolute value of a complex number apart from zero is a positive
real. (Contributed by Jim Kingdon, 13-Aug-2021.)
|
   #         |
|
Theorem | absnegd 11191 |
Absolute value of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
              |
|
Theorem | abscjd 11192 |
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 11193 |
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 11194 |
Absolute value of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                       |
|
Theorem | abssubd 11195 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by Mario Carneiro,
29-May-2016.)
|
                   |
|
Theorem | absmuld 11196 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                       |
|
Theorem | absdivapd 11197 |
Absolute value distributes over division. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
     #
                    |
|
Theorem | abstrid 11198 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
               
       |
|
Theorem | abs2difd 11199 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
              
        |
|
Theorem | abs2dif2d 11200 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
               
       |