Type  Label  Description 
Statement 

Theorem  sqeq0i 9501 
A number is zero iff its square is zero. (Contributed by NM,
2Oct1999.)



Theorem  sqmuli 9502 
Distribution of square over multiplication. (Contributed by NM,
3Sep1999.)



Theorem  sqdivapi 9503 
Distribution of square over division. (Contributed by Jim Kingdon,
12Jun2020.)

#


Theorem  resqcli 9504 
Closure of square in reals. (Contributed by NM, 2Aug1999.)



Theorem  sqgt0api 9505 
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12Jun2020.)

# 

Theorem  sqge0i 9506 
A square of a real is nonnegative. (Contributed by NM, 3Aug1999.)



Theorem  lt2sqi 9507 
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12Sep1999.)



Theorem  le2sqi 9508 
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12Sep1999.)



Theorem  sq11i 9509 
The square function is onetoone for nonnegative reals. (Contributed
by NM, 27Oct1999.)



Theorem  sq0 9510 
The square of 0 is 0. (Contributed by NM, 6Jun2006.)



Theorem  sq0i 9511 
If a number is zero, its square is zero. (Contributed by FL,
10Dec2006.)



Theorem  sq0id 9512 
If a number is zero, its square is zero. Deduction form of sq0i 9511.
Converse of sqeq0d 9548. (Contributed by David Moews, 28Feb2017.)



Theorem  sq1 9513 
The square of 1 is 1. (Contributed by NM, 22Aug1999.)



Theorem  neg1sqe1 9514 
squared is 1 (common case).
(Contributed by David A. Wheeler,
8Dec2018.)



Theorem  sq2 9515 
The square of 2 is 4. (Contributed by NM, 22Aug1999.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  expnlbnd2 9542* 
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 9543 
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28May2016.)



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



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



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



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



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



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



Theorem  expp1d 9550 
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 9551 
Sum of exponents law for nonnegative integer exponentiation.
Proposition 104.2(a) of [Gleason] p.
135. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  expmuld 9552 
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 9553 
Square of reciprocal. (Contributed by Jim Kingdon, 12Jun2020.)

# 

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

# 

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

# # 

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

#


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

# 

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

# 

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

# 

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

#


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



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

#


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

#


Theorem  mulexpd 9564 
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 9565 
Value of zero raised to a positive integer power. (Contributed by Mario
Carneiro, 28May2016.)



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



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



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



Theorem  sqoddm1div8 9569 
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 9570 
The naturals are closed under squaring. (Contributed by Mario Carneiro,
28May2016.)



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



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



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



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

# 

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



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



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

# 

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



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



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



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



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



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

# #


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

; ;; 

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

; ; 

Theorem  3dec 9586 
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.)

;; ; ; 

3.6.6 Ordered pair theorem for nonnegative
integers


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



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



Theorem  nn0opthlem2d 9589 
Lemma for nn0opth2 9592. (Contributed by Jim Kingdon, 31Oct2021.)



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



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



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



3.6.7 Factorial function


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



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



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



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



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



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



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



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

