Theorem List for Intuitionistic Logic Explorer - 10401-10500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zsqcl2 10401 |
The square of an integer is a nonnegative integer. (Contributed by Mario
Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
|
Theorem | sumsqeq0 10402 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqvali 10403 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | sqcli 10404 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![CC CC](bbc.gif) |
|
Theorem | sqeq0i 10405 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![0 0](0.gif) ![)
)](rp.gif) |
|
Theorem | sqmuli 10406 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqdivapi 10407 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
# ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | resqcli 10408 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![RR RR](bbr.gif) |
|
Theorem | sqgt0api 10409 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
![( (](lp.gif) # ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqge0i 10410 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) |
|
Theorem | lt2sqi 10411 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | le2sqi 10412 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sq11i 10413 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sq0 10414 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
![( (](lp.gif) ![0 0](0.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![0 0](0.gif) |
|
Theorem | sq0i 10415 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | sq0id 10416 |
If a number is zero, its square is zero. Deduction form of sq0i 10415.
Converse of sqeq0d 10454. (Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | sq1 10417 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
![( (](lp.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) |
|
Theorem | neg1sqe1 10418 |
![-u -u](shortminus.gif) squared is 1 (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) |
|
Theorem | sq2 10419 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![4 4](4.gif) |
|
Theorem | sq3 10420 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
![( (](lp.gif) ![3 3](3.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![9 9](9.gif) |
|
Theorem | sq4e2t8 10421 |
The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|
![( (](lp.gif) ![4 4](4.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![8 8](8.gif) ![) )](rp.gif) |
|
Theorem | cu2 10422 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![8 8](8.gif) |
|
Theorem | irec 10423 |
The reciprocal of .
(Contributed by NM, 11-Oct-1999.)
|
![( (](lp.gif) ![_i _i](rmi.gif)
![-u -u](shortminus.gif) ![_i _i](rmi.gif) |
|
Theorem | i2 10424 |
squared.
(Contributed by NM, 6-May-1999.)
|
![( (](lp.gif) ![_i _i](rmi.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) |
|
Theorem | i3 10425 |
cubed. (Contributed
by NM, 31-Jan-2007.)
|
![( (](lp.gif) ![_i _i](rmi.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![-u -u](shortminus.gif) ![_i _i](rmi.gif) |
|
Theorem | i4 10426 |
to the fourth power.
(Contributed by NM, 31-Jan-2007.)
|
![( (](lp.gif) ![_i _i](rmi.gif) ![^ ^](uparrow.gif) ![4 4](4.gif) ![1 1](1.gif) |
|
Theorem | nnlesq 10427 |
A positive integer is less than or equal to its square. (Contributed by
NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
|
![( (](lp.gif)
![( (](lp.gif) ![N N](_cn.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iexpcyc 10428 |
Taking to the -th power is the same as
using the
-th power instead, by i4 10426. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![_i _i](rmi.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![_i _i](rmi.gif) ![^ ^](uparrow.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expnass 10429 |
A counterexample showing that exponentiation is not associative.
(Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![3 3](3.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif)
![( (](lp.gif) ![3 3](3.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![3 3](3.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsq 10430 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsq2 10431 |
Express the difference of the squares of two numbers as a polynomial in
the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom2i 10432 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsqi 10433 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom2 10434 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom21 10435 |
Special case of binom2 10434 where
. (Contributed by Scott
Fenton,
11-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom2sub 10436 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom2sub1 10437 |
Special case of binom2sub 10436 where
. (Contributed by AV,
2-Aug-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom2subi 10438 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulbinom2 10439 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | binom3 10440 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zesq 10441 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![N N](_cn.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![2 2](2.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnesq 10442 |
A positive integer is even iff its square is even. (Contributed by NM,
20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![N N](_cn.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![2 2](2.gif) ![NN NN](bbn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | bernneq 10443 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | bernneq2 10444 |
Variation of Bernoulli's inequality bernneq 10443. (Contributed by NM,
18-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![N N](_cn.gif) ![1 1](1.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | bernneq3 10445 |
A corollary of bernneq 10443. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![P P](_cp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expnbnd 10446* |
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![k
k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expnlbnd 10447* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | expnlbnd2 10448* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![j j](_j.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![k
k](_k.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | exp0d 10449 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![0 0](0.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | exp1d 10450 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![1 1](1.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | expeq0d 10451 |
Positive integer exponentiation is 0 iff its mantissa is 0.
(Contributed by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![0 0](0.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | sqvald 10452 |
Value of square. Inference version. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqcld 10453 |
Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![CC
CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | sqeq0d 10454 |
A number is zero iff its square is zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![0 0](0.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | expcld 10455 |
Closure law for nonnegative integer exponentiation. (Contributed by
Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![CC
CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | expp1d 10456 |
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.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expaddd 10457 |
Sum of exponents law for nonnegative integer exponentiation.
Proposition 10-4.2(a) of [Gleason] p.
135. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expmuld 10458 |
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.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqrecapd 10459 |
Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expclzapd 10460 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | expap0d 10461 |
Nonnegative integer exponentiation is nonzero if its mantissa is
nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) # ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | expnegapd 10462 |
Value of a complex number raised to a negative power. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![-u -u](shortminus.gif) ![N N](_cn.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | exprecapd 10463 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by
Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expp1zapd 10464 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expm1apd 10465 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expsubapd 10466 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 12-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqmuld 10467 |
Distribution of square over multiplication. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqdivapd 10468 |
Distribution of square over division. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) #
![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expdivapd 10469 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) #
![0 0](0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulexpd 10470 |
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.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 0expd 10471 |
Value of zero raised to a positive integer power. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | reexpcld 10472 |
Closure of exponentiation of reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![RR
RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | expge0d 10473 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expge1d 10474 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sqoddm1div8 10475 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif)
![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) ![8 8](8.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | nnsqcld 10476 |
The naturals are closed under squaring. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![NN
NN](bbn.gif) ![) )](rp.gif) |
|
Theorem | nnexpcld 10477 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![NN
NN](bbn.gif) ![) )](rp.gif) |
|
Theorem | nn0expcld 10478 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![NN0
NN0](_bbn0.gif) ![) )](rp.gif) |
|
Theorem | rpexpcld 10479 |
Closure law for exponentiation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
|
Theorem | reexpclzapd 10480 |
Closure of exponentiation of reals. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | resqcld 10481 |
Closure of square in reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR
RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | sqge0d 10482 |
A square of a real is nonnegative. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | sqgt0apd 10483 |
The square of a real apart from zero is positive. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | leexp2ad 10484 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | leexp2rd 10485 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | lt2sqd 10486 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | le2sqd 10487 |
The square function on nonnegative reals is monotonic. (Contributed by
Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sq11d 10488 |
The square function is one-to-one for nonnegative reals. (Contributed
by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | sq11ap 10489 |
Analogue to sq11 10396 but for apartness. (Contributed by Jim
Kingdon,
12-Aug-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) # ![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) #
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | sq10 10490 |
The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by
AV, 1-Aug-2021.)
|
;![1 1](1.gif) ![0 0](0.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ;;![1 1](1.gif) ![0 0](0.gif) ![0 0](0.gif) |
|
Theorem | sq10e99m1 10491 |
The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.)
(Revised by AV, 1-Aug-2021.)
|
;![1 1](1.gif) ![0 0](0.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ;![9 9](9.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | 3dec 10492 |
A "decimal constructor" which is used to build up "decimal
integers" or
"numeric terms" in base 10 with 3 "digits".
(Contributed by AV,
14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|
;;![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ;![1 1](1.gif) ![0
0](0.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![A A](_ca.gif) ;![1 1](1.gif) ![B B](_cb.gif) ![) )](rp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | expcanlem 10493 |
Lemma for expcan 10494. Proving the order in one direction.
(Contributed
by Jim Kingdon, 29-Jan-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expcan 10494 |
Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.)
(Revised by Mario Carneiro, 4-Jun-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | expcand 10495 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) |
|
Theorem | apexp1 10496 |
Exponentiation and apartness. (Contributed by Jim Kingdon,
9-Jul-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) #
![( (](lp.gif) ![B B](_cb.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) # ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.6.7 Ordered pair theorem for nonnegative
integers
|
|
Theorem | nn0le2msqd 10497 |
The square function on nonnegative integers is monotonic. (Contributed
by Jim Kingdon, 31-Oct-2021.)
|
![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nn0opthlem1d 10498 |
A rather pretty lemma for nn0opth2 10502. (Contributed by Jim Kingdon,
31-Oct-2021.)
|
![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nn0opthlem2d 10499 |
Lemma for nn0opth2 10502. (Contributed by Jim Kingdon, 31-Oct-2021.)
|
![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nn0opthd 10500 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. We can represent an
ordered pair of nonnegative
integers and
by ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) . If
two such ordered pairs are equal, their first elements are equal and
their second elements are equal. Contrast this ordered pair
representation with the standard one df-op 3541 that works for any set.
(Contributed by Jim Kingdon, 31-Oct-2021.)
|
![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |