Theorem List for Intuitionistic Logic Explorer - 10301-10400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | leexp2a 10301 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
|
|
Theorem | leexp2r 10302 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
|
|
Theorem | leexp1a 10303 |
Weak mantissa ordering relationship for exponentiation. (Contributed by
NM, 18-Dec-2005.)
|
|
|
Theorem | exple1 10304 |
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 10305 |
An upper bound on when .
(Contributed by NM,
19-Dec-2005.)
|
|
|
Theorem | sqval 10306 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
|
|
Theorem | sqneg 10307 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
|
|
Theorem | sqsubswap 10308 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
|
|
Theorem | sqcl 10309 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
|
|
Theorem | sqmul 10310 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
|
|
Theorem | sqeq0 10311 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
|
|
Theorem | sqdivap 10312 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
# |
|
Theorem | sqne0 10313 |
A number is nonzero iff its square is nonzero. See also sqap0 10314 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
|
|
Theorem | sqap0 10314 |
A number is apart from zero iff its square is apart from zero.
(Contributed by Jim Kingdon, 13-Aug-2021.)
|
# #
|
|
Theorem | resqcl 10315 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
|
|
Theorem | sqgt0ap 10316 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
#
|
|
Theorem | nnsqcl 10317 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | zsqcl 10318 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | qsqcl 10319 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
|
|
Theorem | sq11 10320 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 10413 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 10321 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
|
|
Theorem | le2sq 10322 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
|
|
Theorem | le2sq2 10323 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
|
|
Theorem | sqge0 10324 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|
|
|
Theorem | zsqcl2 10325 |
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 10326 |
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 10327 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
|
|
Theorem | sqcli 10328 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqeq0i 10329 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | sqmuli 10330 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
|
|
Theorem | sqdivapi 10331 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
#
|
|
Theorem | resqcli 10332 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqgt0api 10333 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
# |
|
Theorem | sqge0i 10334 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | lt2sqi 10335 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
|
|
Theorem | le2sqi 10336 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
|
|
Theorem | sq11i 10337 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
|
|
Theorem | sq0 10338 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | sq0i 10339 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
|
|
Theorem | sq0id 10340 |
If a number is zero, its square is zero. Deduction form of sq0i 10339.
Converse of sqeq0d 10378. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | sq1 10341 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | neg1sqe1 10342 |
squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | sq2 10343 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | sq3 10344 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
|
|
Theorem | sq4e2t8 10345 |
The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|
|
|
Theorem | cu2 10346 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
|
|
Theorem | irec 10347 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
|
|
Theorem | i2 10348 |
squared.
(Contributed by NM, 6-May-1999.)
|
|
|
Theorem | i3 10349 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
|
|
Theorem | i4 10350 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
|
|
Theorem | nnlesq 10351 |
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 10352 |
Taking to the -th power is the same as
using the
-th power instead, by i4 10350. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
|
|
Theorem | expnass 10353 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
|
|
Theorem | subsq 10354 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
|
|
Theorem | subsq2 10355 |
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 10356 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | subsqi 10357 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
|
|
Theorem | binom2 10358 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
|
|
Theorem | binom21 10359 |
Special case of binom2 10358 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
|
|
Theorem | binom2sub 10360 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
|
|
Theorem | binom2sub1 10361 |
Special case of binom2sub 10360 where
. (Contributed by AV,
2-Aug-2021.)
|
|
|
Theorem | binom2subi 10362 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
|
|
Theorem | mulbinom2 10363 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
|
|
Theorem | binom3 10364 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
|
|
Theorem | zesq 10365 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
|
|
Theorem | nnesq 10366 |
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 10367 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | bernneq2 10368 |
Variation of Bernoulli's inequality bernneq 10367. (Contributed by NM,
18-Oct-2007.)
|
|
|
Theorem | bernneq3 10369 |
A corollary of bernneq 10367. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
|
|
Theorem | expnbnd 10370* |
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
|
|
Theorem | expnlbnd 10371* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.)
|
|
|
Theorem | expnlbnd2 10372* |
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 10373 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | exp1d 10374 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expeq0d 10375 |
Positive integer exponentiation is 0 iff its mantissa is 0.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqvald 10376 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | sqcld 10377 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqeq0d 10378 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | expcld 10379 |
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expp1d 10380 |
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 10381 |
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 10382 |
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 10383 |
Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expclzapd 10384 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
# |
|
Theorem | expap0d 10385 |
Nonnegative integer exponentiation is nonzero if its mantissa is
nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
# # |
|
Theorem | expnegapd 10386 |
Value of a complex number raised to a negative power. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
#
|
|
Theorem | exprecapd 10387 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expp1zapd 10388 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expm1apd 10389 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
# |
|
Theorem | expsubapd 10390 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
#
|
|
Theorem | sqmuld 10391 |
Distribution of square over multiplication. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | sqdivapd 10392 |
Distribution of square over division. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
#
|
|
Theorem | expdivapd 10393 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
#
|
|
Theorem | mulexpd 10394 |
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 10395 |
Value of zero raised to a positive integer power. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reexpcld 10396 |
Closure of exponentiation of reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | expge0d 10397 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | expge1d 10398 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | sqoddm1div8 10399 |
A squared odd number minus 1 divided by 8 is the odd number multiplied
with its successor divided by 2. (Contributed by AV, 19-Jul-2021.)
|
|
|
Theorem | nnsqcld 10400 |
The naturals are closed under squaring. (Contributed by Mario Carneiro,
28-May-2016.)
|
|