Theorem List for Intuitionistic Logic Explorer - 10101-10200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | expeq0 10101 |
Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed
by NM, 23-Feb-2005.)
|
       
   |
|
Theorem | expap0i 10102 |
Integer exponentiation is apart from zero if its mantissa is apart from
zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
  #
     #   |
|
Theorem | expgt0 10103 |
Nonnegative integer exponentiation with a positive mantissa is positive.
(Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro,
4-Jun-2014.)
|
  
      |
|
Theorem | expnegzap 10104 |
Value of a complex number raised to a negative power. (Contributed by
Mario Carneiro, 4-Jun-2014.)
|
  #
     
        |
|
Theorem | 0exp 10105 |
Value of zero raised to a positive integer power. (Contributed by NM,
19-Aug-2004.)
|
    
  |
|
Theorem | expge0 10106 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario
Carneiro, 4-Jun-2014.)
|
 

      |
|
Theorem | expge1 10107 |
Nonnegative integer exponentiation with a mantissa greater than or equal
to 1 is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.)
(Revised by Mario Carneiro, 4-Jun-2014.)
|
 

      |
|
Theorem | expgt1 10108 |
Positive integer exponentiation with a mantissa greater than 1 is greater
than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro,
4-Jun-2014.)
|
  
      |
|
Theorem | mulexp 10109 |
Positive integer exponentiation of a product. Proposition 10-4.2(c) of
[Gleason] p. 135, restricted to
nonnegative integer exponents.
(Contributed by NM, 13-Feb-2005.)
|
        
            |
|
Theorem | mulexpzap 10110 |
Integer exponentiation of a product. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
   # 
 # 

          
       |
|
Theorem | exprecap 10111 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
  #
      
        |
|
Theorem | expadd 10112 |
Sum of exponents law for nonnegative integer exponentiation.
Proposition 10-4.2(a) of [Gleason] p.
135. (Contributed by NM,
30-Nov-2004.)
|
      
              |
|
Theorem | expaddzaplem 10113 |
Lemma for expaddzap 10114. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
   # 
              
       |
|
Theorem | expaddzap 10114 |
Sum of exponents law for integer exponentiation. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
   # 
                     |
|
Theorem | expmul 10115 |
Product of exponents law for positive integer exponentiation.
Proposition 10-4.2(b) of [Gleason] p.
135, restricted to nonnegative
integer exponents. (Contributed by NM, 4-Jan-2006.)
|
                   |
|
Theorem | expmulzap 10116 |
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11-Jun-2020.)
|
   # 
                   |
|
Theorem | m1expeven 10117 |
Exponentiation of negative one to an even power. (Contributed by Scott
Fenton, 17-Jan-2018.)
|
          |
|
Theorem | expsubap 10118 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
   # 
                     |
|
Theorem | expp1zap 10119 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
  #
    
          |
|
Theorem | expm1ap 10120 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
  #
               |
|
Theorem | expdivap 10121 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
   #        
            |
|
Theorem | ltexp2a 10122 |
Ordering relationship for exponentiation. (Contributed by NM,
2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|
   
             |
|
Theorem | leexp2a 10123 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
                 |
|
Theorem | leexp2r 10124 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
  
    
             |
|
Theorem | leexp1a 10125 |
Weak mantissa ordering relationship for exponentiation. (Contributed by
NM, 18-Dec-2005.)
|
                 |
|
Theorem | exple1 10126 |
Nonnegative integer exponentiation with a mantissa between 0 and 1
inclusive is less than or equal to 1. (Contributed by Paul Chapman,
29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
    
      |
|
Theorem | expubnd 10127 |
An upper bound on   when .
(Contributed by NM,
19-Dec-2005.)
|
 
                   |
|
Theorem | sqval 10128 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
         |
|
Theorem | sqneg 10129 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
            |
|
Theorem | sqsubswap 10130 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
                 |
|
Theorem | sqcl 10131 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
       |
|
Theorem | sqmul 10132 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
                     |
|
Theorem | sqeq0 10133 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
     
   |
|
Theorem | sqdivap 10134 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
  #                    |
|
Theorem | sqne0 10135 |
A number is nonzero iff its square is nonzero. See also sqap0 10136 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
         |
|
Theorem | sqap0 10136 |
A number is apart from zero iff its square is apart from zero.
(Contributed by Jim Kingdon, 13-Aug-2021.)
|
      # #
   |
|
Theorem | resqcl 10137 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
       |
|
Theorem | sqgt0ap 10138 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
  # 
      |
|
Theorem | nnsqcl 10139 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
       |
|
Theorem | zsqcl 10140 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
       |
|
Theorem | qsqcl 10141 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
       |
|
Theorem | sq11 10142 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 10235 which would easily follow from this given
excluded middle, but
which for us is proved another way. (Contributed by NM, 8-Apr-2001.)
(Proof shortened by Mario Carneiro, 28-May-2016.)
|
    
          
   |
|
Theorem | lt2sq 10143 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
    
  
           |
|
Theorem | le2sq 10144 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
    
  
           |
|
Theorem | le2sq2 10145 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
    
            |
|
Theorem | sqge0 10146 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|

      |
|
Theorem | zsqcl2 10147 |
The square of an integer is a nonnegative integer. (Contributed by Mario
Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
       |
|
Theorem | sumsqeq0 10148 |
Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed
by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof
shortened by Mario Carneiro, 28-May-2016.)
|
                   |
|
Theorem | sqvali 10149 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
       |
|
Theorem | sqcli 10150 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
     |
|
Theorem | sqeq0i 10151 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
    
  |
|
Theorem | sqmuli 10152 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
                 |
|
Theorem | sqdivapi 10153 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
#           
      |
|
Theorem | resqcli 10154 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
     |
|
Theorem | sqgt0api 10155 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
 #       |
|
Theorem | sqge0i 10156 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
     |
|
Theorem | lt2sqi 10157 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
       
       |
|
Theorem | le2sqi 10158 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
       
       |
|
Theorem | sq11i 10159 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
               |
|
Theorem | sq0 10160 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
     |
|
Theorem | sq0i 10161 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
       |
|
Theorem | sq0id 10162 |
If a number is zero, its square is zero. Deduction form of sq0i 10161.
Converse of sqeq0d 10200. (Contributed by David Moews, 28-Feb-2017.)
|
         |
|
Theorem | sq1 10163 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
     |
|
Theorem | neg1sqe1 10164 |
 squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
      |
|
Theorem | sq2 10165 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
     |
|
Theorem | sq3 10166 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
     |
|
Theorem | sq4e2t8 10167 |
The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|
       |
|
Theorem | cu2 10168 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
     |
|
Theorem | irec 10169 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
 
  |
|
Theorem | i2 10170 |
squared.
(Contributed by NM, 6-May-1999.)
|
      |
|
Theorem | i3 10171 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
      |
|
Theorem | i4 10172 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
     |
|
Theorem | nnlesq 10173 |
A positive integer is less than or equal to its square. (Contributed by
NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
|

      |
|
Theorem | iexpcyc 10174 |
Taking to the -th power is the same as
using the
-th power instead, by i4 10172. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
             |
|
Theorem | expnass 10175 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
       
         |
|
Theorem | subsq 10176 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
                     |
|
Theorem | subsq2 10177 |
Express the difference of the squares of two numbers as a polynomial in
the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
|
                             |
|
Theorem | binom2i 10178 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
                       |
|
Theorem | subsqi 10179 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
                 |
|
Theorem | binom2 10180 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
                           |
|
Theorem | binom21 10181 |
Special case of binom2 10180 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
                   |
|
Theorem | binom2sub 10182 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
                           |
|
Theorem | binom2sub1 10183 |
Special case of binom2sub 10182 where
. (Contributed by AV,
2-Aug-2021.)
|
                   |
|
Theorem | binom2subi 10184 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
                       |
|
Theorem | mulbinom2 10185 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
                                 |
|
Theorem | binom3 10186 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
                                         |
|
Theorem | zesq 10187 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
        
    |
|
Theorem | nnesq 10188 |
A positive integer is even iff its square is even. (Contributed by NM,
20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
|
        
    |
|
Theorem | bernneq 10189 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
  
             |
|
Theorem | bernneq2 10190 |
Variation of Bernoulli's inequality bernneq 10189. (Contributed by NM,
18-Oct-2007.)
|
 
      
      |
|
Theorem | bernneq3 10191 |
A corollary of bernneq 10189. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
             |
|
Theorem | expnbnd 10192* |
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
          |
|
Theorem | expnlbnd 10193* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.)
|
   
        |
|
Theorem | expnlbnd2 10194* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by
Mario Carneiro, 5-Jun-2014.)
|
   
              |
|
Theorem | exp0d 10195 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | exp1d 10196 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | expeq0d 10197 |
Positive integer exponentiation is 0 iff its mantissa is 0.
(Contributed by Mario Carneiro, 28-May-2016.)
|
        
    |
|
Theorem | sqvald 10198 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
           |
|
Theorem | sqcld 10199 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | sqeq0d 10200 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
           |