Theorem List for Intuitionistic Logic Explorer - 8901-9000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3t3e9 8901 |
3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
|
![( (](lp.gif) ![3 3](3.gif) ![9 9](9.gif) |
|
Theorem | 4t2e8 8902 |
4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
|
![( (](lp.gif) ![2 2](2.gif) ![8 8](8.gif) |
|
Theorem | 2t0e0 8903 |
2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
![( (](lp.gif) ![0 0](0.gif) ![0 0](0.gif) |
|
Theorem | 4d2e2 8904 |
One half of four is two. (Contributed by NM, 3-Sep-1999.)
|
![( (](lp.gif) ![2 2](2.gif) ![2 2](2.gif) |
|
Theorem | 2nn 8905 |
2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
|
![NN NN](bbn.gif) |
|
Theorem | 3nn 8906 |
3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|
![NN NN](bbn.gif) |
|
Theorem | 4nn 8907 |
4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
|
![NN NN](bbn.gif) |
|
Theorem | 5nn 8908 |
5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![NN NN](bbn.gif) |
|
Theorem | 6nn 8909 |
6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![NN NN](bbn.gif) |
|
Theorem | 7nn 8910 |
7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![NN NN](bbn.gif) |
|
Theorem | 8nn 8911 |
8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![NN NN](bbn.gif) |
|
Theorem | 9nn 8912 |
9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
|
![NN NN](bbn.gif) |
|
Theorem | 1lt2 8913 |
1 is less than 2. (Contributed by NM, 24-Feb-2005.)
|
![2 2](2.gif) |
|
Theorem | 2lt3 8914 |
2 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
![3 3](3.gif) |
|
Theorem | 1lt3 8915 |
1 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
![3 3](3.gif) |
|
Theorem | 3lt4 8916 |
3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![4 4](4.gif) |
|
Theorem | 2lt4 8917 |
2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![4 4](4.gif) |
|
Theorem | 1lt4 8918 |
1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![4 4](4.gif) |
|
Theorem | 4lt5 8919 |
4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![5 5](5.gif) |
|
Theorem | 3lt5 8920 |
3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![5 5](5.gif) |
|
Theorem | 2lt5 8921 |
2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![5 5](5.gif) |
|
Theorem | 1lt5 8922 |
1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![5 5](5.gif) |
|
Theorem | 5lt6 8923 |
5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![6 6](6.gif) |
|
Theorem | 4lt6 8924 |
4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![6 6](6.gif) |
|
Theorem | 3lt6 8925 |
3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![6 6](6.gif) |
|
Theorem | 2lt6 8926 |
2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![6 6](6.gif) |
|
Theorem | 1lt6 8927 |
1 is less than 6. (Contributed by NM, 19-Oct-2012.)
|
![6 6](6.gif) |
|
Theorem | 6lt7 8928 |
6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![7 7](7.gif) |
|
Theorem | 5lt7 8929 |
5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![7 7](7.gif) |
|
Theorem | 4lt7 8930 |
4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![7 7](7.gif) |
|
Theorem | 3lt7 8931 |
3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![7 7](7.gif) |
|
Theorem | 2lt7 8932 |
2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![7 7](7.gif) |
|
Theorem | 1lt7 8933 |
1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![7 7](7.gif) |
|
Theorem | 7lt8 8934 |
7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 6lt8 8935 |
6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 5lt8 8936 |
5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 4lt8 8937 |
4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 3lt8 8938 |
3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 2lt8 8939 |
2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 1lt8 8940 |
1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
![8 8](8.gif) |
|
Theorem | 8lt9 8941 |
8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.)
|
![9 9](9.gif) |
|
Theorem | 7lt9 8942 |
7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 6lt9 8943 |
6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 5lt9 8944 |
5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 4lt9 8945 |
4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 3lt9 8946 |
3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 2lt9 8947 |
2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 1lt9 8948 |
1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
![9 9](9.gif) |
|
Theorem | 0ne2 8949 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
![2 2](2.gif) |
|
Theorem | 1ne2 8950 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
![2 2](2.gif) |
|
Theorem | 1ap2 8951 |
1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.)
|
# ![2 2](2.gif) |
|
Theorem | 1le2 8952 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
![2 2](2.gif) |
|
Theorem | 2cnne0 8953 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | 2rene0 8954 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | 1le3 8955 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
![3 3](3.gif) |
|
Theorem | neg1mulneg1e1 8956 |
![-u -u](shortminus.gif) ![-u -u](shortminus.gif) is
1 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![1 1](1.gif) |
|
Theorem | halfre 8957 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) |
|
Theorem | halfcn 8958 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
![( (](lp.gif) ![2 2](2.gif) ![CC CC](bbc.gif) |
|
Theorem | halfgt0 8959 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
|
Theorem | halfge0 8960 |
One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
|
Theorem | halflt1 8961 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
![( (](lp.gif) ![2 2](2.gif)
![1 1](1.gif) |
|
Theorem | 1mhlfehlf 8962 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
![( (](lp.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
|
Theorem | 8th4div3 8963 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![8
8](8.gif) ![( (](lp.gif)
![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![6 6](6.gif) ![) )](rp.gif) |
|
Theorem | halfpm6th 8964 |
One half plus or minus one sixth. (Contributed by Paul Chapman,
17-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![6 6](6.gif) ![)
)](rp.gif) ![( (](lp.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![6 6](6.gif) ![)
)](rp.gif) ![( (](lp.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | it0e0 8965 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
![( (](lp.gif) ![0 0](0.gif) ![0 0](0.gif) |
|
Theorem | 2mulicn 8966 |
![( (](lp.gif) ![_i _i](rmi.gif) (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
![( (](lp.gif) ![_i _i](rmi.gif)
![CC CC](bbc.gif) |
|
Theorem | iap0 8967 |
The imaginary unit
is apart from zero. (Contributed by Jim
Kingdon, 9-Mar-2020.)
|
# ![0 0](0.gif) |
|
Theorem | 2muliap0 8968 |
is apart from zero. (Contributed by Jim Kingdon,
9-Mar-2020.)
|
![( (](lp.gif) ![_i _i](rmi.gif) # ![0 0](0.gif) |
|
Theorem | 2muline0 8969 |
![( (](lp.gif) ![_i _i](rmi.gif) . See also 2muliap0 8968. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
![( (](lp.gif) ![_i _i](rmi.gif) ![0 0](0.gif) |
|
4.4.5 Simple number properties
|
|
Theorem | halfcl 8970 |
Closure of half of a number (common case). (Contributed by NM,
1-Jan-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | rehalfcl 8971 |
Real closure of half. (Contributed by NM, 1-Jan-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | half0 8972 |
Half of a number is zero iff the number is zero. (Contributed by NM,
20-Apr-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif)
![0 0](0.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | 2halves 8973 |
Two halves make a whole. (Contributed by NM, 11-Apr-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | halfpos2 8974 |
A number is positive iff its half is positive. (Contributed by NM,
10-Apr-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | halfpos 8975 |
A positive number is greater than its half. (Contributed by NM,
28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | halfnneg2 8976 |
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9-Dec-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | halfaddsubcl 8977 |
Closure of half-sum and half-difference. (Contributed by Paul Chapman,
12-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![2 2](2.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![2
2](2.gif) ![CC CC](bbc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | halfaddsub 8978 |
Sum and difference of half-sum and half-difference. (Contributed by Paul
Chapman, 12-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![2 2](2.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | lt2halves 8979 |
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13-Dec-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addltmul 8980 |
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24-Sep-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nominpos 8981* |
There is no smallest positive real number. (Contributed by NM,
28-Oct-2004.)
|
![E. E.](exists.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif)
![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | avglt1 8982 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | avglt2 8983 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![2 2](2.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | avgle1 8984 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | avgle2 8985 |
Ordering property for average. (Contributed by Jeff Hankins,
15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![2 2](2.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | 2timesd 8986 |
Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | times2d 8987 |
A number times 2. (Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | halfcld 8988 |
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![CC
CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | 2halvesd 8989 |
Two halves make a whole. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | rehalfcld 8990 |
Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR
RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | lt2halvesd 8991 |
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | rehalfcli 8992 |
Half a real number is real. Inference form. (Contributed by David
Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![2
2](2.gif) ![RR RR](bbr.gif) |
|
Theorem | add1p1 8993 |
Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![1 1](1.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sub1m1 8994 |
Subtracting two times 1 from a number. (Contributed by AV,
23-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![1 1](1.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cnm2m1cnm3 8995 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![1 1](1.gif) ![( (](lp.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xp1d2m1eqxm1d2 8996 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2
2](2.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | div4p1lem1div2 8997 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.4.6 The Archimedean property
|
|
Theorem | arch 8998* |
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.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![n n](_n.gif) ![) )](rp.gif) |
|
Theorem | nnrecl 8999* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![n n](_n.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | bndndx 9000* |
A bounded real sequence ![A A](_ca.gif) ![( (](lp.gif) ![k k](_k.gif) is less than or equal to at least
one of its indices. (Contributed by NM, 18-Jan-2008.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![x x](_x.gif) ![E. E.](exists.gif) ![k k](_k.gif) ![) )](rp.gif) |