Type  Label  Description 
Statement 

Theorem  sq3 10401 
The square of 3 is 9. (Contributed by NM, 26Apr2006.)



Theorem  sq4e2t8 10402 
The square of 4 is 2 times 8. (Contributed by AV, 20Jul2021.)



Theorem  cu2 10403 
The cube of 2 is 8. (Contributed by NM, 2Aug2004.)



Theorem  irec 10404 
The reciprocal of .
(Contributed by NM, 11Oct1999.)



Theorem  i2 10405 
squared.
(Contributed by NM, 6May1999.)



Theorem  i3 10406 
cubed. (Contributed
by NM, 31Jan2007.)



Theorem  i4 10407 
to the fourth power.
(Contributed by NM, 31Jan2007.)



Theorem  nnlesq 10408 
A positive integer is less than or equal to its square. (Contributed by
NM, 15Sep1999.) (Revised by Mario Carneiro, 12Sep2015.)



Theorem  iexpcyc 10409 
Taking to the th power is the same as
using the
th power instead, by i4 10407. (Contributed by Mario Carneiro,
7Jul2014.)



Theorem  expnass 10410 
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21Sep2010.)



Theorem  subsq 10411 
Factor the difference of two squares. (Contributed by NM,
21Feb2008.)



Theorem  subsq2 10412 
Express the difference of the squares of two numbers as a polynomial in
the difference of the numbers. (Contributed by NM, 21Feb2008.)



Theorem  binom2i 10413 
The square of a binomial. (Contributed by NM, 11Aug1999.)



Theorem  subsqi 10414 
Factor the difference of two squares. (Contributed by NM,
7Feb2005.)



Theorem  binom2 10415 
The square of a binomial. (Contributed by FL, 10Dec2006.)



Theorem  binom21 10416 
Special case of binom2 10415 where
. (Contributed by Scott
Fenton,
11May2014.)



Theorem  binom2sub 10417 
Expand the square of a subtraction. (Contributed by Scott Fenton,
10Jun2013.)



Theorem  binom2sub1 10418 
Special case of binom2sub 10417 where
. (Contributed by AV,
2Aug2021.)



Theorem  binom2subi 10419 
Expand the square of a subtraction. (Contributed by Scott Fenton,
13Jun2013.)



Theorem  mulbinom2 10420 
The square of a binomial with factor. (Contributed by AV,
19Jul2021.)



Theorem  binom3 10421 
The cube of a binomial. (Contributed by Mario Carneiro, 24Apr2015.)



Theorem  zesq 10422 
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12Sep2015.)



Theorem  nnesq 10423 
A positive integer is even iff its square is even. (Contributed by NM,
20Aug2001.) (Revised by Mario Carneiro, 12Sep2015.)



Theorem  bernneq 10424 
Bernoulli's inequality, due to Johan Bernoulli (16671748).
(Contributed by NM, 21Feb2005.)



Theorem  bernneq2 10425 
Variation of Bernoulli's inequality bernneq 10424. (Contributed by NM,
18Oct2007.)



Theorem  bernneq3 10426 
A corollary of bernneq 10424. (Contributed by Mario Carneiro,
11Mar2014.)



Theorem  expnbnd 10427* 
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20Oct2007.)



Theorem  expnlbnd 10428* 
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18Jul2008.)



Theorem  expnlbnd2 10429* 
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18Jul2008.) (Proof shortened by
Mario Carneiro, 5Jun2014.)



Theorem  exp0d 10430 
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  exp1d 10431 
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  expeq0d 10432 
Positive integer exponentiation is 0 iff its mantissa is 0.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  sqvald 10433 
Value of square. Inference version. (Contributed by Mario Carneiro,
28May2016.)



Theorem  sqcld 10434 
Closure of square. (Contributed by Mario Carneiro, 28May2016.)



Theorem  sqeq0d 10435 
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  expcld 10436 
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  expp1d 10437 
Value of a complex number raised to a nonnegative integer power plus
one. Part of Definition 104.1 of [Gleason] p. 134. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  expaddd 10438 
Sum of exponents law for nonnegative integer exponentiation.
Proposition 104.2(a) of [Gleason] p.
135. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  expmuld 10439 
Product of exponents law for positive integer exponentiation.
Proposition 104.2(b) of [Gleason] p.
135, restricted to nonnegative
integer exponents. (Contributed by Mario Carneiro, 28May2016.)



Theorem  sqrecapd 10440 
Square of reciprocal. (Contributed by Jim Kingdon, 12Jun2020.)

# 

Theorem  expclzapd 10441 
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
12Jun2020.)

# 

Theorem  expap0d 10442 
Nonnegative integer exponentiation is nonzero if its mantissa is
nonzero. (Contributed by Jim Kingdon, 12Jun2020.)

# # 

Theorem  expnegapd 10443 
Value of a complex number raised to a negative power. (Contributed by
Jim Kingdon, 12Jun2020.)

#


Theorem  exprecapd 10444 
Nonnegative integer exponentiation of a reciprocal. (Contributed by
Jim Kingdon, 12Jun2020.)

# 

Theorem  expp1zapd 10445 
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 12Jun2020.)

# 

Theorem  expm1apd 10446 
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 12Jun2020.)

# 

Theorem  expsubapd 10447 
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 12Jun2020.)

#


Theorem  sqmuld 10448 
Distribution of square over multiplication. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  sqdivapd 10449 
Distribution of square over division. (Contributed by Jim Kingdon,
13Jun2020.)

#


Theorem  expdivapd 10450 
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 13Jun2020.)

#


Theorem  mulexpd 10451 
Positive integer exponentiation of a product. Proposition 104.2(c) of
[Gleason] p. 135, restricted to
nonnegative integer exponents.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  0expd 10452 
Value of zero raised to a positive integer power. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  reexpcld 10453 
Closure of exponentiation of reals. (Contributed by Mario Carneiro,
28May2016.)



Theorem  expge0d 10454 
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28May2016.)



Theorem  expge1d 10455 
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28May2016.)



Theorem  sqoddm1div8 10456 
A squared odd number minus 1 divided by 8 is the odd number multiplied
with its successor divided by 2. (Contributed by AV, 19Jul2021.)



Theorem  nnsqcld 10457 
The naturals are closed under squaring. (Contributed by Mario Carneiro,
28May2016.)



Theorem  nnexpcld 10458 
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  nn0expcld 10459 
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  rpexpcld 10460 
Closure law for exponentiation of positive reals. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  reexpclzapd 10461 
Closure of exponentiation of reals. (Contributed by Jim Kingdon,
13Jun2020.)

# 

Theorem  resqcld 10462 
Closure of square in reals. (Contributed by Mario Carneiro,
28May2016.)



Theorem  sqge0d 10463 
A square of a real is nonnegative. (Contributed by Mario Carneiro,
28May2016.)



Theorem  sqgt0apd 10464 
The square of a real apart from zero is positive. (Contributed by Jim
Kingdon, 13Jun2020.)

# 

Theorem  leexp2ad 10465 
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  leexp2rd 10466 
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  lt2sqd 10467 
The square function on nonnegative reals is strictly monotonic.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  le2sqd 10468 
The square function on nonnegative reals is monotonic. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  sq11d 10469 
The square function is onetoone for nonnegative reals. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  sq11ap 10470 
Analogue to sq11 10377 but for apartness. (Contributed by Jim
Kingdon,
12Aug2021.)

# #


Theorem  sq10 10471 
The square of 10 is 100. (Contributed by AV, 14Jun2021.) (Revised by
AV, 1Aug2021.)

; ;; 

Theorem  sq10e99m1 10472 
The square of 10 is 99 plus 1. (Contributed by AV, 14Jun2021.)
(Revised by AV, 1Aug2021.)

; ; 

Theorem  3dec 10473 
A "decimal constructor" which is used to build up "decimal
integers" or
"numeric terms" in base 10 with 3 "digits".
(Contributed by AV,
14Jun2021.) (Revised by AV, 1Aug2021.)

;; ; ; 

Theorem  expcanlem 10474 
Lemma for expcan 10475. Proving the order in one direction.
(Contributed
by Jim Kingdon, 29Jan2022.)



Theorem  expcan 10475 
Cancellation law for exponentiation. (Contributed by NM, 2Aug2006.)
(Revised by Mario Carneiro, 4Jun2014.)



Theorem  expcand 10476 
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28May2016.)



4.6.7 Ordered pair theorem for nonnegative
integers


Theorem  nn0le2msqd 10477 
The square function on nonnegative integers is monotonic. (Contributed
by Jim Kingdon, 31Oct2021.)



Theorem  nn0opthlem1d 10478 
A rather pretty lemma for nn0opth2 10482. (Contributed by Jim Kingdon,
31Oct2021.)



Theorem  nn0opthlem2d 10479 
Lemma for nn0opth2 10482. (Contributed by Jim Kingdon, 31Oct2021.)



Theorem  nn0opthd 10480 
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 dfop 3536 that works for any set.
(Contributed by Jim Kingdon, 31Oct2021.)



Theorem  nn0opth2d 10481 
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. See comments for nn0opthd 10480. (Contributed by Jim
Kingdon, 31Oct2021.)



Theorem  nn0opth2 10482 
An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine]
p. 124. See nn0opthd 10480. (Contributed by NM, 22Jul2004.)



4.6.8 Factorial function


Syntax  cfa 10483 
Extend class notation to include the factorial of nonnegative integers.



Definition  dffac 10484 
Define the factorial function on nonnegative integers. For example,
because
(exfac 13045). In the literature, the factorial function
is written as a
postscript exclamation point. (Contributed by NM, 2Dec2004.)



Theorem  facnn 10485 
Value of the factorial function for positive integers. (Contributed by
NM, 2Dec2004.) (Revised by Mario Carneiro, 13Jul2013.)



Theorem  fac0 10486 
The factorial of 0. (Contributed by NM, 2Dec2004.) (Revised by Mario
Carneiro, 13Jul2013.)



Theorem  fac1 10487 
The factorial of 1. (Contributed by NM, 2Dec2004.) (Revised by Mario
Carneiro, 13Jul2013.)



Theorem  facp1 10488 
The factorial of a successor. (Contributed by NM, 2Dec2004.)
(Revised by Mario Carneiro, 13Jul2013.)



Theorem  fac2 10489 
The factorial of 2. (Contributed by NM, 17Mar2005.)



Theorem  fac3 10490 
The factorial of 3. (Contributed by NM, 17Mar2005.)



Theorem  fac4 10491 
The factorial of 4. (Contributed by Mario Carneiro, 18Jun2015.)

; 

Theorem  facnn2 10492 
Value of the factorial function expressed recursively. (Contributed by
NM, 2Dec2004.)



Theorem  faccl 10493 
Closure of the factorial function. (Contributed by NM, 2Dec2004.)



Theorem  faccld 10494 
Closure of the factorial function, deduction version of faccl 10493.
(Contributed by Glauco Siliprandi, 5Apr2020.)



Theorem  facne0 10495 
The factorial function is nonzero. (Contributed by NM, 26Apr2005.)



Theorem  facdiv 10496 
A positive integer divides the factorial of an equal or larger number.
(Contributed by NM, 2May2005.)



Theorem  facndiv 10497 
No positive integer (greater than one) divides the factorial plus one of
an equal or larger number. (Contributed by NM, 3May2005.)



Theorem  facwordi 10498 
Ordering property of factorial. (Contributed by NM, 9Dec2005.)



Theorem  faclbnd 10499 
A lower bound for the factorial function. (Contributed by NM,
17Dec2005.)



Theorem  faclbnd2 10500 
A lower bound for the factorial function. (Contributed by NM,
17Dec2005.)

