Type  Label  Description 
Statement 

Theorem  isermono 9401* 
The partial sums in an infinite series of positive terms form a
monotonic sequence. (Contributed by Jim Kingdon, 15Aug2021.)



Theorem  iseqsplit 9402* 
Split a sequence into two sequences. (Contributed by Jim Kingdon,
16Aug2021.)



Theorem  iseq1p 9403* 
Removing the first term from a sequence. (Contributed by Jim Kingdon,
16Aug2021.)



Theorem  iseqcaopr3 9404* 
Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16Aug2021.)

..^


Theorem  iseqcaopr2 9405* 
The sum of two infinite series (generalized to an arbitrary commutative
and associative operation). (Contributed by Mario Carneiro,
30May2014.)



Theorem  iseqcaopr 9406* 
The sum of two infinite series (generalized to an arbitrary commutative
and associative operation). (Contributed by Jim Kingdon,
17Aug2021.)



Theorem  iseradd 9407* 
The sum of two infinite series. (Contributed by NM, 17Mar2005.)
(Revised by Mario Carneiro, 26May2014.)



Theorem  isersub 9408* 
The difference of two infinite series. (Contributed by NM,
17Mar2005.) (Revised by Mario Carneiro, 27May2014.)



Theorem  iseqid3 9409* 
A sequence that consists entirely of zeroes (or whatever the identity
is for
operation ) sums
to zero. (Contributed by Jim
Kingdon, 18Aug2021.)



Theorem  iseqid3s 9410* 
A sequence that consists of zeroes up to sums to zero at .
In this case by "zero" we mean whatever the identity is for the
operation ). (Contributed by Jim Kingdon, 18Aug2021.)



Theorem  iseqid 9411* 
Discard the first few terms of a sequence that starts with all zeroes
(or whatever the identity is for operation ). (Contributed
by Mario Carneiro, 13Jul2013.) (Revised by Mario Carneiro,
27May2014.)



Theorem  iseqhomo 9412* 
Apply a homomorphism to a sequence. (Contributed by Jim Kingdon,
21Aug2021.)



Theorem  iseqz 9413* 
If the operation
has an absorbing element (a.k.a. zero
element), then any sequence containing a evaluates to .
(Contributed by Mario Carneiro, 27May2014.)



Theorem  iseqdistr 9414* 
The distributive property for series. (Contributed by Jim Kingdon,
21Aug2021.)



Theorem  iser0 9415 
The value of the partial sums in a zerovalued infinite series.
(Contributed by Jim Kingdon, 19Aug2021.)



Theorem  iser0f 9416 
A zerovalued infinite series is equal to the constant zero function.
(Contributed by Jim Kingdon, 19Aug2021.)



Theorem  serige0 9417* 
A finite sum of nonnegative terms is nonnegative. (Contributed by Jim
Kingdon, 22Aug2021.)



Theorem  serile 9418* 
Comparison of partial sums of two infinite series of reals.
(Contributed by Jim Kingdon, 22Aug2021.)



3.6.5 Integer powers


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



Definition  dfiexp 9420* 
Define exponentiation to nonnegative integer powers. This definition is
not meant to be used directly; instead, exp0 9424
and expp1 9427 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 9421 
Lemma for expival 9422. 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 9422 
Value of exponentiation to integer powers. (Contributed by Jim Kingdon,
7Jun2020.)

#


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



Theorem  exp0 9424 
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 9425 
(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 9426 
Value of a complex number raised to the first power. (Contributed by
NM, 20Oct2004.) (Revised by Mario Carneiro, 2Jul2013.)



Theorem  expp1 9427 
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 9428 
Value of a complex number raised to a negative integer power.
(Contributed by Jim Kingdon, 8Jun2020.)

#


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

#


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

# 

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



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

#
# 

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



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



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



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



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



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



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



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

#


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



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



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



Theorem  expclzaplem 9444* 
Closure law for integer exponentiation. Lemma for expclzap 9445 and
expap0i 9452. (Contributed by Jim Kingdon, 9Jun2020.)

#
# 

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

#


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



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



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



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



Theorem  expap0 9450 
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 9451 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 9451 
Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed
by NM, 23Feb2005.)



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

#
# 

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



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

#


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



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



Theorem  expge1 9457 
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 9458 
Positive integer exponentiation with a mantissa greater than 1 is greater
than 1. (Contributed by NM, 13Feb2005.) (Revised by Mario Carneiro,
4Jun2014.)



Theorem  mulexp 9459 
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 9460 
Integer exponentiation of a product. (Contributed by Jim Kingdon,
10Jun2020.)

#
#


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

#


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



Theorem  expaddzaplem 9463 
Lemma for expaddzap 9464. (Contributed by Jim Kingdon, 10Jun2020.)

#


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

#


Theorem  expmul 9465 
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 9466 
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11Jun2020.)

#


Theorem  m1expeven 9467 
Exponentiation of negative one to an even power. (Contributed by Scott
Fenton, 17Jan2018.)



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

#


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

#


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

#


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

#


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



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



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



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



Theorem  exple1 9476 
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 9477 
An upper bound on when .
(Contributed by NM,
19Dec2005.)



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



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



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



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



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



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



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

# 

Theorem  sqne0 9485 
A number is nonzero iff its square is nonzero. See also sqap0 9486 which is
the same but with not equal changed to apart. (Contributed by NM,
11Mar2006.)



Theorem  sqap0 9486 
A number is apart from zero iff its square is apart from zero.
(Contributed by Jim Kingdon, 13Aug2021.)

# #


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



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

#


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



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



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



Theorem  sq11 9492 
The square function is onetoone for nonnegative reals. Also see
sq11ap 9583 which would easily follow from this given
excluded middle, but
which for us is proved another way. (Contributed by NM, 8Apr2001.)
(Proof shortened by Mario Carneiro, 28May2016.)



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



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



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



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



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



Theorem  sumsqeq0 9498 
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 9499 
Value of square. Inference version. (Contributed by NM,
1Aug1999.)



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

