Type  Label  Description 
Statement 

Theorem  iseqfn 8901* 
The sequence builder function is a function. (Contributed by Jim
Kingdon, 30May2020.)



Theorem  iseq1 8902* 
Value of the sequence builder function at its initial value.
(Contributed by Jim Kingdon, 31May2020.)



Theorem  iseqcl 8903* 
Closure properties of the recursive sequence builder. (Contributed by
Jim Kingdon, 1Jun2020.)



Theorem  iseqp1 8904* 
Value of the sequence builder function at a successor. (Contributed by
Jim Kingdon, 31May2020.)



Theorem  iseqfveq2 8905* 
Equality of sequences. (Contributed by Jim Kingdon, 3Jun2020.)



Theorem  iseqfeq2 8906* 
Equality of sequences. (Contributed by Jim Kingdon, 3Jun2020.)



Theorem  iseqfveq 8907* 
Equality of sequences. (Contributed by Jim Kingdon, 4Jun2020.)



3.5.9 Integer powers


Syntax  cexp 8908 
Extend class notation to include exponentiation of a complex number to an
integer power.



Definition  dfiexp 8909* 
Define exponentiation to nonnegative integer powers. This definition is
not meant to be used directly; instead, exp0 8913
and expp1 8916 provide the
standard recursive definition. The uparrow notation is used by Donald
Knuth for iterated exponentiation (Science 194, 12351242, 1976)
and
is convenient for us since we don't have superscripts. 10Jun2005: The
definition was extended to include zero exponents, so that
per the convention of Definition 104.1 of [Gleason] p. 134.
4Jun2014: The definition was extended to include negative integer
exponents. The case gives the value ,
so we will avoid this case in our theorems. (Contributed by Jim
Kingdon, 7Jun2020.)



Theorem  expivallem 8910 
Lemma for expival 8911. If we take a complex number apart from zero
and
raise it to a positive integer power, the result is apart from zero.
(Contributed by Jim Kingdon, 7Jun2020.)

#
# 

Theorem  expival 8911 
Value of exponentiation to integer powers. (Contributed by Jim Kingdon,
7Jun2020.)

#


Theorem  expinnval 8912 
Value of exponentiation to positive integer powers. (Contributed by Jim
Kingdon, 8Jun2020.)



Theorem  exp0 8913 
Value of a complex number raised to the 0th power. Note that under our
definition, , following
the convention used by Gleason.
Part of Definition 104.1 of [Gleason] p.
134. (Contributed by NM,
20May2004.) (Revised by Mario Carneiro, 4Jun2014.)



Theorem  0exp0e1 8914 
(common case). This is our
convention. It follows the
convention used by Gleason; see Part of Definition 104.1 of [Gleason]
p. 134. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  exp1 8915 
Value of a complex number raised to the first power. (Contributed by
NM, 20Oct2004.) (Revised by Mario Carneiro, 2Jul2013.)



Theorem  expp1 8916 
Value of a complex number raised to a nonnegative integer power plus
one. Part of Definition 104.1 of [Gleason] p. 134. (Contributed by
NM, 20May2005.) (Revised by Mario Carneiro, 2Jul2013.)



Theorem  expnegap0 8917 
Value of a complex number raised to a negative integer power.
(Contributed by Jim Kingdon, 8Jun2020.)

#


Theorem  expineg2 8918 
Value of a complex number raised to a negative integer power.
(Contributed by Jim Kingdon, 8Jun2020.)

#


Theorem  expn1ap0 8919 
A number to the negative one power is the reciprocal. (Contributed by Jim
Kingdon, 8Jun2020.)

#


Theorem  expcllem 8920* 
Lemma for proving nonnegative integer exponentiation closure laws.
(Contributed by NM, 14Dec2005.)



Theorem  expcl2lemap 8921* 
Lemma for proving integer exponentiation closure laws. (Contributed by
Jim Kingdon, 8Jun2020.)

#
# 

Theorem  nnexpcl 8922 
Closure of exponentiation of nonnegative integers. (Contributed by NM,
16Dec2005.)



Theorem  nn0expcl 8923 
Closure of exponentiation of nonnegative integers. (Contributed by NM,
14Dec2005.)



Theorem  zexpcl 8924 
Closure of exponentiation of integers. (Contributed by NM,
16Dec2005.)



Theorem  qexpcl 8925 
Closure of exponentiation of rationals. (Contributed by NM,
16Dec2005.)



Theorem  reexpcl 8926 
Closure of exponentiation of reals. (Contributed by NM,
14Dec2005.)



Theorem  expcl 8927 
Closure law for nonnegative integer exponentiation. (Contributed by NM,
26May2005.)



Theorem  rpexpcl 8928 
Closure law for exponentiation of positive reals. (Contributed by NM,
24Feb2008.) (Revised by Mario Carneiro, 9Sep2014.)



Theorem  reexpclzap 8929 
Closure of exponentiation of reals. (Contributed by Jim Kingdon,
9Jun2020.)

#


Theorem  qexpclz 8930 
Closure of exponentiation of rational numbers. (Contributed by Mario
Carneiro, 9Sep2014.)



Theorem  m1expcl2 8931 
Closure of exponentiation of negative one. (Contributed by Mario
Carneiro, 18Jun2015.)



Theorem  m1expcl 8932 
Closure of exponentiation of negative one. (Contributed by Mario
Carneiro, 18Jun2015.)



Theorem  expclzaplem 8933* 
Closure law for integer exponentiation. Lemma for expclzap 8934 and
expap0i 8941. (Contributed by Jim Kingdon, 9Jun2020.)

#
# 

Theorem  expclzap 8934 
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
9Jun2020.)

#


Theorem  nn0expcli 8935 
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 17Apr2015.)



Theorem  nn0sqcl 8936 
The square of a nonnegative integer is a nonnegative integer.
(Contributed by Stefan O'Rear, 16Oct2014.)



Theorem  expm1t 8937 
Exponentiation in terms of predecessor exponent. (Contributed by NM,
19Dec2005.)



Theorem  1exp 8938 
Value of one raised to a nonnegative integer power. (Contributed by NM,
15Dec2005.) (Revised by Mario Carneiro, 4Jun2014.)



Theorem  expap0 8939 
Positive integer exponentiation is apart from zero iff its mantissa is
apart from zero. That it is easier to prove this first, and then prove
expeq0 8940 in terms of it, rather than the other way
around, is perhaps an
illustration of the maxim "In constructive analysis, the apartness
is
more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim
Kingdon, 10Jun2020.)

# # 

Theorem  expeq0 8940 
Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed
by NM, 23Feb2005.)



Theorem  expap0i 8941 
Integer exponentiation is apart from zero if its mantissa is apart from
zero. (Contributed by Jim Kingdon, 10Jun2020.)

#
# 

Theorem  expgt0 8942 
Nonnegative integer exponentiation with a positive mantissa is positive.
(Contributed by NM, 16Dec2005.) (Revised by Mario Carneiro,
4Jun2014.)



Theorem  expnegzap 8943 
Value of a complex number raised to a negative power. (Contributed by
Mario Carneiro, 4Jun2014.)

#


Theorem  0exp 8944 
Value of zero raised to a positive integer power. (Contributed by NM,
19Aug2004.)



Theorem  expge0 8945 
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by NM, 16Dec2005.) (Revised by Mario
Carneiro, 4Jun2014.)



Theorem  expge1 8946 
Nonnegative integer exponentiation with a mantissa greater than or equal
to 1 is greater than or equal to 1. (Contributed by NM, 21Feb2005.)
(Revised by Mario Carneiro, 4Jun2014.)



Theorem  expgt1 8947 
Positive integer exponentiation with a mantissa greater than 1 is greater
than 1. (Contributed by NM, 13Feb2005.) (Revised by Mario Carneiro,
4Jun2014.)



Theorem  mulexp 8948 
Positive integer exponentiation of a product. Proposition 104.2(c) of
[Gleason] p. 135, restricted to
nonnegative integer exponents.
(Contributed by NM, 13Feb2005.)



Theorem  mulexpzap 8949 
Integer exponentiation of a product. (Contributed by Jim Kingdon,
10Jun2020.)

#
#


Theorem  exprecap 8950 
Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim
Kingdon, 10Jun2020.)

#


Theorem  expadd 8951 
Sum of exponents law for nonnegative integer exponentiation.
Proposition 104.2(a) of [Gleason] p.
135. (Contributed by NM,
30Nov2004.)



Theorem  expaddzaplem 8952 
Lemma for expaddzap 8953. (Contributed by Jim Kingdon, 10Jun2020.)

#


Theorem  expaddzap 8953 
Sum of exponents law for integer exponentiation. (Contributed by Jim
Kingdon, 10Jun2020.)

#


Theorem  expmul 8954 
Product of exponents law for positive integer exponentiation.
Proposition 104.2(b) of [Gleason] p.
135, restricted to nonnegative
integer exponents. (Contributed by NM, 4Jan2006.)



Theorem  expmulzap 8955 
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11Jun2020.)

#


Theorem  expsubap 8956 
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 11Jun2020.)

#


Theorem  expp1zap 8957 
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 11Jun2020.)

#


Theorem  expm1ap 8958 
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11Jun2020.)

#


Theorem  expdivap 8959 
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11Jun2020.)

# 

Theorem  ltexp2a 8960 
Ordering relationship for exponentiation. (Contributed by NM,
2Aug2006.) (Revised by Mario Carneiro, 4Jun2014.)



Theorem  leexp2a 8961 
Weak ordering relationship for exponentiation. (Contributed by NM,
14Dec2005.) (Revised by Mario Carneiro, 5Jun2014.)



Theorem  leexp2r 8962 
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14Jan2008.) (Revised by Mario Carneiro, 29Apr2014.)



Theorem  leexp1a 8963 
Weak mantissa ordering relationship for exponentiation. (Contributed by
NM, 18Dec2005.)



Theorem  exple1 8964 
Nonnegative integer exponentiation with a mantissa between 0 and 1
inclusive is less than or equal to 1. (Contributed by Paul Chapman,
29Dec2007.) (Revised by Mario Carneiro, 5Jun2014.)



Theorem  expubnd 8965 
An upper bound on when . (Contributed by NM,
19Dec2005.)



Theorem  sqval 8966 
Value of the square of a complex number. (Contributed by Raph Levien,
10Apr2004.)



Theorem  sqneg 8967 
The square of the negative of a number.) (Contributed by NM,
15Jan2006.)



Theorem  sqsubswap 8968 
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10Jun2013.)



Theorem  sqcl 8969 
Closure of square. (Contributed by NM, 10Aug1999.)



Theorem  sqmul 8970 
Distribution of square over multiplication. (Contributed by NM,
21Mar2008.)



Theorem  sqeq0 8971 
A number is zero iff its square is zero. (Contributed by NM,
11Mar2006.)



Theorem  sqdivap 8972 
Distribution of square over division. (Contributed by Jim Kingdon,
11Jun2020.)

#


Theorem  sqne0 8973 
A number is nonzero iff its square is nonzero. (Contributed by NM,
11Mar2006.)



Theorem  resqcl 8974 
Closure of the square of a real number. (Contributed by NM,
18Oct1999.)



Theorem  sqgt0ap 8975 
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11Jun2020.)

# 

Theorem  nnsqcl 8976 
The naturals are closed under squaring. (Contributed by Scott Fenton,
29Mar2014.) (Revised by Mario Carneiro, 19Apr2014.)



Theorem  zsqcl 8977 
Integers are closed under squaring. (Contributed by Scott Fenton,
18Apr2014.) (Revised by Mario Carneiro, 19Apr2014.)



Theorem  qsqcl 8978 
The square of a rational is rational. (Contributed by Stefan O'Rear,
15Sep2014.)



Theorem  sq11 8979 
The square function is onetoone for nonnegative reals. (Contributed by
NM, 8Apr2001.) (Proof shortened by Mario Carneiro, 28May2016.)



Theorem  lt2sq 8980 
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24Feb2006.)



Theorem  le2sq 8981 
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18Oct1999.)



Theorem  le2sq2 8982 
The square of a 'less than or equal to' ordering. (Contributed by NM,
21Mar2008.)



Theorem  sqge0 8983 
A square of a real is nonnegative. (Contributed by NM, 18Oct1999.)



Theorem  zsqcl2 8984 
The square of an integer is a nonnegative integer. (Contributed by Mario
Carneiro, 18Apr2014.) (Revised by Mario Carneiro, 14Jul2014.)



Theorem  sumsqeq0 8985 
Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed
by NM, 29Apr2005.) (Revised by Stefan O'Rear, 5Oct2014.) (Proof
shortened by Mario Carneiro, 28May2016.)



Theorem  sqvali 8986 
Value of square. Inference version. (Contributed by NM,
1Aug1999.)



Theorem  sqcli 8987 
Closure of square. (Contributed by NM, 2Aug1999.)



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



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



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

# 

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



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

# 

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



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



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



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



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



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



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



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

