Type | Label | Description |
Statement |
|
Theorem | abssubap0 11101 |
If the absolute value of a complex number is less than a real, its
difference from the real is apart from zero. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
       
 #   |
|
Theorem | abssubne0 11102 |
If the absolute value of a complex number is less than a real, its
difference from the real is nonzero. See also abssubap0 11101 which is the
same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.)
|
       
   |
|
Theorem | absdiflt 11103 |
The absolute value of a difference and 'less than' relation. (Contributed
by Paul Chapman, 18-Sep-2007.)
|
             
     |
|
Theorem | absdifle 11104 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Paul Chapman, 18-Sep-2007.)
|
             
     |
|
Theorem | elicc4abs 11105 |
Membership in a symmetric closed real interval. (Contributed by Stefan
O'Rear, 16-Nov-2014.)
|
        ![[,] [,]](_icc.gif)             |
|
Theorem | lenegsq 11106 |
Comparison to a nonnegative number based on comparison to squares.
(Contributed by NM, 16-Jan-2006.)
|
 
        
       |
|
Theorem | releabs 11107 |
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,
1-Apr-2005.)
|
           |
|
Theorem | recvalap 11108 |
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
  #   
                |
|
Theorem | absidm 11109 |
The absolute value function is idempotent. (Contributed by NM,
20-Nov-2004.)
|
               |
|
Theorem | absgt0ap 11110 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
  #        |
|
Theorem | nnabscl 11111 |
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 11112 |
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 11113 |
Absolute value of a nonnegative difference. (Contributed by NM,
14-Feb-2008.)
|
 
           |
|
Theorem | abssuble0 11114 |
Absolute value of a nonpositive difference. (Contributed by FL,
3-Jan-2008.)
|
 
           |
|
Theorem | abstri 11115 |
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 11116 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
                         |
|
Theorem | abs2dif 11117 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
                     |
|
Theorem | abs2dif2 11118 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
             
       |
|
Theorem | abs2difabs 11119 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
                         |
|
Theorem | recan 11120* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
        
 
     
   |
|
Theorem | absf 11121 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
     |
|
Theorem | abs3lem 11122 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
    
         
                    |
|
Theorem | fzomaxdiflem 11123 |
Lemma for fzomaxdif 11124. (Contributed by Stefan O'Rear,
6-Sep-2015.)
|
    ..^  ..^          ..^     |
|
Theorem | fzomaxdif 11124 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
   ..^
 ..^         ..^     |
|
Theorem | cau3lem 11125* |
Lemma for cau3 11126. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
          
                

                                  
                                   
    
                                                         
 
                           
                                |
|
Theorem | cau3 11126* |
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 10999
and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
|
                                   
          
            
         |
|
Theorem | cau4 11127* |
Change the base of a Cauchy criterion. (Contributed by Mario
Carneiro, 18-Mar-2014.)
|
                      
               
           
                  |
|
Theorem | caubnd2 11128* |
A Cauchy sequence of complex numbers is eventually bounded.
(Contributed by Mario Carneiro, 14-Feb-2014.)
|
                                   
               |
|
Theorem | amgm2 11129 |
Arithmetic-geometric mean inequality for
. (Contributed by
Mario Carneiro, 2-Jul-2014.)
|
    
          
   |
|
Theorem | sqrtthi 11130 |
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 11131 |
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 11132 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
       |
|
Theorem | sqrtmsqi 11133 |
Square root of square. (Contributed by NM, 2-Aug-1999.)
|
         |
|
Theorem | sqrtsqi 11134 |
Square root of square. (Contributed by NM, 11-Aug-1999.)
|
           |
|
Theorem | sqsqrti 11135 |
Square of square root. (Contributed by NM, 11-Aug-1999.)
|
           |
|
Theorem | sqrtge0i 11136 |
The square root of a nonnegative real is nonnegative. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
       |
|
Theorem | absidi 11137 |
A nonnegative number is its own absolute value. (Contributed by NM,
2-Aug-1999.)
|
    
  |
|
Theorem | absnidi 11138 |
A negative number is the negative of its own absolute value.
(Contributed by NM, 2-Aug-1999.)
|
    
   |
|
Theorem | leabsi 11139 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 2-Aug-1999.)
|
     |
|
Theorem | absrei 11140 |
Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|
   
         |
|
Theorem | sqrtpclii 11141 |
The square root of a positive real is a real. (Contributed by Mario
Carneiro, 6-Sep-2013.)
|
   
 |
|
Theorem | sqrtgt0ii 11142 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
     |
|
Theorem | sqrt11i 11143 |
The square root function is one-to-one. (Contributed by NM,
27-Jul-1999.)
|
               |
|
Theorem | sqrtmuli 11144 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
                     |
|
Theorem | sqrtmulii 11145 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
                 |
|
Theorem | sqrtmsq2i 11146 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.)
|
             |
|
Theorem | sqrtlei 11147 |
Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|
               |
|
Theorem | sqrtlti 11148 |
Square root is strictly monotonic. (Contributed by Roy F. Longton,
8-Aug-2005.)
|
               |
|
Theorem | abslti 11149 |
Absolute value and 'less than' relation. (Contributed by NM,
6-Apr-2005.)
|
          |
|
Theorem | abslei 11150 |
Absolute value and 'less than or equal to' relation. (Contributed by
NM, 6-Apr-2005.)
|
          |
|
Theorem | absvalsqi 11151 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
               |
|
Theorem | absvalsq2i 11152 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
                           |
|
Theorem | abscli 11153 |
Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|
   
 |
|
Theorem | absge0i 11154 |
Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|
     |
|
Theorem | absval2i 11155 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 2-Oct-1999.)
|
   
                       |
|
Theorem | abs00i 11156 |
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 11157 |
The absolute value of a nonzero number is positive. Remark in [Apostol]
p. 363. (Contributed by NM, 1-Oct-1999.)
|
 #       |
|
Theorem | absnegi 11158 |
Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|
    
     |
|
Theorem | abscji 11159 |
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 11160 |
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 11161 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by NM, 1-Oct-1999.)
|
             |
|
Theorem | absmuli 11162 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
NM, 1-Oct-1999.)
|
                 |
|
Theorem | sqabsaddi 11163 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 2-Oct-1999.)
|
    
                                      |
|
Theorem | sqabssubi 11164 |
Square of absolute value of difference. (Contributed by Steve
Rodriguez, 20-Jan-2007.)
|
                                           |
|
Theorem | absdivapzi 11165 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
 #                   |
|
Theorem | abstrii 11166 |
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 11167 |
Absolute value of differences around common element. (Contributed by
NM, 2-Oct-1999.)
|
                     |
|
Theorem | abs3lemi 11168 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
       
                   |
|
Theorem | rpsqrtcld 11169 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
         |
|
Theorem | sqrtgt0d 11170 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
         |
|
Theorem | absnidd 11171 |
A negative number is the negative of its own absolute value.
(Contributed by Mario Carneiro, 29-May-2016.)
|
            |
|
Theorem | leabsd 11172 |
A real number is less than or equal to its absolute value. (Contributed
by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | absred 11173 |
Absolute value of a real number. (Contributed by Mario Carneiro,
29-May-2016.)
|
                 |
|
Theorem | resqrtcld 11174 |
The square root of a nonnegative real is a real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
           |
|
Theorem | sqrtmsqd 11175 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
             |
|
Theorem | sqrtsqd 11176 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
               |
|
Theorem | sqrtge0d 11177 |
The square root of a nonnegative real is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
           |
|
Theorem | absidd 11178 |
A nonnegative number is its own absolute value. (Contributed by Mario
Carneiro, 29-May-2016.)
|
           |
|
Theorem | sqrtdivd 11179 |
Square root distributes over division. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                         |
|
Theorem | sqrtmuld 11180 |
Square root distributes over multiplication. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                           |
|
Theorem | sqrtsq2d 11181 |
Relationship between square root and squares. (Contributed by Mario
Carneiro, 29-May-2016.)
|
             
       |
|
Theorem | sqrtled 11182 |
Square root is monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
                     |
|
Theorem | sqrtltd 11183 |
Square root is strictly monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
                     |
|
Theorem | sqr11d 11184 |
The square root function is one-to-one. (Contributed by Mario Carneiro,
29-May-2016.)
|
                     |
|
Theorem | absltd 11185 |
Absolute value and 'less than' relation. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                |
|
Theorem | absled 11186 |
Absolute value and 'less than or equal to' relation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
                |
|
Theorem | abssubge0d 11187 |
Absolute value of a nonnegative difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                 |
|
Theorem | abssuble0d 11188 |
Absolute value of a nonpositive difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                 |
|
Theorem | absdifltd 11189 |
The absolute value of a difference and 'less than' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
                
      |
|
Theorem | absdifled 11190 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
                
      |
|
Theorem | icodiamlt 11191 |
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 11192 |
Real closure of absolute value. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | absvalsqd 11193 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                   |
|
Theorem | absvalsq2d 11194 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
                               |
|
Theorem | absge0d 11195 |
Absolute value is nonnegative. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | absval2d 11196 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by Mario Carneiro, 29-May-2016.)
|
                               |
|
Theorem | abs00d 11197 |
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 11198 |
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 11199 |
The absolute value of a complex number apart from zero is a positive
real. (Contributed by Jim Kingdon, 13-Aug-2021.)
|
   #         |
|
Theorem | absnegd 11200 |
Absolute value of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
              |