Theorem List for Intuitionistic Logic Explorer - 8201-8300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 1lt2 8201 |
1 is less than 2. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | 2lt3 8202 |
2 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
|
|
Theorem | 1lt3 8203 |
1 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
|
|
Theorem | 3lt4 8204 |
3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt4 8205 |
2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt4 8206 |
1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 4lt5 8207 |
4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 3lt5 8208 |
3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt5 8209 |
2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt5 8210 |
1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 5lt6 8211 |
5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 4lt6 8212 |
4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 3lt6 8213 |
3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt6 8214 |
2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt6 8215 |
1 is less than 6. (Contributed by NM, 19-Oct-2012.)
|
|
|
Theorem | 6lt7 8216 |
6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 5lt7 8217 |
5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 4lt7 8218 |
4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 3lt7 8219 |
3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt7 8220 |
2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt7 8221 |
1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 7lt8 8222 |
7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 6lt8 8223 |
6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 5lt8 8224 |
5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 4lt8 8225 |
4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 3lt8 8226 |
3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt8 8227 |
2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt8 8228 |
1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 8lt9 8229 |
8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.)
|
|
|
Theorem | 7lt9 8230 |
7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 6lt9 8231 |
6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 5lt9 8232 |
5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 4lt9 8233 |
4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 3lt9 8234 |
3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 2lt9 8235 |
2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 1lt9 8236 |
1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 0ne2 8237 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 1ne2 8238 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
|
|
Theorem | 1le2 8239 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 2cnne0 8240 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
|
|
Theorem | 2rene0 8241 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 1le3 8242 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | neg1mulneg1e1 8243 |
is
1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | halfre 8244 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | halfcn 8245 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | halfgt0 8246 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | halfge0 8247 |
One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|
|
|
Theorem | halflt1 8248 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | 1mhlfehlf 8249 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
|
|
Theorem | 8th4div3 8250 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
|
|
Theorem | halfpm6th 8251 |
One half plus or minus one sixth. (Contributed by Paul Chapman,
17-Jan-2008.)
|
|
|
Theorem | it0e0 8252 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | 2mulicn 8253 |
(common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | iap0 8254 |
The imaginary unit
is apart from zero. (Contributed by Jim
Kingdon, 9-Mar-2020.)
|
# |
|
Theorem | 2muliap0 8255 |
is apart from zero. (Contributed by Jim Kingdon,
9-Mar-2020.)
|
# |
|
Theorem | 2muline0 8256 |
. See also 2muliap0 8255. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
3.4.5 Simple number properties
|
|
Theorem | halfcl 8257 |
Closure of half of a number (common case). (Contributed by NM,
1-Jan-2006.)
|
|
|
Theorem | rehalfcl 8258 |
Real closure of half. (Contributed by NM, 1-Jan-2006.)
|
|
|
Theorem | half0 8259 |
Half of a number is zero iff the number is zero. (Contributed by NM,
20-Apr-2006.)
|
|
|
Theorem | 2halves 8260 |
Two halves make a whole. (Contributed by NM, 11-Apr-2005.)
|
|
|
Theorem | halfpos2 8261 |
A number is positive iff its half is positive. (Contributed by NM,
10-Apr-2005.)
|
|
|
Theorem | halfpos 8262 |
A positive number is greater than its half. (Contributed by NM,
28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | halfnneg2 8263 |
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9-Dec-2005.)
|
|
|
Theorem | halfaddsubcl 8264 |
Closure of half-sum and half-difference. (Contributed by Paul Chapman,
12-Oct-2007.)
|
|
|
Theorem | halfaddsub 8265 |
Sum and difference of half-sum and half-difference. (Contributed by Paul
Chapman, 12-Oct-2007.)
|
|
|
Theorem | lt2halves 8266 |
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13-Dec-2006.)
|
|
|
Theorem | addltmul 8267 |
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24-Sep-2010.)
|
|
|
Theorem | nominpos 8268* |
There is no smallest positive real number. (Contributed by NM,
28-Oct-2004.)
|
|
|
Theorem | avglt1 8269 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avglt2 8270 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avgle1 8271 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avgle2 8272 |
Ordering property for average. (Contributed by Jeff Hankins,
15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|
|
|
Theorem | 2timesd 8273 |
Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | times2d 8274 |
A number times 2. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | halfcld 8275 |
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | 2halvesd 8276 |
Two halves make a whole. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | rehalfcld 8277 |
Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt2halvesd 8278 |
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | rehalfcli 8279 |
Half a real number is real. Inference form. (Contributed by David
Moews, 28-Feb-2017.)
|
|
|
Theorem | add1p1 8280 |
Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.)
|
|
|
Theorem | sub1m1 8281 |
Subtracting two times 1 from a number. (Contributed by AV,
23-Oct-2018.)
|
|
|
Theorem | cnm2m1cnm3 8282 |
Subtracting 2 and afterwards 1 from a number results in the difference
between the number and 3. (Contributed by Alexander van der Vekens,
16-Sep-2018.)
|
|
|
Theorem | xp1d2m1eqxm1d2 8283 |
A complex number increased by 1, then divided by 2, then decreased by 1
equals the complex number decreased by 1 and then divided by 2.
(Contributed by AV, 24-May-2020.)
|
|
|
Theorem | div4p1lem1div2 8284 |
An integer greater than 5, divided by 4 and increased by 1, is less than
or equal to the half of the integer minus 1. (Contributed by AV,
8-Jul-2021.)
|
|
|
3.4.6 The Archimedean property
|
|
Theorem | arch 8285* |
Archimedean property of real numbers. For any real number, there is an
integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed
by NM, 21-Jan-1997.)
|
|
|
Theorem | nnrecl 8286* |
There exists a positive integer whose reciprocal is less than a given
positive real. Exercise 3 of [Apostol]
p. 28. (Contributed by NM,
8-Nov-2004.)
|
|
|
Theorem | bndndx 8287* |
A bounded real sequence is less than or equal to at least
one of its indices. (Contributed by NM, 18-Jan-2008.)
|
|
|
3.4.7 Nonnegative integers (as a subset of
complex numbers)
|
|
Syntax | cn0 8288 |
Extend class notation to include the class of nonnegative integers.
|
|
|
Definition | df-n0 8289 |
Define the set of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.)
|
|
|
Theorem | elnn0 8290 |
Nonnegative integers expressed in terms of naturals and zero.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nnssnn0 8291 |
Positive naturals are a subset of nonnegative integers. (Contributed by
Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0ssre 8292 |
Nonnegative integers are a subset of the reals. (Contributed by Raph
Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0sscn 8293 |
Nonnegative integers are a subset of the complex numbers.) (Contributed
by NM, 9-May-2004.)
|
|
|
Theorem | nn0ex 8294 |
The set of nonnegative integers exists. (Contributed by NM,
18-Jul-2004.)
|
|
|
Theorem | nnnn0 8295 |
A positive integer is a nonnegative integer. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nnnn0i 8296 |
A positive integer is a nonnegative integer. (Contributed by NM,
20-Jun-2005.)
|
|
|
Theorem | nn0re 8297 |
A nonnegative integer is a real number. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0cn 8298 |
A nonnegative integer is a complex number. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0rei 8299 |
A nonnegative integer is a real number. (Contributed by NM,
14-May-2003.)
|
|
|
Theorem | nn0cni 8300 |
A nonnegative integer is a complex number. (Contributed by NM,
14-May-2003.)
|
|