![]() |
Metamath
Proof Explorer Theorem List (p. 113 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mulass 11201 | Alias for ax-mulass 11179, for naming consistency with mulassi 11230. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) | ||
Theorem | adddi 11202 | Alias for ax-distr 11180, for naming consistency with adddii 11231. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ))) | ||
Theorem | recn 11203 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
β’ (π΄ β β β π΄ β β) | ||
Theorem | reex 11204 | The real numbers form a set. See also reexALT 12973. (Contributed by Mario Carneiro, 17-Nov-2014.) |
β’ β β V | ||
Theorem | reelprrecn 11205 | Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ β β {β, β} | ||
Theorem | cnelprrecn 11206 | Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ β β {β, β} | ||
Theorem | mpomulf 11207* | Multiplication is an operation on complex numbers. Version of ax-mulf 11193 using maps-to notation, proved from the axioms of set theory and ax-mulcl 11175. (Contributed by GG, 16-Mar-2025.) |
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)):(β Γ β)βΆβ | ||
Theorem | ovmul 11208* | Multiplication of complex numbers produces the same value as multiplication expressed in maps-to notation of the same complex numbers. (Contributed by GG, 16-Mar-2025.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π΅) = (π΄ Β· π΅)) | ||
Theorem | elimne0 11209 | Hypothesis for weak deduction theorem to eliminate π΄ β 0. (Contributed by NM, 15-May-1999.) |
β’ if(π΄ β 0, π΄, 1) β 0 | ||
Theorem | adddir 11210 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β· πΆ) = ((π΄ Β· πΆ) + (π΅ Β· πΆ))) | ||
Theorem | 0cn 11211 | Zero is a complex number. See also 0cnALT 11453. (Contributed by NM, 19-Feb-2005.) |
β’ 0 β β | ||
Theorem | 0cnd 11212 | Zero is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (π β 0 β β) | ||
Theorem | c0ex 11213 | Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.) |
β’ 0 β V | ||
Theorem | 1cnd 11214 | One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ (π β 1 β β) | ||
Theorem | 1ex 11215 | One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.) |
β’ 1 β V | ||
Theorem | cnre 11216* | Alias for ax-cnre 11186, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
β’ (π΄ β β β βπ₯ β β βπ¦ β β π΄ = (π₯ + (i Β· π¦))) | ||
Theorem | mulrid 11217 | The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
β’ (π΄ β β β (π΄ Β· 1) = π΄) | ||
Theorem | mullid 11218 | Identity law for multiplication. See mulrid 11217 for commuted version. (Contributed by NM, 8-Oct-1999.) |
β’ (π΄ β β β (1 Β· π΄) = π΄) | ||
Theorem | 1re 11219 | The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11171, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
β’ 1 β β | ||
Theorem | 1red 11220 | The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ (π β 1 β β) | ||
Theorem | 0re 11221 | The number 0 is real. Remark: the first step could also be ax-icn 11172. See also 0reALT 11562. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.) |
β’ 0 β β | ||
Theorem | 0red 11222 | The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ (π β 0 β β) | ||
Theorem | mulridi 11223 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
β’ π΄ β β β β’ (π΄ Β· 1) = π΄ | ||
Theorem | mullidi 11224 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
β’ π΄ β β β β’ (1 Β· π΄) = π΄ | ||
Theorem | addcli 11225 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) β β | ||
Theorem | mulcli 11226 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) β β | ||
Theorem | mulcomi 11227 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) = (π΅ Β· π΄) | ||
Theorem | mulcomli 11228 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ (π΄ Β· π΅) = πΆ β β’ (π΅ Β· π΄) = πΆ | ||
Theorem | addassi 11229 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ)) | ||
Theorem | mulassi 11230 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ)) | ||
Theorem | adddii 11231 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ)) | ||
Theorem | adddiri 11232 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) Β· πΆ) = ((π΄ Β· πΆ) + (π΅ Β· πΆ)) | ||
Theorem | recni 11233 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
β’ π΄ β β β β’ π΄ β β | ||
Theorem | readdcli 11234 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) β β | ||
Theorem | remulcli 11235 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) β β | ||
Theorem | mulridd 11236 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (π΄ Β· 1) = π΄) | ||
Theorem | mullidd 11237 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (1 Β· π΄) = π΄) | ||
Theorem | addcld 11238 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ + π΅) β β) | ||
Theorem | mulcld 11239 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· π΅) β β) | ||
Theorem | mulcomd 11240 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Theorem | addassd 11241 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) | ||
Theorem | mulassd 11242 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) | ||
Theorem | adddid 11243 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ))) | ||
Theorem | adddird 11244 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅) Β· πΆ) = ((π΄ Β· πΆ) + (π΅ Β· πΆ))) | ||
Theorem | adddirp1d 11245 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((π΄ + 1) Β· π΅) = ((π΄ Β· π΅) + π΅)) | ||
Theorem | joinlmuladdmuld 11246 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β ((π΄ Β· π΅) + (πΆ Β· π΅)) = π·) β β’ (π β ((π΄ + πΆ) Β· π΅) = π·) | ||
Theorem | recnd 11247 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
β’ (π β π΄ β β) β β’ (π β π΄ β β) | ||
Theorem | readdcld 11248 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ + π΅) β β) | ||
Theorem | remulcld 11249 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· π΅) β β) | ||
Syntax | cpnf 11250 | Plus infinity. |
class +β | ||
Syntax | cmnf 11251 | Minus infinity. |
class -β | ||
Syntax | cxr 11252 | The set of extended reals (includes plus and minus infinity). |
class β* | ||
Syntax | clt 11253 | 'Less than' predicate (extended to include the extended reals). |
class < | ||
Syntax | cle 11254 | Extend wff notation to include the 'less than or equal to' relation. |
class β€ | ||
Definition | df-pnf 11255 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that +β be a set not in β and different from -β
(df-mnf 11256). We use π« βͺ β to make it independent of the
construction of β, and Cantor's Theorem will
show that it is
different from any member of β and therefore
β. See pnfnre 11260,
mnfnre 11262, and pnfnemnf 11274.
A simpler possibility is to define +β as β and -β as {β}, but that approach requires the Axiom of Regularity to show that +β and -β are different from each other and from all members of β. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
β’ +β = π« βͺ β | ||
Definition | df-mnf 11256 | Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -β be a set not in β and different from +β (see mnfnre 11262 and pnfnemnf 11274). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
β’ -β = π« +β | ||
Definition | df-xr 11257 | 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 11258* | 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, <β is primitive and not necessarily a relation on β. (Contributed by NM, 13-Oct-2005.) |
β’ < = ({β¨π₯, π¦β© β£ (π₯ β β β§ π¦ β β β§ π₯ <β π¦)} βͺ (((β βͺ {-β}) Γ {+β}) βͺ ({-β} Γ β))) | ||
Definition | df-le 11259 | Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 11305 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.) |
β’ β€ = ((β* Γ β*) β β‘ < ) | ||
Theorem | pnfnre 11260 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
β’ +β β β | ||
Theorem | pnfnre2 11261 | Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ Β¬ +β β β | ||
Theorem | mnfnre 11262 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
β’ -β β β | ||
Theorem | ressxr 11263 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
β’ β β β* | ||
Theorem | rexpssxrxp 11264 | The Cartesian product of standard reals are a subset of the Cartesian product of extended reals. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (β Γ β) β (β* Γ β*) | ||
Theorem | rexr 11265 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
β’ (π΄ β β β π΄ β β*) | ||
Theorem | 0xr 11266 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
β’ 0 β β* | ||
Theorem | renepnf 11267 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
β’ (π΄ β β β π΄ β +β) | ||
Theorem | renemnf 11268 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
β’ (π΄ β β β π΄ β -β) | ||
Theorem | rexrd 11269 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β β*) | ||
Theorem | renepnfd 11270 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β +β) | ||
Theorem | renemnfd 11271 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β -β) | ||
Theorem | pnfex 11272 | Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.) |
β’ +β β V | ||
Theorem | pnfxr 11273 | Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) |
β’ +β β β* | ||
Theorem | pnfnemnf 11274 | Plus and minus infinity are different elements of β*. (Contributed by NM, 14-Oct-2005.) |
β’ +β β -β | ||
Theorem | mnfnepnf 11275 | Minus and plus infinity are different. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -β β +β | ||
Theorem | mnfxr 11276 | 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 11277 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
β’ π΄ β β β β’ π΄ β β* | ||
Theorem | 1xr 11278 | 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ 1 β β* | ||
Theorem | renfdisj 11279 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
β’ (β β© {+β, -β}) = β | ||
Theorem | ltrelxr 11280 | "Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
β’ < β (β* Γ β*) | ||
Theorem | ltrel 11281 | "Less than" is a relation. (Contributed by NM, 14-Oct-2005.) |
β’ Rel < | ||
Theorem | lerelxr 11282 | "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
β’ β€ β (β* Γ β*) | ||
Theorem | lerel 11283 | "Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ Rel β€ | ||
Theorem | xrlenlt 11284 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ β€ π΅ β Β¬ π΅ < π΄)) | ||
Theorem | xrlenltd 11285 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ β€ π΅ β Β¬ π΅ < π΄)) | ||
Theorem | xrltnle 11286 | "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ < π΅ β Β¬ π΅ β€ π΄)) | ||
Theorem | xrnltled 11287 | "Not less than" implies "less than or equal to". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β Β¬ π΅ < π΄) β β’ (π β π΄ β€ π΅) | ||
Theorem | ssxr 11288 | The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
β’ (π΄ β β* β (π΄ β β β¨ +β β π΄ β¨ -β β π΄)) | ||
Theorem | ltxrlt 11289 | The standard less-than <β and the extended real less-than < are identical when restricted to the non-extended reals β. (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β π΄ <β π΅)) | ||
Theorem | axlttri 11290 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-lttri 11187 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β Β¬ (π΄ = π΅ β¨ π΅ < π΄))) | ||
Theorem | axlttrn 11291 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 11188 with ordering on the extended reals. New proofs should use lttr 11295 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ < π΅ β§ π΅ < πΆ) β π΄ < πΆ)) | ||
Theorem | axltadd 11292 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd 11189 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ < π΅ β (πΆ + π΄) < (πΆ + π΅))) | ||
Theorem | axmulgt0 11293 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 11190 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β) β ((0 < π΄ β§ 0 < π΅) β 0 < (π΄ Β· π΅))) | ||
Theorem | axsup 11294* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup 11191 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ < π₯) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) | ||
Theorem | lttr 11295 | Alias for axlttrn 11291, for naming consistency with lttri 11345. New proofs should generally use this instead of ax-pre-lttrn 11188. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ < π΅ β§ π΅ < πΆ) β π΄ < πΆ)) | ||
Theorem | mulgt0 11296 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
β’ (((π΄ β β β§ 0 < π΄) β§ (π΅ β β β§ 0 < π΅)) β 0 < (π΄ Β· π΅)) | ||
Theorem | lenlt 11297 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β€ π΅ β Β¬ π΅ < π΄)) | ||
Theorem | ltnle 11298 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β Β¬ π΅ β€ π΄)) | ||
Theorem | ltso 11299 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
β’ < Or β | ||
Theorem | gtso 11300 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
β’ β‘ < Or β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |