Theorem List for Intuitionistic Logic Explorer - 8801-8900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | divlt1lt 8801 |
A real number divided by a positive real number is less than 1 iff the
real number is less than the positive real number. (Contributed by AV,
25-May-2020.)
|
|
|
Theorem | divle1le 8802 |
A real number divided by a positive real number is less than or equal to 1
iff the real number is less than or equal to the positive real number.
(Contributed by AV, 29-Jun-2021.)
|
|
|
Theorem | ledivge1le 8803 |
If a number is less than or equal to another number, the number divided by
a positive number greater than or equal to one is less than or equal to
the other number. (Contributed by AV, 29-Jun-2021.)
|
|
|
Theorem | ge0p1rpd 8804 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rerpdivcld 8805 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltsubrpd 8806 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrpd 8807 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrp2d 8808 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt11d 8809 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt12d 8810 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | gt0divd 8811 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ge0divd 8812 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpgecld 8813 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge0d 8814 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1d 8815 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul2d 8816 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | lemul1d 8817 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul2d 8818 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv1d 8819 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv1d 8820 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmuldivd 8821 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmuldiv2d 8822 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemuldivd 8823 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lemuldiv2d 8824 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltdivmuld 8825 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdivmul2d 8826 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmuld 8827 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmul2d 8828 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1dd 8829 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltmul2dd 8830 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
30-May-2016.)
|
|
|
Theorem | ltdiv1dd 8831 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv1dd 8832 |
Division of both sides of a less than or equal to relation by a
positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv12ad 8833 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv23d 8834 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv23d 8835 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lt2mul2divd 8836 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | nnledivrp 8837 |
Division of a positive integer by a positive number is less than or equal
to the integer iff the number is greater than or equal to 1. (Contributed
by AV, 19-Jun-2021.)
|
|
|
Theorem | nn0ledivnn 8838 |
Division of a nonnegative integer by a positive integer is less than or
equal to the integer. (Contributed by AV, 19-Jun-2021.)
|
|
|
Theorem | addlelt 8839 |
If the sum of a real number and a positive real number is less than or
equal to a third real number, the first real number is less than the third
real number. (Contributed by AV, 1-Jul-2021.)
|
|
|
3.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 8840 |
Extend class notation to include the negative of an extended real.
|
|
|
Syntax | cxad 8841 |
Extend class notation to include addition of extended reals.
|
|
|
Syntax | cxmu 8842 |
Extend class notation to include multiplication of extended reals.
|
|
|
Definition | df-xneg 8843 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
|
|
Definition | df-xadd 8844* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Definition | df-xmul 8845* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | pnfxr 8846 |
Plus infinity belongs to the set of extended reals. (Contributed by NM,
13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
|
|
|
Theorem | pnfex 8847 |
Plus infinity exists (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | mnfxr 8848 |
Minus infinity belongs to the set of extended reals. (Contributed by NM,
13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof
shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltxr 8849 |
The 'less than' binary relation on the set of extended reals.
Definition 12-3.1 of [Gleason] p. 173.
(Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | elxr 8850 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | pnfnemnf 8851 |
Plus and minus infinity are different elements of . (Contributed
by NM, 14-Oct-2005.)
|
|
|
Theorem | mnfnepnf 8852 |
Minus and plus infinity are different (common case). (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | xrnemnf 8853 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrnepnf 8854 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrltnr 8855 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | ltpnf 8856 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | 0ltpnf 8857 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnflt 8858 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnflt0 8859 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnfltpnf 8860 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnfltxr 8861 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | pnfnlt 8862 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | nltmnf 8863 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | pnfge 8864 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
|
|
Theorem | 0lepnf 8865 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | nn0pnfge0 8866 |
If a number is a nonnegative integer or positive infinity, it is greater
than or equal to 0. (Contributed by Alexander van der Vekens,
6-Jan-2018.)
|
|
|
Theorem | mnfle 8867 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltnsym 8868 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltnsym2 8869 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
|
|
Theorem | xrlttr 8870 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltso 8871 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
|
|
Theorem | xrlttri3 8872 |
Extended real version of lttri3 7191. (Contributed by NM, 9-Feb-2006.)
|
|
|
Theorem | xrltle 8873 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrleid 8874 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
|
|
Theorem | xrletri3 8875 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
|
|
Theorem | xrlelttr 8876 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrltletr 8877 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrletr 8878 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
|
|
Theorem | xrlttrd 8879 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrlelttrd 8880 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltletrd 8881 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrletrd 8882 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltne 8883 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
|
|
Theorem | nltpnft 8884 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
|
|
Theorem | ngtmnft 8885 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | xrrebnd 8886 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | xrre 8887 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
|
|
Theorem | xrre2 8888 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
|
|
Theorem | xrre3 8889 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
|
|
Theorem | ge0gtmnf 8890 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ge0nemnf 8891 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrrege0 8892 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | z2ge 8893* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
|
|
Theorem | xnegeq 8894 |
Equality of two extended numbers with in front of them.
(Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnegpnf 8895 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.)
|
|
|
Theorem | xnegmnf 8896 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexneg 8897 |
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xneg0 8898 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xnegcl 8899 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnegneg 8900 |
Extended real version of negneg 7358. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|