![]() |
Metamath
Proof Explorer Theorem List (p. 97 of 406) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-26571) |
![]() (26572-28094) |
![]() (28095-40593) |
Type | Label | Description |
---|---|---|
Statement | ||
Axiom | ax-mulcl 9601 | Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by theorem axmulcl 9577. Proofs should normally use mulcl 9623 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-mulrcl 9602 | Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by theorem axmulrcl 9578. Proofs should normally use remulcl 9624 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-mulcom 9603 | Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by theorem axmulcom 9579. Proofs should normally use mulcom 9625 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-addass 9604 | Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by theorem axaddass 9580. Proofs should normally use addass 9626 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-mulass 9605 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by theorem axmulass 9581. Proofs should normally use mulass 9627 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-distr 9606 | Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9582. Proofs should normally use adddi 9628 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-i2m1 9607 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by theorem axi2m1 9583. (Contributed by NM, 29-Jan-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-1ne0 9608 | 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 9584. (Contributed by NM, 29-Jan-1995.) |
![]() ![]() ![]() ![]() | ||
Axiom | ax-1rid 9609 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-rnegex 9610* | Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 9586. (Contributed by Eric Schmidt, 21-May-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-rrecex 9611* | Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by theorem axrrecex 9587. (Contributed by Eric Schmidt, 11-Apr-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-cnre 9612* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, justified by theorem axcnre 9588. For naming consistency, use cnre 9639 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-pre-lttri 9613 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by theorem axpre-lttri 9589. Note: The more general version for extended reals is axlttri 9705. Normally new proofs would use xrlttri 11438. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-pre-lttrn 9614 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn 9590. Note: The more general version for extended reals is axlttrn 9706. Normally new proofs would use lttr 9710. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-pre-ltadd 9615 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd 9591. Normally new proofs would use axltadd 9707. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-pre-mulgt0 9616 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by theorem axpre-mulgt0 9592. Normally new proofs would use axmulgt0 9708. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-pre-sup 9617* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by theorem axpre-sup 9593. Note: Normally new proofs would use axsup 9709. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-addf 9618 |
Addition is an operation on the complex numbers. This deprecated axiom is
provided for historical compatibility but is not a bona fide axiom for
complex numbers (independent of set theory) since it cannot be interpreted
as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific addcl 9621 should be used. Note that uses of ax-addf 9618 can
be eliminated by using the defined operation
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() This axiom is justified by theorem axaddf 9569. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-mulf 9619 |
Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ax-mulcl 9601 should be used. Note that uses of ax-mulf 9619
can be eliminated by using the defined operation
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() This axiom is justified by theorem axmulf 9570. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cnex 9620 | Alias for ax-cnex 9595. See also cnexALT 11298. (Contributed by Mario Carneiro, 17-Nov-2014.) |
![]() ![]() ![]() ![]() | ||
Theorem | addcl 9621 | Alias for ax-addcl 9599, for naming consistency with addcli 9647. Use this theorem instead of ax-addcl 9599 or axaddcl 9575. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | readdcl 9622 | Alias for ax-addrcl 9600, for naming consistency with readdcli 9656. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcl 9623 | Alias for ax-mulcl 9601, for naming consistency with mulcli 9648. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | remulcl 9624 | Alias for ax-mulrcl 9602, for naming consistency with remulcli 9657. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcom 9625 | Alias for ax-mulcom 9603, for naming consistency with mulcomi 9649. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addass 9626 | Alias for ax-addass 9604, for naming consistency with addassi 9651. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulass 9627 | Alias for ax-mulass 9605, for naming consistency with mulassi 9652. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddi 9628 | Alias for ax-distr 9606, for naming consistency with adddii 9653. (Contributed by NM, 10-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | recn 9629 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | reex 9630 | The real numbers form a set. See also reexALT 11296. (Contributed by Mario Carneiro, 17-Nov-2014.) |
![]() ![]() ![]() ![]() | ||
Theorem | reelprrecn 9631 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cnelprrecn 9632 | Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elimne0 9633 |
Hypothesis for weak deduction theorem to eliminate ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddir 9634 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0cn 9635 | 0 is a complex number. See also 0cnALT 9864. (Contributed by NM, 19-Feb-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | 0cnd 9636 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | c0ex 9637 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
![]() ![]() ![]() ![]() | ||
Theorem | 1ex 9638 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
![]() ![]() ![]() ![]() | ||
Theorem | cnre 9639* | Alias for ax-cnre 9612, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid1 9640 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid2 9641 | Identity law for multiplication. Note: see mulid1 9640 for commuted version. (Contributed by NM, 8-Oct-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1re 9642 |
![]() ![]() |
![]() ![]() ![]() ![]() | ||
Theorem | 0re 9643 |
![]() |
![]() ![]() ![]() ![]() | ||
Theorem | 0red 9644 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid1i 9645 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid2i 9646 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addcli 9647 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcli 9648 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcomi 9649 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcomli 9650 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addassi 9651 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulassi 9652 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddii 9653 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddiri 9654 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | recni 9655 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | readdcli 9656 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | remulcli 9657 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1red 9658 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1cnd 9659 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid1d 9660 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulid2d 9661 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addcld 9662 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcld 9663 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulcomd 9664 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | addassd 9665 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mulassd 9666 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddid 9667 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | adddird 9668 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | recnd 9669 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | readdcld 9670 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | remulcld 9671 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | cpnf 9672 | Plus infinity. |
![]() ![]() | ||
Syntax | cmnf 9673 | Minus infinity. |
![]() ![]() | ||
Syntax | cxr 9674 | The set of extended reals (includes plus and minus infinity). |
![]() ![]() | ||
Syntax | clt 9675 | 'Less than' predicate (extended to include the extended reals). |
![]() ![]() | ||
Syntax | cle 9676 | Extend wff notation to include the 'less than or equal to' relation. |
![]() ![]() | ||
Definition | df-pnf 9677 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]()
A simpler possibility is to define |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Definition | df-mnf 9678 |
Define minus infinity as the power set of plus infinity. Note that the
definition is arbitrary, requiring only that ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() | ||
Definition | df-xr 9679 | 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 9680* |
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 9681 | Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9720 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pnfnre 9682 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | mnfnre 9683 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | ressxr 9684 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() ![]() | ||
Theorem | rexpssxrxp 9685 | 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 9686 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0xr 9687 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
![]() ![]() ![]() ![]() | ||
Theorem | renepnf 9688 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renemnf 9689 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rexrd 9690 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renepnfd 9691 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renemnfd 9692 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rexri 9693 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | renfdisj 9694 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltrelxr 9695 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ltrel 9696 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() | ||
Theorem | lerelxr 9697 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lerel 9698 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() | ||
Theorem | xrlenlt 9699 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | xrlenltd 9700 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |