Theorem List for Intuitionistic Logic Explorer - 7801-7900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | axlttrn 7801 |
Ordering on reals is transitive. Axiom for real and complex numbers,
derived from set theory. This restates ax-pre-lttrn 7702 with ordering on
the extended reals. New proofs should use lttr 7806
instead for naming
consistency. (New usage is discouraged.) (Contributed by NM,
13-Oct-2005.)
|
|
|
Theorem | axltadd 7802 |
Ordering property of addition on reals. Axiom for real and complex
numbers, derived from set theory. (This restates ax-pre-ltadd 7704 with
ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|
|
|
Theorem | axapti 7803 |
Apartness of reals is tight. Axiom for real and complex numbers, derived
from set theory. (This restates ax-pre-apti 7703 with ordering on the
extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
|
|
|
Theorem | axmulgt0 7804 |
The product of two positive reals is positive. Axiom for real and complex
numbers, derived from set theory. (This restates ax-pre-mulgt0 7705 with
ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|
|
|
Theorem | axsuploc 7805* |
An inhabited, bounded-above, located set of reals has a supremum. Axiom
for real and complex numbers, derived from ZF set theory. (This
restates ax-pre-suploc 7709 with ordering on the extended reals.)
(Contributed by Jim Kingdon, 30-Jan-2024.)
|
|
|
4.2.4 Ordering on reals
|
|
Theorem | lttr 7806 |
Alias for axlttrn 7801, for naming consistency with lttri 7836. New proofs
should generally use this instead of ax-pre-lttrn 7702. (Contributed by NM,
10-Mar-2008.)
|
|
|
Theorem | mulgt0 7807 |
The product of two positive numbers is positive. (Contributed by NM,
10-Mar-2008.)
|
|
|
Theorem | lenlt 7808 |
'Less than or equal to' expressed in terms of 'less than'. Part of
definition 11.2.7(vi) of [HoTT], p.
(varies). (Contributed by NM,
13-May-1999.)
|
|
|
Theorem | ltnr 7809 |
'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|
|
|
Theorem | ltso 7810 |
'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|
|
|
Theorem | gtso 7811 |
'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|
|
|
Theorem | lttri3 7812 |
Tightness of real apartness. (Contributed by NM, 5-May-1999.)
|
|
|
Theorem | letri3 7813 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
|
|
Theorem | ltleletr 7814 |
Transitive law, weaker form of
.
(Contributed by AV, 14-Oct-2018.)
|
|
|
Theorem | letr 7815 |
Transitive law. (Contributed by NM, 12-Nov-1999.)
|
|
|
Theorem | leid 7816 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | ltne 7817 |
'Less than' implies not equal. See also ltap 8363
which is the same but for
apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro,
16-Sep-2015.)
|
|
|
Theorem | ltnsym 7818 |
'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|
|
|
Theorem | ltle 7819 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
25-Aug-1999.)
|
|
|
Theorem | lelttr 7820 |
Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 23-May-1999.)
|
|
|
Theorem | ltletr 7821 |
Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 25-Aug-1999.)
|
|
|
Theorem | ltnsym2 7822 |
'Less than' is antisymmetric and irreflexive. (Contributed by NM,
13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | eqle 7823 |
Equality implies 'less than or equal to'. (Contributed by NM,
4-Apr-2005.)
|
|
|
Theorem | ltnri 7824 |
'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|
|
|
Theorem | eqlei 7825 |
Equality implies 'less than or equal to'. (Contributed by NM,
23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|
|
|
Theorem | eqlei2 7826 |
Equality implies 'less than or equal to'. (Contributed by Alexander van
der Vekens, 20-Mar-2018.)
|
|
|
Theorem | gtneii 7827 |
'Less than' implies not equal. See also gtapii 8364 which is the same
for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|
|
|
Theorem | ltneii 7828 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
16-Sep-2015.)
|
|
|
Theorem | lttri3i 7829 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
|
|
Theorem | letri3i 7830 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
|
|
Theorem | ltnsymi 7831 |
'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|
|
|
Theorem | lenlti 7832 |
'Less than or equal to' in terms of 'less than'. (Contributed by NM,
24-May-1999.)
|
|
|
Theorem | ltlei 7833 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | ltleii 7834 |
'Less than' implies 'less than or equal to' (inference). (Contributed
by NM, 22-Aug-1999.)
|
|
|
Theorem | ltnei 7835 |
'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|
|
|
Theorem | lttri 7836 |
'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
|
|
Theorem | lelttri 7837 |
'Less than or equal to', 'less than' transitive law. (Contributed by
NM, 14-May-1999.)
|
|
|
Theorem | ltletri 7838 |
'Less than', 'less than or equal to' transitive law. (Contributed by
NM, 14-May-1999.)
|
|
|
Theorem | letri 7839 |
'Less than or equal to' is transitive. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | le2tri3i 7840 |
Extended trichotomy law for 'less than or equal to'. (Contributed by
NM, 14-Aug-2000.)
|
|
|
Theorem | mulgt0i 7841 |
The product of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | mulgt0ii 7842 |
The product of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | ltnrd 7843 |
'Less than' is irreflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | gtned 7844 |
'Less than' implies not equal. See also gtapd 8367 which is the same but
for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltned 7845 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | lttri3d 7846 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | letri3d 7847 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | lenltd 7848 |
'Less than or equal to' in terms of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | ltled 7849 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | ltnsymd 7850 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | nltled 7851 |
'Not less than ' implies 'less than or equal to'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | lensymd 7852 |
'Less than or equal to' implies 'not less than'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | mulgt0d 7853 |
The product of two positive numbers is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | letrd 7854 |
Transitive law deduction for 'less than or equal to'. (Contributed by
NM, 20-May-2005.)
|
|
|
Theorem | lelttrd 7855 |
Transitive law deduction for 'less than or equal to', 'less than'.
(Contributed by NM, 8-Jan-2006.)
|
|
|
Theorem | lttrd 7856 |
Transitive law deduction for 'less than'. (Contributed by NM,
9-Jan-2006.)
|
|
|
Theorem | 0lt1 7857 |
0 is less than 1. Theorem I.21 of [Apostol] p.
20. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 17-Jan-1997.)
|
|
|
Theorem | ltntri 7858 |
Negative trichotomy property for real numbers. It is well known that we
cannot prove real number trichotomy,
. Does
that mean there is a pair of real numbers where none of those hold (that
is, where we can refute each of those three relationships)? Actually, no,
as shown here. This is another example of distinguishing between being
unable to prove something, or being able to refute it. (Contributed by
Jim Kingdon, 13-Aug-2023.)
|
|
|
4.2.5 Initial properties of the complex
numbers
|
|
Theorem | mul12 7859 |
Commutative/associative law for multiplication. (Contributed by NM,
30-Apr-2005.)
|
|
|
Theorem | mul32 7860 |
Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|
|
|
Theorem | mul31 7861 |
Commutative/associative law. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | mul4 7862 |
Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|
|
|
Theorem | muladd11 7863 |
A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | 1p1times 7864 |
Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | peano2cn 7865 |
A theorem for complex numbers analogous the second Peano postulate
peano2 4479. (Contributed by NM, 17-Aug-2005.)
|
|
|
Theorem | peano2re 7866 |
A theorem for reals analogous the second Peano postulate peano2 4479.
(Contributed by NM, 5-Jul-2005.)
|
|
|
Theorem | addcom 7867 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
|
|
Theorem | addid1 7868 |
is an additive identity.
(Contributed by Jim Kingdon,
16-Jan-2020.)
|
|
|
Theorem | addid2 7869 |
is a left identity for
addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | readdcan 7870 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
|
|
Theorem | 00id 7871 |
is its own additive
identity. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | addid1i 7872 |
is an additive identity.
(Contributed by NM, 23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | addid2i 7873 |
is a left identity for
addition. (Contributed by NM,
3-Jan-2013.)
|
|
|
Theorem | addcomi 7874 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | addcomli 7875 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
|
|
Theorem | mul12i 7876 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew
Salmon, 19-Nov-2011.)
|
|
|
Theorem | mul32i 7877 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
|
|
Theorem | mul4i 7878 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
|
|
Theorem | addid1d 7879 |
is an additive identity.
(Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addid2d 7880 |
is a left identity for
addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addcomd 7881 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul12d 7882 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul32d 7883 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul31d 7884 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mul4d 7885 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | muladd11r 7886 |
A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|
|
|
Theorem | comraddd 7887 |
Commute RHS addition, in deduction form. (Contributed by David A.
Wheeler, 11-Oct-2018.)
|
|
|
4.3 Real and complex numbers - basic
operations
|
|
4.3.1 Addition
|
|
Theorem | add12 7888 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
|
|
Theorem | add32 7889 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
|
|
Theorem | add32r 7890 |
Commutative/associative law that swaps the last two terms in a triple sum,
rearranging the parentheses. (Contributed by Paul Chapman,
18-May-2007.)
|
|
|
Theorem | add4 7891 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | add42 7892 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
|
|
Theorem | add12i 7893 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | add32i 7894 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | add4i 7895 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
|
|
Theorem | add42i 7896 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | add12d 7897 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | add32d 7898 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | add4d 7899 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | add42d 7900 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
|