Theorem List for Intuitionistic Logic Explorer - 10501-10600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | expgt1 10501 |
A real greater than 1 raised to a positive integer is greater than 1.
(Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro,
4-Jun-2014.)
|
|
|
Theorem | mulexp 10502 |
Nonnegative integer exponentiation of a product. Proposition 10-4.2(c)
of [Gleason] p. 135, restricted to
nonnegative integer exponents.
(Contributed by NM, 13-Feb-2005.)
|
|
|
Theorem | mulexpzap 10503 |
Integer exponentiation of a product. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
#
#
|
|
Theorem | exprecap 10504 |
Integer exponentiation of a reciprocal. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
#
|
|
Theorem | expadd 10505 |
Sum of exponents law for nonnegative integer exponentiation.
Proposition 10-4.2(a) of [Gleason] p.
135. (Contributed by NM,
30-Nov-2004.)
|
|
|
Theorem | expaddzaplem 10506 |
Lemma for expaddzap 10507. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
#
|
|
Theorem | expaddzap 10507 |
Sum of exponents law for integer exponentiation. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
#
|
|
Theorem | expmul 10508 |
Product of exponents law for nonnegative integer exponentiation.
Proposition 10-4.2(b) of [Gleason] p.
135, restricted to nonnegative
integer exponents. (Contributed by NM, 4-Jan-2006.)
|
|
|
Theorem | expmulzap 10509 |
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | m1expeven 10510 |
Exponentiation of negative one to an even power. (Contributed by Scott
Fenton, 17-Jan-2018.)
|
|
|
Theorem | expsubap 10511 |
Exponent subtraction law for integer exponentiation. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expp1zap 10512 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expm1ap 10513 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expdivap 10514 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | ltexp2a 10515 |
Ordering relationship for exponentiation. (Contributed by NM,
2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|
|
|
Theorem | leexp2a 10516 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | leexp2r 10517 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | leexp1a 10518 |
Weak base ordering relationship for exponentiation. (Contributed by NM,
18-Dec-2005.)
|
|
|
Theorem | exple1 10519 |
A real between 0 and 1 inclusive raised to a nonnegative integer is less
than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised
by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | expubnd 10520 |
An upper bound on when .
(Contributed by NM,
19-Dec-2005.)
|
|
|
Theorem | sqval 10521 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
|
|
Theorem | sqneg 10522 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
|
|
Theorem | sqsubswap 10523 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
|
|
Theorem | sqcl 10524 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
|
|
Theorem | sqmul 10525 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
|
|
Theorem | sqeq0 10526 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
|
|
Theorem | sqdivap 10527 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
# |
|
Theorem | sqne0 10528 |
A number is nonzero iff its square is nonzero. See also sqap0 10529 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
|
|
Theorem | sqap0 10529 |
A number is apart from zero iff its square is apart from zero.
(Contributed by Jim Kingdon, 13-Aug-2021.)
|
# #
|
|
Theorem | resqcl 10530 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
|
|
Theorem | sqgt0ap 10531 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
#
|
|
Theorem | nnsqcl 10532 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | zsqcl 10533 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | qsqcl 10534 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
|
|
Theorem | sq11 10535 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 10630 which would easily follow from this given
excluded middle, but
which for us is proved another way. (Contributed by NM, 8-Apr-2001.)
(Proof shortened by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lt2sq 10536 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
|
|
Theorem | le2sq 10537 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
|
|
Theorem | le2sq2 10538 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
|
|
Theorem | sqge0 10539 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|
|
|
Theorem | zsqcl2 10540 |
The square of an integer is a nonnegative integer. (Contributed by Mario
Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | sumsqeq0 10541 |
Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed
by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof
shortened by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqvali 10542 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
|
|
Theorem | sqcli 10543 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqeq0i 10544 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | sqmuli 10545 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
|
|
Theorem | sqdivapi 10546 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
#
|
|
Theorem | resqcli 10547 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqgt0api 10548 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
# |
|
Theorem | sqge0i 10549 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | lt2sqi 10550 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
|
|
Theorem | le2sqi 10551 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
|
|
Theorem | sq11i 10552 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
|
|
Theorem | sq0 10553 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | sq0i 10554 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
|
|
Theorem | sq0id 10555 |
If a number is zero, its square is zero. Deduction form of sq0i 10554.
Converse of sqeq0d 10595. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | sq1 10556 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | neg1sqe1 10557 |
squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | sq2 10558 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | sq3 10559 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
|
|
Theorem | sq4e2t8 10560 |
The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|
|
|
Theorem | cu2 10561 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
|
|
Theorem | irec 10562 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
|
|
Theorem | i2 10563 |
squared.
(Contributed by NM, 6-May-1999.)
|
|
|
Theorem | i3 10564 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
|
|
Theorem | i4 10565 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
|
|
Theorem | nnlesq 10566 |
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 10567 |
Taking to the -th power is the same as
using the
-th power instead, by i4 10565. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
|
|
Theorem | expnass 10568 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
|
|
Theorem | subsq 10569 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
|
|
Theorem | subsq2 10570 |
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 10571 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | subsqi 10572 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
|
|
Theorem | qsqeqor 10573 |
The squares of two rational numbers are equal iff one number equals the
other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
|
|
|
Theorem | binom2 10574 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
|
|
Theorem | binom21 10575 |
Special case of binom2 10574 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
|
|
Theorem | binom2sub 10576 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
|
|
Theorem | binom2sub1 10577 |
Special case of binom2sub 10576 where
. (Contributed by AV,
2-Aug-2021.)
|
|
|
Theorem | binom2subi 10578 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
|
|
Theorem | mulbinom2 10579 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
|
|
Theorem | binom3 10580 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
|
|
Theorem | zesq 10581 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
|
|
Theorem | nnesq 10582 |
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 10583 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | bernneq2 10584 |
Variation of Bernoulli's inequality bernneq 10583. (Contributed by NM,
18-Oct-2007.)
|
|
|
Theorem | bernneq3 10585 |
A corollary of bernneq 10583. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
|
|
Theorem | expnbnd 10586* |
Exponentiation with a base greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
|
|
Theorem | expnlbnd 10587* |
The reciprocal of exponentiation with a base greater than 1 has no
positive lower bound. (Contributed by NM, 18-Jul-2008.)
|
|
|
Theorem | expnlbnd2 10588* |
The reciprocal of exponentiation with a base greater than 1 has no
positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof
shortened by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | modqexp 10589 |
Exponentiation property of the modulo operation, see theorem 5.2(c) in
[ApostolNT] p. 107. (Contributed by
Mario Carneiro, 28-Feb-2014.)
(Revised by Jim Kingdon, 7-Sep-2024.)
|
|
|
Theorem | exp0d 10590 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | exp1d 10591 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expeq0d 10592 |
Positive integer exponentiation is 0 iff its base is 0. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqvald 10593 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | sqcld 10594 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqeq0d 10595 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | expcld 10596 |
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expp1d 10597 |
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 10598 |
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 10599 |
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 10600 |
Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |