Theorem List for Intuitionistic Logic Explorer - 8101-8200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 6lt7 8101 |
6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 5lt7 8102 |
5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 4lt7 8103 |
4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 3lt7 8104 |
3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt7 8105 |
2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt7 8106 |
1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 7lt8 8107 |
7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 6lt8 8108 |
6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 5lt8 8109 |
5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 4lt8 8110 |
4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 3lt8 8111 |
3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 2lt8 8112 |
2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 1lt8 8113 |
1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
|
|
Theorem | 8lt9 8114 |
8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.)
|
|
|
Theorem | 7lt9 8115 |
7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 6lt9 8116 |
6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 5lt9 8117 |
5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 4lt9 8118 |
4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 3lt9 8119 |
3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 2lt9 8120 |
2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 1lt9 8121 |
1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 9lt10 8122 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.)
|
|
|
Theorem | 8lt10 8123 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.)
|
|
|
Theorem | 7lt10 8124 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
|
|
Theorem | 6lt10 8125 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
|
|
Theorem | 5lt10 8126 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
|
|
Theorem | 4lt10 8127 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
|
|
Theorem | 3lt10 8128 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
|
|
Theorem | 2lt10 8129 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
|
|
Theorem | 1lt10 8130 |
1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
|
|
Theorem | 0ne2 8131 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 1ne2 8132 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
|
|
Theorem | 1le2 8133 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 2cnne0 8134 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
|
|
Theorem | 2rene0 8135 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 1le3 8136 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | neg1mulneg1e1 8137 |
is
1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | halfre 8138 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | halfcn 8139 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | halfgt0 8140 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | halfge0 8141 |
One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|
|
|
Theorem | halflt1 8142 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | 1mhlfehlf 8143 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
|
|
Theorem | 8th4div3 8144 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
|
|
Theorem | halfpm6th 8145 |
One half plus or minus one sixth. (Contributed by Paul Chapman,
17-Jan-2008.)
|
|
|
Theorem | it0e0 8146 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | 2mulicn 8147 |
(common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | iap0 8148 |
The imaginary unit
is apart from zero. (Contributed by Jim
Kingdon, 9-Mar-2020.)
|
# |
|
Theorem | 2muliap0 8149 |
is apart from zero. (Contributed by Jim Kingdon,
9-Mar-2020.)
|
# |
|
Theorem | 2muline0 8150 |
. See also 2muliap0 8149. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
3.4.5 Simple number properties
|
|
Theorem | halfcl 8151 |
Closure of half of a number (common case). (Contributed by NM,
1-Jan-2006.)
|
|
|
Theorem | rehalfcl 8152 |
Real closure of half. (Contributed by NM, 1-Jan-2006.)
|
|
|
Theorem | half0 8153 |
Half of a number is zero iff the number is zero. (Contributed by NM,
20-Apr-2006.)
|
|
|
Theorem | 2halves 8154 |
Two halves make a whole. (Contributed by NM, 11-Apr-2005.)
|
|
|
Theorem | halfpos2 8155 |
A number is positive iff its half is positive. (Contributed by NM,
10-Apr-2005.)
|
|
|
Theorem | halfpos 8156 |
A positive number is greater than its half. (Contributed by NM,
28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | halfnneg2 8157 |
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9-Dec-2005.)
|
|
|
Theorem | halfaddsubcl 8158 |
Closure of half-sum and half-difference. (Contributed by Paul Chapman,
12-Oct-2007.)
|
|
|
Theorem | halfaddsub 8159 |
Sum and difference of half-sum and half-difference. (Contributed by Paul
Chapman, 12-Oct-2007.)
|
|
|
Theorem | lt2halves 8160 |
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13-Dec-2006.)
|
|
|
Theorem | addltmul 8161 |
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24-Sep-2010.)
|
|
|
Theorem | nominpos 8162* |
There is no smallest positive real number. (Contributed by NM,
28-Oct-2004.)
|
|
|
Theorem | avglt1 8163 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avglt2 8164 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avgle1 8165 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avgle2 8166 |
Ordering property for average. (Contributed by Jeff Hankins,
15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|
|
|
Theorem | 2timesd 8167 |
Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | times2d 8168 |
A number times 2. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | halfcld 8169 |
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | 2halvesd 8170 |
Two halves make a whole. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | rehalfcld 8171 |
Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt2halvesd 8172 |
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | rehalfcli 8173 |
Half a real number is real. Inference form. (Contributed by David
Moews, 28-Feb-2017.)
|
|
|
Theorem | add1p1 8174 |
Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.)
|
|
|
Theorem | sub1m1 8175 |
Subtracting two times 1 from a number. (Contributed by AV,
23-Oct-2018.)
|
|
|
Theorem | cnm2m1cnm3 8176 |
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 | div4p1lem1div2 8177 |
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 8178* |
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 8179* |
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 8180* |
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 8181 |
Extend class notation to include the class of nonnegative integers.
|
|
|
Definition | df-n0 8182 |
Define the set of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.)
|
|
|
Theorem | elnn0 8183 |
Nonnegative integers expressed in terms of naturals and zero.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nnssnn0 8184 |
Positive naturals are a subset of nonnegative integers. (Contributed by
Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0ssre 8185 |
Nonnegative integers are a subset of the reals. (Contributed by Raph
Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0sscn 8186 |
Nonnegative integers are a subset of the complex numbers.) (Contributed
by NM, 9-May-2004.)
|
|
|
Theorem | nn0ex 8187 |
The set of nonnegative integers exists. (Contributed by NM,
18-Jul-2004.)
|
|
|
Theorem | nnnn0 8188 |
A positive integer is a nonnegative integer. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nnnn0i 8189 |
A positive integer is a nonnegative integer. (Contributed by NM,
20-Jun-2005.)
|
|
|
Theorem | nn0re 8190 |
A nonnegative integer is a real number. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0cn 8191 |
A nonnegative integer is a complex number. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0rei 8192 |
A nonnegative integer is a real number. (Contributed by NM,
14-May-2003.)
|
|
|
Theorem | nn0cni 8193 |
A nonnegative integer is a complex number. (Contributed by NM,
14-May-2003.)
|
|
|
Theorem | dfn2 8194 |
The set of positive integers defined in terms of nonnegative integers.
(Contributed by NM, 23-Sep-2007.) (Proof shortened by Mario Carneiro,
13-Feb-2013.)
|
|
|
Theorem | elnnne0 8195 |
The positive integer property expressed in terms of difference from zero.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
|
|
Theorem | 0nn0 8196 |
0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | 1nn0 8197 |
1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | 2nn0 8198 |
2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | 3nn0 8199 |
3 is a nonnegative integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | 4nn0 8200 |
4 is a nonnegative integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|