Theorem List for Intuitionistic Logic Explorer - 8901-9000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | halfre 8901 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | halfcn 8902 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | halfgt0 8903 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | halfge0 8904 |
One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|
|
|
Theorem | halflt1 8905 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | 1mhlfehlf 8906 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
|
|
Theorem | 8th4div3 8907 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
|
|
Theorem | halfpm6th 8908 |
One half plus or minus one sixth. (Contributed by Paul Chapman,
17-Jan-2008.)
|
|
|
Theorem | it0e0 8909 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | 2mulicn 8910 |
(common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | iap0 8911 |
The imaginary unit
is apart from zero. (Contributed by Jim
Kingdon, 9-Mar-2020.)
|
# |
|
Theorem | 2muliap0 8912 |
is apart from zero. (Contributed by Jim Kingdon,
9-Mar-2020.)
|
# |
|
Theorem | 2muline0 8913 |
. See also 2muliap0 8912. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
4.4.5 Simple number properties
|
|
Theorem | halfcl 8914 |
Closure of half of a number (common case). (Contributed by NM,
1-Jan-2006.)
|
|
|
Theorem | rehalfcl 8915 |
Real closure of half. (Contributed by NM, 1-Jan-2006.)
|
|
|
Theorem | half0 8916 |
Half of a number is zero iff the number is zero. (Contributed by NM,
20-Apr-2006.)
|
|
|
Theorem | 2halves 8917 |
Two halves make a whole. (Contributed by NM, 11-Apr-2005.)
|
|
|
Theorem | halfpos2 8918 |
A number is positive iff its half is positive. (Contributed by NM,
10-Apr-2005.)
|
|
|
Theorem | halfpos 8919 |
A positive number is greater than its half. (Contributed by NM,
28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | halfnneg2 8920 |
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9-Dec-2005.)
|
|
|
Theorem | halfaddsubcl 8921 |
Closure of half-sum and half-difference. (Contributed by Paul Chapman,
12-Oct-2007.)
|
|
|
Theorem | halfaddsub 8922 |
Sum and difference of half-sum and half-difference. (Contributed by Paul
Chapman, 12-Oct-2007.)
|
|
|
Theorem | lt2halves 8923 |
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13-Dec-2006.)
|
|
|
Theorem | addltmul 8924 |
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24-Sep-2010.)
|
|
|
Theorem | nominpos 8925* |
There is no smallest positive real number. (Contributed by NM,
28-Oct-2004.)
|
|
|
Theorem | avglt1 8926 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avglt2 8927 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avgle1 8928 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
|
|
Theorem | avgle2 8929 |
Ordering property for average. (Contributed by Jeff Hankins,
15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|
|
|
Theorem | 2timesd 8930 |
Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | times2d 8931 |
A number times 2. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | halfcld 8932 |
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | 2halvesd 8933 |
Two halves make a whole. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | rehalfcld 8934 |
Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt2halvesd 8935 |
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | rehalfcli 8936 |
Half a real number is real. Inference form. (Contributed by David
Moews, 28-Feb-2017.)
|
|
|
Theorem | add1p1 8937 |
Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.)
|
|
|
Theorem | sub1m1 8938 |
Subtracting two times 1 from a number. (Contributed by AV,
23-Oct-2018.)
|
|
|
Theorem | cnm2m1cnm3 8939 |
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 8940 |
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 8941 |
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.)
|
|
|
4.4.6 The Archimedean property
|
|
Theorem | arch 8942* |
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 8943* |
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 8944* |
A bounded real sequence is less than or equal to at least
one of its indices. (Contributed by NM, 18-Jan-2008.)
|
|
|
4.4.7 Nonnegative integers (as a subset of
complex numbers)
|
|
Syntax | cn0 8945 |
Extend class notation to include the class of nonnegative integers.
|
|
|
Definition | df-n0 8946 |
Define the set of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.)
|
|
|
Theorem | elnn0 8947 |
Nonnegative integers expressed in terms of naturals and zero.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nnssnn0 8948 |
Positive naturals are a subset of nonnegative integers. (Contributed by
Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0ssre 8949 |
Nonnegative integers are a subset of the reals. (Contributed by Raph
Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0sscn 8950 |
Nonnegative integers are a subset of the complex numbers.) (Contributed
by NM, 9-May-2004.)
|
|
|
Theorem | nn0ex 8951 |
The set of nonnegative integers exists. (Contributed by NM,
18-Jul-2004.)
|
|
|
Theorem | nnnn0 8952 |
A positive integer is a nonnegative integer. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nnnn0i 8953 |
A positive integer is a nonnegative integer. (Contributed by NM,
20-Jun-2005.)
|
|
|
Theorem | nn0re 8954 |
A nonnegative integer is a real number. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0cn 8955 |
A nonnegative integer is a complex number. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0rei 8956 |
A nonnegative integer is a real number. (Contributed by NM,
14-May-2003.)
|
|
|
Theorem | nn0cni 8957 |
A nonnegative integer is a complex number. (Contributed by NM,
14-May-2003.)
|
|
|
Theorem | dfn2 8958 |
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 8959 |
The positive integer property expressed in terms of difference from zero.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
|
|
Theorem | 0nn0 8960 |
0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | 1nn0 8961 |
1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | 2nn0 8962 |
2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | 3nn0 8963 |
3 is a nonnegative integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | 4nn0 8964 |
4 is a nonnegative integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | 5nn0 8965 |
5 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 6nn0 8966 |
6 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 7nn0 8967 |
7 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 8nn0 8968 |
8 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 9nn0 8969 |
9 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | nn0ge0 8970 |
A nonnegative integer is greater than or equal to zero. (Contributed by
NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nn0nlt0 8971 |
A nonnegative integer is not less than zero. (Contributed by NM,
9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0ge0i 8972 |
Nonnegative integers are nonnegative. (Contributed by Raph Levien,
10-Dec-2002.)
|
|
|
Theorem | nn0le0eq0 8973 |
A nonnegative integer is less than or equal to zero iff it is equal to
zero. (Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | nn0p1gt0 8974 |
A nonnegative integer increased by 1 is greater than 0. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
|
|
Theorem | nnnn0addcl 8975 |
A positive integer plus a nonnegative integer is a positive integer.
(Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro,
16-May-2014.)
|
|
|
Theorem | nn0nnaddcl 8976 |
A nonnegative integer plus a positive integer is a positive integer.
(Contributed by NM, 22-Dec-2005.)
|
|
|
Theorem | 0mnnnnn0 8977 |
The result of subtracting a positive integer from 0 is not a nonnegative
integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
|
|
|
Theorem | un0addcl 8978 |
If is closed under
addition, then so is
.
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | un0mulcl 8979 |
If is closed under
multiplication, then so is .
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | nn0addcl 8980 |
Closure of addition of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | nn0mulcl 8981 |
Closure of multiplication of nonnegative integers. (Contributed by NM,
22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | nn0addcli 8982 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0mulcli 8983 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0p1nn 8984 |
A nonnegative integer plus 1 is a positive integer. (Contributed by Raph
Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | peano2nn0 8985 |
Second Peano postulate for nonnegative integers. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nnm1nn0 8986 |
A positive integer minus 1 is a nonnegative integer. (Contributed by
Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro,
16-May-2014.)
|
|
|
Theorem | elnn0nn 8987 |
The nonnegative integer property expressed in terms of positive integers.
(Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro,
16-May-2014.)
|
|
|
Theorem | elnnnn0 8988 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-May-2004.)
|
|
|
Theorem | elnnnn0b 8989 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 1-Sep-2005.)
|
|
|
Theorem | elnnnn0c 8990 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-Jan-2006.)
|
|
|
Theorem | nn0addge1 8991 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0addge2 8992 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0addge1i 8993 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0addge2i 8994 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0le2xi 8995 |
A nonnegative integer is less than or equal to twice itself.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0lele2xi 8996 |
'Less than or equal to' implies 'less than or equal to twice' for
nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0supp 8997 |
Two ways to write the support of a function on . (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | nnnn0d 8998 |
A positive integer is a nonnegative integer. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0red 8999 |
A nonnegative integer is a real number. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nn0cnd 9000 |
A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|