Theorem List for Intuitionistic Logic Explorer - 9701-9800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sq0id 9701 |
If a number is zero, its square is zero. Deduction form of sq0i 9700.
Converse of sqeq0d 9737. (Contributed by David Moews, 28-Feb-2017.)
|
         |
|
Theorem | sq1 9702 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
     |
|
Theorem | neg1sqe1 9703 |
 squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
      |
|
Theorem | sq2 9704 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
     |
|
Theorem | sq3 9705 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
     |
|
Theorem | cu2 9706 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
     |
|
Theorem | irec 9707 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
 
  |
|
Theorem | i2 9708 |
squared.
(Contributed by NM, 6-May-1999.)
|
      |
|
Theorem | i3 9709 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
      |
|
Theorem | i4 9710 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
     |
|
Theorem | nnlesq 9711 |
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 9712 |
Taking to the -th power is the same as
using the
-th power instead, by i4 9710. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
             |
|
Theorem | expnass 9713 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
       
         |
|
Theorem | subsq 9714 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
                     |
|
Theorem | subsq2 9715 |
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 9716 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
                       |
|
Theorem | subsqi 9717 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
                 |
|
Theorem | binom2 9718 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
                           |
|
Theorem | binom21 9719 |
Special case of binom2 9718 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
                   |
|
Theorem | binom2sub 9720 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
                           |
|
Theorem | binom2subi 9721 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
                       |
|
Theorem | mulbinom2 9722 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
                                 |
|
Theorem | binom3 9723 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
                                         |
|
Theorem | zesq 9724 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
        
    |
|
Theorem | nnesq 9725 |
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 9726 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
  
             |
|
Theorem | bernneq2 9727 |
Variation of Bernoulli's inequality bernneq 9726. (Contributed by NM,
18-Oct-2007.)
|
 
      
      |
|
Theorem | bernneq3 9728 |
A corollary of bernneq 9726. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
             |
|
Theorem | expnbnd 9729* |
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
          |
|
Theorem | expnlbnd 9730* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.)
|
   
        |
|
Theorem | expnlbnd2 9731* |
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 9732 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | exp1d 9733 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | expeq0d 9734 |
Positive integer exponentiation is 0 iff its mantissa is 0.
(Contributed by Mario Carneiro, 28-May-2016.)
|
        
    |
|
Theorem | sqvald 9735 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
           |
|
Theorem | sqcld 9736 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | sqeq0d 9737 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
           |
|
Theorem | expcld 9738 |
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28-May-2016.)
|
           |
|
Theorem | expp1d 9739 |
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 9740 |
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 9741 |
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 9742 |
Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                 |
|
Theorem | expclzapd 9743 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
   #           |
|
Theorem | expap0d 9744 |
Nonnegative integer exponentiation is nonzero if its mantissa is
nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #         #   |
|
Theorem | expnegapd 9745 |
Value of a complex number raised to a negative power. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
   #         
        |
|
Theorem | exprecapd 9746 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
   #                   |
|
Theorem | expp1zapd 9747 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                   |
|
Theorem | expm1apd 9748 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                   |
|
Theorem | expsubapd 9749 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
   #                 
       |
|
Theorem | sqmuld 9750 |
Distribution of square over multiplication. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                       |
|
Theorem | sqdivapd 9751 |
Distribution of square over division. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
     #
            
       |
|
Theorem | expdivapd 9752 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
     #
              
       |
|
Theorem | mulexpd 9753 |
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.)
|
                 
       |
|
Theorem | 0expd 9754 |
Value of zero raised to a positive integer power. (Contributed by Mario
Carneiro, 28-May-2016.)
|
         |
|
Theorem | reexpcld 9755 |
Closure of exponentiation of reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
           |
|
Theorem | expge0d 9756 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
             |
|
Theorem | expge1d 9757 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
             |
|
Theorem | sqoddm1div8 9758 |
A squared odd number minus 1 divided by 8 is the odd number multiplied
with its successor divided by 2. (Contributed by AV, 19-Jul-2021.)
|
    
 
          
     |
|
Theorem | nnsqcld 9759 |
The naturals are closed under squaring. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | nnexpcld 9760 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
           |
|
Theorem | nn0expcld 9761 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
           |
|
Theorem | rpexpcld 9762 |
Closure law for exponentiation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
           |
|
Theorem | reexpclzapd 9763 |
Closure of exponentiation of reals. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
   #           |
|
Theorem | resqcld 9764 |
Closure of square in reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | sqge0d 9765 |
A square of a real is nonnegative. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | sqgt0apd 9766 |
The square of a real apart from zero is positive. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
   #         |
|
Theorem | leexp2ad 9767 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                     |
|
Theorem | leexp2rd 9768 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                         |
|
Theorem | lt2sqd 9769 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by Mario Carneiro, 28-May-2016.)
|
                     |
|
Theorem | le2sqd 9770 |
The square function on nonnegative reals is monotonic. (Contributed by
Mario Carneiro, 28-May-2016.)
|
                     |
|
Theorem | sq11d 9771 |
The square function is one-to-one for nonnegative reals. (Contributed
by Mario Carneiro, 28-May-2016.)
|
                     |
|
Theorem | sq11ap 9772 |
Analogue to sq11 9681 but for apartness. (Contributed by Jim
Kingdon,
12-Aug-2021.)
|
    
       #     #
   |
|
Theorem | sq10 9773 |
The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by
AV, 1-Aug-2021.)
|
;    ;;   |
|
Theorem | sq10e99m1 9774 |
The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.)
(Revised by AV, 1-Aug-2021.)
|
;    ;   |
|
Theorem | 3dec 9775 |
A "decimal constructor" which is used to build up "decimal
integers" or
"numeric terms" in base 10 with 3 "digits".
(Contributed by AV,
14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|
;;     ;     ;     |
|
Theorem | expcanlem 9776 |
Lemma for expcan 9777. Proving the order in one direction.
(Contributed
by Jim Kingdon, 29-Jan-2022.)
|
                 
   |
|
Theorem | expcan 9777 |
Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.)
(Revised by Mario Carneiro, 4-Jun-2014.)
|
   
     
   
   |
|
Theorem | expcand 9778 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
                     |
|
3.6.7 Ordered pair theorem for nonnegative
integers
|
|
Theorem | nn0le2msqd 9779 |
The square function on nonnegative integers is monotonic. (Contributed
by Jim Kingdon, 31-Oct-2021.)
|
       
     |
|
Theorem | nn0opthlem1d 9780 |
A rather pretty lemma for nn0opth2 9784. (Contributed by Jim Kingdon,
31-Oct-2021.)
|
           
     |
|
Theorem | nn0opthlem2d 9781 |
Lemma for nn0opth2 9784. (Contributed by Jim Kingdon, 31-Oct-2021.)
|
              
       
    |
|
Theorem | nn0opthd 9782 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. We can represent an
ordered pair of nonnegative
integers and
by     
   . If
two such ordered pairs are equal, their first elements are equal and
their second elements are equal. Contrast this ordered pair
representation with the standard one df-op 3426 that works for any set.
(Contributed by Jim Kingdon, 31-Oct-2021.)
|
                

       
     |
|
Theorem | nn0opth2d 9783 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. See comments for nn0opthd 9782. (Contributed by Jim
Kingdon, 31-Oct-2021.)
|
                 
       
     |
|
Theorem | nn0opth2 9784 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine]
p. 124. See nn0opthd 9782. (Contributed by NM, 22-Jul-2004.)
|
  
 
          
       
     |
|
3.6.8 Factorial function
|
|
Syntax | cfa 9785 |
Extend class notation to include the factorial of nonnegative integers.
|
 |
|
Definition | df-fac 9786 |
Define the factorial function on nonnegative integers. For example,
      because
 
(ex-fac 10809). In the literature, the factorial function
is written as a
postscript exclamation point. (Contributed by NM, 2-Dec-2004.)
|
           |
|
Theorem | facnn 9787 |
Value of the factorial function for positive integers. (Contributed by
NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|
    
 
      |
|
Theorem | fac0 9788 |
The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario
Carneiro, 13-Jul-2013.)
|
     |
|
Theorem | fac1 9789 |
The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario
Carneiro, 13-Jul-2013.)
|
     |
|
Theorem | facp1 9790 |
The factorial of a successor. (Contributed by NM, 2-Dec-2004.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
                 |
|
Theorem | fac2 9791 |
The factorial of 2. (Contributed by NM, 17-Mar-2005.)
|
     |
|
Theorem | fac3 9792 |
The factorial of 3. (Contributed by NM, 17-Mar-2005.)
|
     |
|
Theorem | fac4 9793 |
The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
|
    ;  |
|
Theorem | facnn2 9794 |
Value of the factorial function expressed recursively. (Contributed by
NM, 2-Dec-2004.)
|
    
          |
|
Theorem | faccl 9795 |
Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
|
       |
|
Theorem | faccld 9796 |
Closure of the factorial function, deduction version of faccl 9795.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
         |
|
Theorem | facne0 9797 |
The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|
       |
|
Theorem | facdiv 9798 |
A positive integer divides the factorial of an equal or larger number.
(Contributed by NM, 2-May-2005.)
|
       
   |
|
Theorem | facndiv 9799 |
No positive integer (greater than one) divides the factorial plus one of
an equal or larger number. (Contributed by NM, 3-May-2005.)
|
  

         
   |
|
Theorem | facwordi 9800 |
Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|
             |