Theorem List for Intuitionistic Logic Explorer - 10701-10800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sqrtlt 10701 |
Square root is strictly monotonic. Closed form of sqrtlti 10801.
(Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario
Carneiro, 29-May-2016.)
|
    
  
           |
|
Theorem | sqrt11ap 10702 |
Analogue to sqrt11 10703 but for apartness. (Contributed by Jim
Kingdon,
11-Aug-2021.)
|
    
       #     #    |
|
Theorem | sqrt11 10703 |
The square root function is one-to-one. Also see sqrt11ap 10702 which would
follow easily from this given excluded middle, but which is proved another
way without it. (Contributed by Scott Fenton, 11-Jun-2013.)
|
    
      
   
   |
|
Theorem | sqrt00 10704 |
A square root is zero iff its argument is 0. (Contributed by NM,
27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|
       
   |
|
Theorem | rpsqrtcl 10705 |
The square root of a positive real is a positive real. (Contributed by
NM, 22-Feb-2008.)
|
       |
|
Theorem | sqrtdiv 10706 |
Square root distributes over division. (Contributed by Mario Carneiro,
5-May-2016.)
|
                       |
|
Theorem | sqrtsq2 10707 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
    
      
       |
|
Theorem | sqrtsq 10708 |
Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by
Mario Carneiro, 29-May-2016.)
|
             |
|
Theorem | sqrtmsq 10709 |
Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by
Mario Carneiro, 29-May-2016.)
|
           |
|
Theorem | sqrt1 10710 |
The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|
     |
|
Theorem | sqrt4 10711 |
The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|
     |
|
Theorem | sqrt9 10712 |
The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|
     |
|
Theorem | sqrt2gt1lt2 10713 |
The square root of 2 is bounded by 1 and 2. (Contributed by Roy F.
Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
           |
|
Theorem | absneg 10714 |
Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|
     
      |
|
Theorem | abscl 10715 |
Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|
    
  |
|
Theorem | abscj 10716 |
The absolute value of a number and its conjugate are the same.
Proposition 10-3.7(b) of [Gleason] p. 133.
(Contributed by NM,
28-Apr-2005.)
|
               |
|
Theorem | absvalsq 10717 |
Square of value of absolute value function. (Contributed by NM,
16-Jan-2006.)
|
                 |
|
Theorem | absvalsq2 10718 |
Square of value of absolute value function. (Contributed by NM,
1-Feb-2007.)
|
                             |
|
Theorem | sqabsadd 10719 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 21-Jan-2007.)
|
                                               |
|
Theorem | sqabssub 10720 |
Square of absolute value of difference. (Contributed by NM,
21-Jan-2007.)
|
                                               |
|
Theorem | absval2 10721 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 17-Mar-2005.)
|
    
                        |
|
Theorem | abs0 10722 |
The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by
Mario Carneiro, 29-May-2016.)
|
     |
|
Theorem | absi 10723 |
The absolute value of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
   
 |
|
Theorem | absge0 10724 |
Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.)
(Revised by Mario Carneiro, 29-May-2016.)
|

      |
|
Theorem | absrpclap 10725 |
The absolute value of a number apart from zero is a positive real.
(Contributed by Jim Kingdon, 11-Aug-2021.)
|
  #     
  |
|
Theorem | abs00ap 10726 |
The absolute value of a number is apart from zero iff the number is apart
from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|
      #
#
   |
|
Theorem | absext 10727 |
Strong extensionality for absolute value. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
        #     #    |
|
Theorem | abs00 10728 |
The absolute value of a number is zero iff the number is zero. Also see
abs00ap 10726 which is similar but for apartness.
Proposition 10-3.7(c) of
[Gleason] p. 133. (Contributed by NM,
26-Sep-2005.) (Proof shortened by
Mario Carneiro, 29-May-2016.)
|
     
   |
|
Theorem | abs00ad 10729 |
A complex number is zero iff its absolute value is zero. Deduction form
of abs00 10728. (Contributed by David Moews, 28-Feb-2017.)
|
       
   |
|
Theorem | abs00bd 10730 |
If a complex number is zero, its absolute value is zero. (Contributed
by David Moews, 28-Feb-2017.)
|
         |
|
Theorem | absreimsq 10731 |
Square of the absolute value of a number that has been decomposed into
real and imaginary parts. (Contributed by NM, 1-Feb-2007.)
|
                           |
|
Theorem | absreim 10732 |
Absolute value of a number that has been decomposed into real and
imaginary parts. (Contributed by NM, 14-Jan-2006.)
|
      
                    |
|
Theorem | absmul 10733 |
Absolute value distributes over multiplication. Proposition 10-3.7(f) of
[Gleason] p. 133. (Contributed by NM,
11-Oct-1999.) (Revised by Mario
Carneiro, 29-May-2016.)
|
                     |
|
Theorem | absdivap 10734 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
  #                    |
|
Theorem | absid 10735 |
A nonnegative number is its own absolute value. (Contributed by NM,
11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
      
  |
|
Theorem | abs1 10736 |
The absolute value of 1. Common special case. (Contributed by David A.
Wheeler, 16-Jul-2016.)
|
     |
|
Theorem | absnid 10737 |
A negative number is the negative of its own absolute value. (Contributed
by NM, 27-Feb-2005.)
|
  
       |
|
Theorem | leabs 10738 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 27-Feb-2005.)
|

      |
|
Theorem | qabsor 10739 |
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|
     
        |
|
Theorem | qabsord 10740 |
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|
       
        |
|
Theorem | absre 10741 |
Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|
    
          |
|
Theorem | absresq 10742 |
Square of the absolute value of a real number. (Contributed by NM,
16-Jan-2006.)
|
               |
|
Theorem | absexp 10743 |
Absolute value of positive integer exponentiation. (Contributed by NM,
5-Jan-2006.)
|
                     |
|
Theorem | absexpzap 10744 |
Absolute value of integer exponentiation. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
  #
                   |
|
Theorem | abssq 10745 |
Square can be moved in and out of absolute value. (Contributed by Scott
Fenton, 18-Apr-2014.) (Proof shortened by Mario Carneiro,
29-May-2016.)
|
                   |
|
Theorem | sqabs 10746 |
The squares of two reals are equal iff their absolute values are equal.
(Contributed by NM, 6-Mar-2009.)
|
               
       |
|
Theorem | absrele 10747 |
The absolute value of a complex number is greater than or equal to the
absolute value of its real part. (Contributed by NM, 1-Apr-2005.)
|
               |
|
Theorem | absimle 10748 |
The absolute value of a complex number is greater than or equal to the
absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005.)
(Proof shortened by Mario Carneiro, 29-May-2016.)
|
               |
|
Theorem | nn0abscl 10749 |
The absolute value of an integer is a nonnegative integer. (Contributed
by NM, 27-Feb-2005.)
|
    
  |
|
Theorem | zabscl 10750 |
The absolute value of an integer is an integer. (Contributed by Stefan
O'Rear, 24-Sep-2014.)
|
    
  |
|
Theorem | ltabs 10751 |
A number which is less than its absolute value is negative. (Contributed
by Jim Kingdon, 12-Aug-2021.)
|
         |
|
Theorem | abslt 10752 |
Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
(Revised by Mario Carneiro, 29-May-2016.)
|
              |
|
Theorem | absle 10753 |
Absolute value and 'less than or equal to' relation. (Contributed by NM,
6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|
         
    |
|
Theorem | abssubap0 10754 |
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 10755 |
If the absolute value of a complex number is less than a real, its
difference from the real is nonzero. See also abssubap0 10754 which is the
same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.)
|
       
   |
|
Theorem | absdiflt 10756 |
The absolute value of a difference and 'less than' relation. (Contributed
by Paul Chapman, 18-Sep-2007.)
|
             
     |
|
Theorem | absdifle 10757 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Paul Chapman, 18-Sep-2007.)
|
             
     |
|
Theorem | elicc4abs 10758 |
Membership in a symmetric closed real interval. (Contributed by Stefan
O'Rear, 16-Nov-2014.)
|
        ![[,] [,]](_icc.gif)             |
|
Theorem | lenegsq 10759 |
Comparison to a nonnegative number based on comparison to squares.
(Contributed by NM, 16-Jan-2006.)
|
 
        
       |
|
Theorem | releabs 10760 |
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 10761 |
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
  #   
                |
|
Theorem | absidm 10762 |
The absolute value function is idempotent. (Contributed by NM,
20-Nov-2004.)
|
               |
|
Theorem | absgt0ap 10763 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
  #        |
|
Theorem | nnabscl 10764 |
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 10765 |
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 10766 |
Absolute value of a nonnegative difference. (Contributed by NM,
14-Feb-2008.)
|
 
           |
|
Theorem | abssuble0 10767 |
Absolute value of a nonpositive difference. (Contributed by FL,
3-Jan-2008.)
|
 
           |
|
Theorem | abstri 10768 |
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 10769 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
                         |
|
Theorem | abs2dif 10770 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
                     |
|
Theorem | abs2dif2 10771 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
             
       |
|
Theorem | abs2difabs 10772 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
                         |
|
Theorem | recan 10773* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
        
 
     
   |
|
Theorem | absf 10774 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
     |
|
Theorem | abs3lem 10775 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
    
         
                    |
|
Theorem | fzomaxdiflem 10776 |
Lemma for fzomaxdif 10777. (Contributed by Stefan O'Rear,
6-Sep-2015.)
|
    ..^  ..^          ..^     |
|
Theorem | fzomaxdif 10777 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
   ..^
 ..^         ..^     |
|
Theorem | cau3lem 10778* |
Lemma for cau3 10779. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
          
                

                                  
                                   
    
                                                         
 
                           
                                |
|
Theorem | cau3 10779* |
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 10652
and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
|
                                   
          
            
         |
|
Theorem | cau4 10780* |
Change the base of a Cauchy criterion. (Contributed by Mario
Carneiro, 18-Mar-2014.)
|
                      
               
           
                  |
|
Theorem | caubnd2 10781* |
A Cauchy sequence of complex numbers is eventually bounded.
(Contributed by Mario Carneiro, 14-Feb-2014.)
|
                                   
               |
|
Theorem | amgm2 10782 |
Arithmetic-geometric mean inequality for
. (Contributed by
Mario Carneiro, 2-Jul-2014.)
|
    
          
   |
|
Theorem | sqrtthi 10783 |
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 10784 |
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 10785 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
       |
|
Theorem | sqrtmsqi 10786 |
Square root of square. (Contributed by NM, 2-Aug-1999.)
|
         |
|
Theorem | sqrtsqi 10787 |
Square root of square. (Contributed by NM, 11-Aug-1999.)
|
           |
|
Theorem | sqsqrti 10788 |
Square of square root. (Contributed by NM, 11-Aug-1999.)
|
           |
|
Theorem | sqrtge0i 10789 |
The square root of a nonnegative real is nonnegative. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
       |
|
Theorem | absidi 10790 |
A nonnegative number is its own absolute value. (Contributed by NM,
2-Aug-1999.)
|
    
  |
|
Theorem | absnidi 10791 |
A negative number is the negative of its own absolute value.
(Contributed by NM, 2-Aug-1999.)
|
    
   |
|
Theorem | leabsi 10792 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 2-Aug-1999.)
|
     |
|
Theorem | absrei 10793 |
Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|
   
         |
|
Theorem | sqrtpclii 10794 |
The square root of a positive real is a real. (Contributed by Mario
Carneiro, 6-Sep-2013.)
|
   
 |
|
Theorem | sqrtgt0ii 10795 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
     |
|
Theorem | sqrt11i 10796 |
The square root function is one-to-one. (Contributed by NM,
27-Jul-1999.)
|
               |
|
Theorem | sqrtmuli 10797 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
                     |
|
Theorem | sqrtmulii 10798 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
                 |
|
Theorem | sqrtmsq2i 10799 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.)
|
             |
|
Theorem | sqrtlei 10800 |
Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|
               |