Theorem List for Intuitionistic Logic Explorer - 9301-9400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | expmulzap 9301 |
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expsubap 9302 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expp1zap 9303 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expm1ap 9304 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | expdivap 9305 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
#
|
|
Theorem | ltexp2a 9306 |
Ordering relationship for exponentiation. (Contributed by NM,
2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|
|
|
Theorem | leexp2a 9307 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | leexp2r 9308 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | leexp1a 9309 |
Weak mantissa ordering relationship for exponentiation. (Contributed by
NM, 18-Dec-2005.)
|
|
|
Theorem | exple1 9310 |
Nonnegative integer exponentiation with a mantissa between 0 and 1
inclusive is less than or equal to 1. (Contributed by Paul Chapman,
29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | expubnd 9311 |
An upper bound on when .
(Contributed by NM,
19-Dec-2005.)
|
|
|
Theorem | sqval 9312 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
|
|
Theorem | sqneg 9313 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
|
|
Theorem | sqsubswap 9314 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
|
|
Theorem | sqcl 9315 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
|
|
Theorem | sqmul 9316 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
|
|
Theorem | sqeq0 9317 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
|
|
Theorem | sqdivap 9318 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
# |
|
Theorem | sqne0 9319 |
A number is nonzero iff its square is nonzero. See also sqap0 9320 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
|
|
Theorem | sqap0 9320 |
A number is apart from zero iff its square is apart from zero.
(Contributed by Jim Kingdon, 13-Aug-2021.)
|
# #
|
|
Theorem | resqcl 9321 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
|
|
Theorem | sqgt0ap 9322 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
#
|
|
Theorem | nnsqcl 9323 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | zsqcl 9324 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | qsqcl 9325 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
|
|
Theorem | sq11 9326 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 9414 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 9327 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
|
|
Theorem | le2sq 9328 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
|
|
Theorem | le2sq2 9329 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
|
|
Theorem | sqge0 9330 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|
|
|
Theorem | zsqcl2 9331 |
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 9332 |
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 9333 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
|
|
Theorem | sqcli 9334 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqeq0i 9335 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | sqmuli 9336 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
|
|
Theorem | sqdivapi 9337 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
#
|
|
Theorem | resqcli 9338 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqgt0api 9339 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
# |
|
Theorem | sqge0i 9340 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | lt2sqi 9341 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
|
|
Theorem | le2sqi 9342 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
|
|
Theorem | sq11i 9343 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
|
|
Theorem | sq0 9344 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | sq0i 9345 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
|
|
Theorem | sq0id 9346 |
If a number is zero, its square is zero. Deduction form of sq0i 9345.
Converse of sqeq0d 9380. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | sq1 9347 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | neg1sqe1 9348 |
squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | sq2 9349 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | sq3 9350 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
|
|
Theorem | cu2 9351 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
|
|
Theorem | irec 9352 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
|
|
Theorem | i2 9353 |
squared.
(Contributed by NM, 6-May-1999.)
|
|
|
Theorem | i3 9354 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
|
|
Theorem | i4 9355 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
|
|
Theorem | nnlesq 9356 |
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 | expnass 9357 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
|
|
Theorem | subsq 9358 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
|
|
Theorem | subsq2 9359 |
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 9360 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | subsqi 9361 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
|
|
Theorem | binom2 9362 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
|
|
Theorem | binom21 9363 |
Special case of binom2 9362 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
|
|
Theorem | binom2sub 9364 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
|
|
Theorem | binom2subi 9365 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
|
|
Theorem | binom3 9366 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
|
|
Theorem | zesq 9367 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
|
|
Theorem | nnesq 9368 |
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 9369 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | bernneq2 9370 |
Variation of Bernoulli's inequality bernneq 9369. (Contributed by NM,
18-Oct-2007.)
|
|
|
Theorem | bernneq3 9371 |
A corollary of bernneq 9369. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
|
|
Theorem | expnbnd 9372* |
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
|
|
Theorem | expnlbnd 9373* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.)
|
|
|
Theorem | expnlbnd2 9374* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by
Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | exp0d 9375 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | exp1d 9376 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expeq0d 9377 |
Positive integer exponentiation is 0 iff its mantissa is 0.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqvald 9378 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | sqcld 9379 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqeq0d 9380 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | expcld 9381 |
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expp1d 9382 |
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 9383 |
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 9384 |
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 9385 |
Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expclzapd 9386 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
# |
|
Theorem | expap0d 9387 |
Nonnegative integer exponentiation is nonzero if its mantissa is
nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
# # |
|
Theorem | expnegapd 9388 |
Value of a complex number raised to a negative power. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
#
|
|
Theorem | exprecapd 9389 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expp1zapd 9390 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expm1apd 9391 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expsubapd 9392 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
#
|
|
Theorem | sqmuld 9393 |
Distribution of square over multiplication. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | sqdivapd 9394 |
Distribution of square over division. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
#
|
|
Theorem | expdivapd 9395 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
#
|
|
Theorem | mulexpd 9396 |
Positive integer exponentiation of a product. Proposition 10-4.2(c) of
[Gleason] p. 135, restricted to
nonnegative integer exponents.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | 0expd 9397 |
Value of zero raised to a positive integer power. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reexpcld 9398 |
Closure of exponentiation of reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | expge0d 9399 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expge1d 9400 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
|