![]() |
Intuitionistic Logic Explorer Theorem List (p. 81 of 153) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1red 8001 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1cnd 8002 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulridd 8003 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mullidd 8004 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid2d 8005 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addcld 8006 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcld 8007 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcomd 8008 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addassd 8009 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulassd 8010 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddid 8011 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddird 8012 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddirp1d 8013 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | joinlmuladdmuld 8014 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | recnd 8015 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | readdcld 8016 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | remulcld 8017 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | cpnf 8018 | Plus infinity. |
![]() ![]() | ||
Syntax | cmnf 8019 | Minus infinity. |
![]() ![]() | ||
Syntax | cxr 8020 | The set of extended reals (includes plus and minus infinity). |
![]() ![]() | ||
Syntax | clt 8021 | 'Less than' predicate (extended to include the extended reals). |
![]() ![]() | ||
Syntax | cle 8022 | Extend wff notation to include the 'less than or equal to' relation. |
![]() ![]() | ||
Definition | df-pnf 8023 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]()
A simpler possibility is to define |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-mnf 8024 |
Define minus infinity as the power set of plus infinity. Note that the
definition is arbitrary, requiring only that ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() | ||
Definition | df-xr 8025 | Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-ltxr 8026* |
Define 'less than' on the set of extended reals. Definition 12-3.1 of
[Gleason] p. 173. Note that in our
postulates for complex numbers,
![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-le 8027 | Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pnfnre 8028 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | mnfnre 8029 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | ressxr 8030 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | rexpssxrxp 8031 | The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rexr 8032 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0xr 8033 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
![]() ![]() ![]() ![]() | ||
Theorem | renepnf 8034 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renemnf 8035 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rexrd 8036 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renepnfd 8037 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renemnfd 8038 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pnfxr 8039 | 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 8040 | Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() | ||
Theorem | pnfnemnf 8041 |
Plus and minus infinity are different elements of ![]() |
![]() ![]() ![]() ![]() | ||
Theorem | mnfnepnf 8042 | Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() | ||
Theorem | mnfxr 8043 | 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 | rexri 8044 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1xr 8045 |
![]() |
![]() ![]() ![]() ![]() | ||
Theorem | renfdisj 8046 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltrelxr 8047 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltrel 8048 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() | ||
Theorem | lerelxr 8049 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lerel 8050 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() | ||
Theorem | xrlenlt 8051 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltxrlt 8052 |
The standard less-than ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axltirr 8053 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7952 with ordering on the extended reals. New proofs should use ltnr 8063 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axltwlin 8054 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7953 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axlttrn 8055 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7954 with ordering on the extended reals. New proofs should use lttr 8060 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axltadd 8056 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7956 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axapti 8057 | Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7955 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axmulgt0 8058 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7957 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axsuploc 8059* | 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 7961 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lttr 8060 | Alias for axlttrn 8055, for naming consistency with lttri 8091. New proofs should generally use this instead of ax-pre-lttrn 7954. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulgt0 8061 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lenlt 8062 | '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 8063 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltso 8064 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
![]() ![]() ![]() ![]() | ||
Theorem | gtso 8065 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | lttri3 8066 | Tightness of real apartness. (Contributed by NM, 5-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | letri3 8067 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltleletr 8068 |
Transitive law, weaker form of ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | letr 8069 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | leid 8070 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltne 8071 | 'Less than' implies not equal. See also ltap 8619 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltnsym 8072 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eqlelt 8073 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltle 8074 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lelttr 8075 | Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltletr 8076 | Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltnsym2 8077 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eqle 8078 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltnri 8079 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eqlei 8080 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eqlei2 8081 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | gtneii 8082 | 'Less than' implies not equal. See also gtapii 8620 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltneii 8083 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lttri3i 8084 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | letri3i 8085 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltnsymi 8086 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lenlti 8087 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltlei 8088 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltleii 8089 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltnei 8090 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lttri 8091 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lelttri 8092 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltletri 8093 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | letri 8094 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | le2tri3i 8095 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulgt0i 8096 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulgt0ii 8097 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltnrd 8098 | 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | gtned 8099 | 'Less than' implies not equal. See also gtapd 8623 which is the same but for apartness. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltned 8100 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |