Theorem List for Intuitionistic Logic Explorer - 10601-10700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | expm1ap 10601 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
  #
               |
|
Theorem | expdivap 10602 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
   #        
            |
|
Theorem | ltexp2a 10603 |
Ordering relationship for exponentiation. (Contributed by NM,
2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|
   
             |
|
Theorem | leexp2a 10604 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
                 |
|
Theorem | leexp2r 10605 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
  
    
             |
|
Theorem | leexp1a 10606 |
Weak base ordering relationship for exponentiation. (Contributed by NM,
18-Dec-2005.)
|
                 |
|
Theorem | exple1 10607 |
A real between 0 and 1 inclusive raised to a nonnegative integer is less
than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised
by Mario Carneiro, 5-Jun-2014.)
|
    
      |
|
Theorem | expubnd 10608 |
An upper bound on   when .
(Contributed by NM,
19-Dec-2005.)
|
 
                   |
|
Theorem | sqval 10609 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
         |
|
Theorem | sqneg 10610 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
            |
|
Theorem | sqsubswap 10611 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
                 |
|
Theorem | sqcl 10612 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
       |
|
Theorem | sqmul 10613 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
                     |
|
Theorem | sqeq0 10614 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
     
   |
|
Theorem | sqdivap 10615 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
  #                    |
|
Theorem | sqdividap 10616 |
The square of a complex number apart from zero divided by itself equals
that number. (Contributed by AV, 19-Jul-2021.)
|
  #       
  |
|
Theorem | sqne0 10617 |
A number is nonzero iff its square is nonzero. See also sqap0 10618 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
         |
|
Theorem | sqap0 10618 |
A number is apart from zero iff its square is apart from zero.
(Contributed by Jim Kingdon, 13-Aug-2021.)
|
      # #
   |
|
Theorem | resqcl 10619 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
       |
|
Theorem | sqgt0ap 10620 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
  # 
      |
|
Theorem | nnsqcl 10621 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
       |
|
Theorem | zsqcl 10622 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
       |
|
Theorem | qsqcl 10623 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
       |
|
Theorem | sq11 10624 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 10719 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 10625 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
    
  
           |
|
Theorem | le2sq 10626 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
    
  
           |
|
Theorem | le2sq2 10627 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
    
            |
|
Theorem | sqge0 10628 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|

      |
|
Theorem | zsqcl2 10629 |
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 10630 |
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 10631 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
       |
|
Theorem | sqcli 10632 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
     |
|
Theorem | sqeq0i 10633 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
    
  |
|
Theorem | sqmuli 10634 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
                 |
|
Theorem | sqdivapi 10635 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
#           
      |
|
Theorem | resqcli 10636 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
     |
|
Theorem | sqgt0api 10637 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
 #       |
|
Theorem | sqge0i 10638 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
     |
|
Theorem | lt2sqi 10639 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
       
       |
|
Theorem | le2sqi 10640 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
       
       |
|
Theorem | sq11i 10641 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
               |
|
Theorem | sq0 10642 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
     |
|
Theorem | sq0i 10643 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
       |
|
Theorem | sq0id 10644 |
If a number is zero, its square is zero. Deduction form of sq0i 10643.
Converse of sqeq0d 10684. (Contributed by David Moews, 28-Feb-2017.)
|
         |
|
Theorem | sq1 10645 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
     |
|
Theorem | neg1sqe1 10646 |
 squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
      |
|
Theorem | sq2 10647 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
     |
|
Theorem | sq3 10648 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
     |
|
Theorem | sq4e2t8 10649 |
The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|
       |
|
Theorem | cu2 10650 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
     |
|
Theorem | irec 10651 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
 
  |
|
Theorem | i2 10652 |
squared.
(Contributed by NM, 6-May-1999.)
|
      |
|
Theorem | i3 10653 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
      |
|
Theorem | i4 10654 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
     |
|
Theorem | nnlesq 10655 |
A positive integer is less than or equal to its square. For general
integers, see zzlesq 10720. (Contributed by NM, 15-Sep-1999.)
(Revised by
Mario Carneiro, 12-Sep-2015.)
|

      |
|
Theorem | iexpcyc 10656 |
Taking to the -th power is the same as
using the
-th power instead, by i4 10654. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
             |
|
Theorem | expnass 10657 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
       
         |
|
Theorem | subsq 10658 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
                     |
|
Theorem | subsq2 10659 |
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 10660 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
                       |
|
Theorem | subsqi 10661 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
                 |
|
Theorem | qsqeqor 10662 |
The squares of two rational numbers are equal iff one number equals the
other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
|
                  |
|
Theorem | binom2 10663 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
                           |
|
Theorem | binom21 10664 |
Special case of binom2 10663 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
                   |
|
Theorem | binom2sub 10665 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
                           |
|
Theorem | binom2sub1 10666 |
Special case of binom2sub 10665 where
. (Contributed by AV,
2-Aug-2021.)
|
                   |
|
Theorem | binom2subi 10667 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
                       |
|
Theorem | mulbinom2 10668 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
                                 |
|
Theorem | binom3 10669 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
                                         |
|
Theorem | zesq 10670 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
        
    |
|
Theorem | nnesq 10671 |
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 10672 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
  
             |
|
Theorem | bernneq2 10673 |
Variation of Bernoulli's inequality bernneq 10672. (Contributed by NM,
18-Oct-2007.)
|
 
      
      |
|
Theorem | bernneq3 10674 |
A corollary of bernneq 10672. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
             |
|
Theorem | expnbnd 10675* |
Exponentiation with a base greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
          |
|
Theorem | expnlbnd 10676* |
The reciprocal of exponentiation with a base greater than 1 has no
positive lower bound. (Contributed by NM, 18-Jul-2008.)
|
   
        |
|
Theorem | expnlbnd2 10677* |
The reciprocal of exponentiation with a base greater than 1 has no
positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof
shortened by Mario Carneiro, 5-Jun-2014.)
|
   
              |
|
Theorem | modqexp 10678 |
Exponentiation property of the modulo operation, see theorem 5.2(c) in
[ApostolNT] p. 107. (Contributed by
Mario Carneiro, 28-Feb-2014.)
(Revised by Jim Kingdon, 7-Sep-2024.)
|
                           
   |
|
Theorem | exp0d 10679 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | exp1d 10680 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | expeq0d 10681 |
Positive integer exponentiation is 0 iff its base is 0. (Contributed
by Mario Carneiro, 28-May-2016.)
|
        
    |
|
Theorem | sqvald 10682 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
           |
|
Theorem | sqcld 10683 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | sqeq0d 10684 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
           |
|
Theorem | expcld 10685 |
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28-May-2016.)
|
           |
|
Theorem | expp1d 10686 |
Value of a complex number raised to a nonnegative integer power plus
one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by
Mario Carneiro, 28-May-2016.)
|
               
   |
|
Theorem | expaddd 10687 |
Sum of exponents law for nonnegative integer exponentiation.
Proposition 10-4.2(a) of [Gleason] p.
135. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                 
       |
|
Theorem | expmuld 10688 |
Product of exponents law for positive integer exponentiation.
Proposition 10-4.2(b) of [Gleason] p.
135, restricted to nonnegative
integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
|
                       |
|
Theorem | sqrecapd 10689 |
Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                 |
|
Theorem | expclzapd 10690 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
   #           |
|
Theorem | expap0d 10691 |
Nonnegative integer exponentiation is nonzero if its base is nonzero.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #         #   |
|
Theorem | expnegapd 10692 |
Value of a complex number raised to a negative power. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
   #         
        |
|
Theorem | exprecapd 10693 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
   #                   |
|
Theorem | expp1zapd 10694 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                   |
|
Theorem | expm1apd 10695 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                   |
|
Theorem | expsubapd 10696 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                 
       |
|
Theorem | sqmuld 10697 |
Distribution of square over multiplication. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                       |
|
Theorem | sqdivapd 10698 |
Distribution of square over division. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
     #
            
       |
|
Theorem | expdivapd 10699 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
     #
              
       |
|
Theorem | mulexpd 10700 |
Positive integer exponentiation of a product. Proposition 10-4.2(c) of
[Gleason] p. 135, restricted to
nonnegative integer exponents.
(Contributed by Mario Carneiro, 28-May-2016.)
|
                 
       |