![]() |
Intuitionistic Logic Explorer Theorem List (p. 80 of 153) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | axpre-ltirr 7901 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 7943. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
β’ (π΄ β β β Β¬ π΄ <β π΄) | ||
Theorem | axpre-ltwlin 7902 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 7944. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ <β π΅ β (π΄ <β πΆ β¨ πΆ <β π΅))) | ||
Theorem | axpre-lttrn 7903 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 7945. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ <β π΅ β§ π΅ <β πΆ) β π΄ <β πΆ)) | ||
Theorem | axpre-apti 7904 |
Apartness of reals is tight. Axiom for real and complex numbers,
derived from set theory. This construction-dependent theorem should not
be referenced directly; instead, use ax-pre-apti 7946.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ Β¬ (π΄ <β π΅ β¨ π΅ <β π΄)) β π΄ = π΅) | ||
Theorem | axpre-ltadd 7905 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 7947. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ <β π΅ β (πΆ + π΄) <β (πΆ + π΅))) | ||
Theorem | axpre-mulgt0 7906 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 7948. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((0 <β π΄ β§ 0 <β π΅) β 0 <β (π΄ Β· π΅))) | ||
Theorem | axpre-mulext 7907 |
Strong extensionality of multiplication (expressed in terms of
<β). Axiom for real and
complex numbers, derived from set theory.
This construction-dependent theorem should not be referenced directly;
instead, use ax-pre-mulext 7949.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· πΆ) <β (π΅ Β· πΆ) β (π΄ <β π΅ β¨ π΅ <β π΄))) | ||
Theorem | rereceu 7908* | The reciprocal from axprecex 7899 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
β’ ((π΄ β β β§ 0 <β π΄) β β!π₯ β β (π΄ Β· π₯) = 1) | ||
Theorem | recriota 7909* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
β’ (π β N β (β©π β β (β¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ© Β· π) = 1) = β¨[β¨(β¨{π β£ π <Q (*Qβ[β¨π, 1oβ©] ~Q )}, {π’ β£ (*Qβ[β¨π, 1oβ©] ~Q ) <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) | ||
Theorem | axarch 7910* |
Archimedean axiom. The Archimedean property is more naturally stated
once we have defined β. Unless we find
another way to state it,
we'll just use the right hand side of dfnn2 8941 in stating what we mean by
"natural number" in the context of this axiom.
This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7950. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
β’ (π΄ β β β βπ β β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)}π΄ <β π) | ||
Theorem | peano5nnnn 7911* | Peano's inductive postulate. This is a counterpart to peano5nni 8942 designed for real number axioms which involve natural numbers (notably, axcaucvg 7919). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} β β’ ((1 β π΄ β§ βπ§ β π΄ (π§ + 1) β π΄) β π β π΄) | ||
Theorem | nnindnn 7912* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8955 designed for real number axioms which involve natural numbers (notably, axcaucvg 7919). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π§ = 1 β (π β π)) & β’ (π§ = π β (π β π)) & β’ (π§ = (π + 1) β (π β π)) & β’ (π§ = π΄ β (π β π)) & β’ π & β’ (π β π β (π β π)) β β’ (π΄ β π β π) | ||
Theorem | nntopi 7913* | Mapping from β to N. (Contributed by Jim Kingdon, 13-Jul-2021.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} β β’ (π΄ β π β βπ§ β N β¨[β¨(β¨{π β£ π <Q [β¨π§, 1oβ©] ~Q }, {π’ β£ [β¨π§, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ© = π΄) | ||
Theorem | axcaucvglemcl 7914* | Lemma for axcaucvg 7919. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) β β’ ((π β§ π½ β N) β (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©] ~Q }, {π’ β£ [β¨π½, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©) β R) | ||
Theorem | axcaucvglemf 7915* | Lemma for axcaucvg 7919. Mapping to N and R yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) & β’ πΊ = (π β N β¦ (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©)) β β’ (π β πΊ:NβΆR) | ||
Theorem | axcaucvglemval 7916* | Lemma for axcaucvg 7919. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) & β’ πΊ = (π β N β¦ (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©)) β β’ ((π β§ π½ β N) β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©] ~Q }, {π’ β£ [β¨π½, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨(πΊβπ½), 0Rβ©) | ||
Theorem | axcaucvglemcau 7917* | Lemma for axcaucvg 7919. The result of mapping to N and R satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) & β’ πΊ = (π β N β¦ (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©)) β β’ (π β βπ β N βπ β N (π <N π β ((πΊβπ) <R ((πΊβπ) +R [β¨(β¨{π β£ π <Q (*Qβ[β¨π, 1oβ©] ~Q )}, {π’ β£ (*Qβ[β¨π, 1oβ©] ~Q ) <Q π’}β© +P 1P), 1Pβ©] ~R ) β§ (πΊβπ) <R ((πΊβπ) +R [β¨(β¨{π β£ π <Q (*Qβ[β¨π, 1oβ©] ~Q )}, {π’ β£ (*Qβ[β¨π, 1oβ©] ~Q ) <Q π’}β© +P 1P), 1Pβ©] ~R )))) | ||
Theorem | axcaucvglemres 7918* | Lemma for axcaucvg 7919. Mapping the limit from N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) & β’ πΊ = (π β N β¦ (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©)) β β’ (π β βπ¦ β β βπ₯ β β (0 <β π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))))) | ||
Theorem | axcaucvg 7919* |
Real number completeness axiom. A Cauchy sequence with a modulus of
convergence converges. This is basically Corollary 11.2.13 of [HoTT],
p. (varies). The HoTT book theorem has a modulus of convergence
(that is, a rate of convergence) specified by (11.2.9) in HoTT whereas
this theorem fixes the rate of convergence to say that all terms after
the nth term must be within 1 / π of the nth term (it should later
be able to prove versions of this theorem with a different fixed rate
or a modulus of convergence supplied as a hypothesis).
Because we are stating this axiom before we have introduced notations for β or division, we use π for the natural numbers and express a reciprocal in terms of β©. This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 7951. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) β β’ (π β βπ¦ β β βπ₯ β β (0 <β π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))))) | ||
Theorem | axpre-suploclemres 7920* | Lemma for axpre-suploc 7921. The result. The proof just needs to define π΅ as basically the same set as π΄ (but expressed as a subset of R rather than a subset of β), and apply suplocsr 7828. (Contributed by Jim Kingdon, 24-Jan-2024.) |
β’ (π β π΄ β β) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ <β π₯) & β’ (π β βπ₯ β β βπ¦ β β (π₯ <β π¦ β (βπ§ β π΄ π₯ <β π§ β¨ βπ§ β π΄ π§ <β π¦))) & β’ π΅ = {π€ β R β£ β¨π€, 0Rβ© β π΄} β β’ (π β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§))) | ||
Theorem | axpre-suploc 7921* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given π₯ < π¦, either there is an element of the set greater than π₯, or π¦ is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7952. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
β’ (((π΄ β β β§ βπ₯ π₯ β π΄) β§ (βπ₯ β β βπ¦ β π΄ π¦ <β π₯ β§ βπ₯ β β βπ¦ β β (π₯ <β π¦ β (βπ§ β π΄ π₯ <β π§ β¨ βπ§ β π΄ π§ <β π¦)))) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§))) | ||
Axiom | ax-cnex 7922 | The complex numbers form a set. Proofs should normally use cnex 7955 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
β’ β β V | ||
Axiom | ax-resscn 7923 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7879. (Contributed by NM, 1-Mar-1995.) |
β’ β β β | ||
Axiom | ax-1cn 7924 | 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7880. (Contributed by NM, 1-Mar-1995.) |
β’ 1 β β | ||
Axiom | ax-1re 7925 | 1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7881. Proofs should use 1re 7976 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
β’ 1 β β | ||
Axiom | ax-icn 7926 | i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7882. (Contributed by NM, 1-Mar-1995.) |
β’ i β β | ||
Axiom | ax-addcl 7927 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 7883. Proofs should normally use addcl 7956 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) | ||
Axiom | ax-addrcl 7928 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 7884. Proofs should normally use readdcl 7957 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) | ||
Axiom | ax-mulcl 7929 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 7885. Proofs should normally use mulcl 7958 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) | ||
Axiom | ax-mulrcl 7930 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 7886. Proofs should normally use remulcl 7959 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) | ||
Axiom | ax-addcom 7931 | Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 7889. Proofs should normally use addcom 8114 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) = (π΅ + π΄)) | ||
Axiom | ax-mulcom 7932 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 7890. Proofs should normally use mulcom 7960 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Axiom | ax-addass 7933 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 7891. Proofs should normally use addass 7961 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) | ||
Axiom | ax-mulass 7934 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 7892. Proofs should normally use mulass 7962 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) | ||
Axiom | ax-distr 7935 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7893. Proofs should normally use adddi 7963 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ))) | ||
Axiom | ax-i2m1 7936 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 7894. (Contributed by NM, 29-Jan-1995.) |
β’ ((i Β· i) + 1) = 0 | ||
Axiom | ax-0lt1 7937 | 0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 7895. Proofs should normally use 0lt1 8104 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
β’ 0 <β 1 | ||
Axiom | ax-1rid 7938 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7896. (Contributed by NM, 29-Jan-1995.) |
β’ (π΄ β β β (π΄ Β· 1) = π΄) | ||
Axiom | ax-0id 7939 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, justified by Theorem ax0id 7897.
Proofs should normally use addrid 8115 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Axiom | ax-rnegex 7940* | Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7898. (Contributed by Eric Schmidt, 21-May-2007.) |
β’ (π΄ β β β βπ₯ β β (π΄ + π₯) = 0) | ||
Axiom | ax-precex 7941* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 7899. (Contributed by Jim Kingdon, 6-Feb-2020.) |
β’ ((π΄ β β β§ 0 <β π΄) β βπ₯ β β (0 <β π₯ β§ (π΄ Β· π₯) = 1)) | ||
Axiom | ax-cnre 7942* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, justified by Theorem axcnre 7900. For naming consistency, use cnre 7973 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
β’ (π΄ β β β βπ₯ β β βπ¦ β β π΄ = (π₯ + (i Β· π¦))) | ||
Axiom | ax-pre-ltirr 7943 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7943. (Contributed by Jim Kingdon, 12-Jan-2020.) |
β’ (π΄ β β β Β¬ π΄ <β π΄) | ||
Axiom | ax-pre-ltwlin 7944 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 7902. (Contributed by Jim Kingdon, 12-Jan-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ <β π΅ β (π΄ <β πΆ β¨ πΆ <β π΅))) | ||
Axiom | ax-pre-lttrn 7945 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 7903. (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ <β π΅ β§ π΅ <β πΆ) β π΄ <β πΆ)) | ||
Axiom | ax-pre-apti 7946 | Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 7904. (Contributed by Jim Kingdon, 29-Jan-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ Β¬ (π΄ <β π΅ β¨ π΅ <β π΄)) β π΄ = π΅) | ||
Axiom | ax-pre-ltadd 7947 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 7905. (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ <β π΅ β (πΆ + π΄) <β (πΆ + π΅))) | ||
Axiom | ax-pre-mulgt0 7948 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 7906. (Contributed by NM, 13-Oct-2005.) |
β’ ((π΄ β β β§ π΅ β β) β ((0 <β π΄ β§ 0 <β π΅) β 0 <β (π΄ Β· π΅))) | ||
Axiom | ax-pre-mulext 7949 |
Strong extensionality of multiplication (expressed in terms of <β).
Axiom for real and complex numbers, justified by Theorem axpre-mulext 7907
(Contributed by Jim Kingdon, 18-Feb-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· πΆ) <β (π΅ Β· πΆ) β (π΄ <β π΅ β¨ π΅ <β π΄))) | ||
Axiom | ax-arch 7950* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by Theorem axarch 7910.
This axiom should not be used directly; instead use arch 9193 (which is the same, but stated in terms of β and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
β’ (π΄ β β β βπ β β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)}π΄ <β π) | ||
Axiom | ax-caucvg 7951* |
Completeness. Axiom for real and complex numbers, justified by Theorem
axcaucvg 7919.
A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / π of the nth term. This axiom should not be used directly; instead use caucvgre 11010 (which is the same, but stated in terms of the β and 1 / π notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) |
β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} & β’ (π β πΉ:πβΆβ) & β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) β β’ (π β βπ¦ β β βπ₯ β β (0 <β π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))))) | ||
Axiom | ax-pre-suploc 7952* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given π₯ < π¦, either there is an element of the set greater than π₯, or π¦ is an upper bound. Although this and ax-caucvg 7951 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7951. (Contributed by Jim Kingdon, 23-Jan-2024.) |
β’ (((π΄ β β β§ βπ₯ π₯ β π΄) β§ (βπ₯ β β βπ¦ β π΄ π¦ <β π₯ β§ βπ₯ β β βπ¦ β β (π₯ <β π¦ β (βπ§ β π΄ π₯ <β π§ β¨ βπ§ β π΄ π§ <β π¦)))) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§))) | ||
Axiom | ax-addf 7953 |
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
https://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 7956 should be used. Note that uses of ax-addf 7953 can
be eliminated by using the defined operation
(π₯
β β, π¦ β
β β¦ (π₯ + π¦)) in place of +, from which
this axiom (with the defined operation in place of +) follows as a
theorem.
This axiom is justified by Theorem axaddf 7887. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
β’ + :(β Γ β)βΆβ | ||
Axiom | ax-mulf 7954 |
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
https://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 7929 should be used. Note that uses of ax-mulf 7954
can be eliminated by using the defined operation
(π₯
β β, π¦ β
β β¦ (π₯ Β·
π¦)) in place of
Β·, from which
this axiom (with the defined operation in place of Β·) follows as a
theorem.
This axiom is justified by Theorem axmulf 7888. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
β’ Β· :(β Γ β)βΆβ | ||
Theorem | cnex 7955 | Alias for ax-cnex 7922. (Contributed by Mario Carneiro, 17-Nov-2014.) |
β’ β β V | ||
Theorem | addcl 7956 | Alias for ax-addcl 7927, for naming consistency with addcli 7981. Use this theorem instead of ax-addcl 7927 or axaddcl 7883. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) | ||
Theorem | readdcl 7957 | Alias for ax-addrcl 7928, for naming consistency with readdcli 7990. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) | ||
Theorem | mulcl 7958 | Alias for ax-mulcl 7929, for naming consistency with mulcli 7982. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) | ||
Theorem | remulcl 7959 | Alias for ax-mulrcl 7930, for naming consistency with remulcli 7991. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) | ||
Theorem | mulcom 7960 | Alias for ax-mulcom 7932, for naming consistency with mulcomi 7983. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Theorem | addass 7961 | Alias for ax-addass 7933, for naming consistency with addassi 7985. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) | ||
Theorem | mulass 7962 | Alias for ax-mulass 7934, for naming consistency with mulassi 7986. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) | ||
Theorem | adddi 7963 | Alias for ax-distr 7935, for naming consistency with adddii 7987. (Contributed by NM, 10-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ))) | ||
Theorem | recn 7964 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
β’ (π΄ β β β π΄ β β) | ||
Theorem | reex 7965 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
β’ β β V | ||
Theorem | reelprrecn 7966 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ β β {β, β} | ||
Theorem | cnelprrecn 7967 | Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ β β {β, β} | ||
Theorem | adddir 7968 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β· πΆ) = ((π΄ Β· πΆ) + (π΅ Β· πΆ))) | ||
Theorem | 0cn 7969 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
β’ 0 β β | ||
Theorem | 0cnd 7970 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (π β 0 β β) | ||
Theorem | c0ex 7971 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
β’ 0 β V | ||
Theorem | 1ex 7972 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
β’ 1 β V | ||
Theorem | cnre 7973* | Alias for ax-cnre 7942, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
β’ (π΄ β β β βπ₯ β β βπ¦ β β π΄ = (π₯ + (i Β· π¦))) | ||
Theorem | mulrid 7974 | 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
β’ (π΄ β β β (π΄ Β· 1) = π΄) | ||
Theorem | mullid 7975 | Identity law for multiplication. Note: see mulrid 7974 for commuted version. (Contributed by NM, 8-Oct-1999.) |
β’ (π΄ β β β (1 Β· π΄) = π΄) | ||
Theorem | 1re 7976 | 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
β’ 1 β β | ||
Theorem | 0re 7977 | 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
β’ 0 β β | ||
Theorem | 0red 7978 | 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ (π β 0 β β) | ||
Theorem | mulid1i 7979 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
β’ π΄ β β β β’ (π΄ Β· 1) = π΄ | ||
Theorem | mullidi 7980 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
β’ π΄ β β β β’ (1 Β· π΄) = π΄ | ||
Theorem | addcli 7981 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) β β | ||
Theorem | mulcli 7982 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) β β | ||
Theorem | mulcomi 7983 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) = (π΅ Β· π΄) | ||
Theorem | mulcomli 7984 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ (π΄ Β· π΅) = πΆ β β’ (π΅ Β· π΄) = πΆ | ||
Theorem | addassi 7985 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ)) | ||
Theorem | mulassi 7986 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ)) | ||
Theorem | adddii 7987 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β· (π΅ + πΆ)) = ((π΄ Β· π΅) + (π΄ Β· πΆ)) | ||
Theorem | adddiri 7988 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) Β· πΆ) = ((π΄ Β· πΆ) + (π΅ Β· πΆ)) | ||
Theorem | recni 7989 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
β’ π΄ β β β β’ π΄ β β | ||
Theorem | readdcli 7990 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) β β | ||
Theorem | remulcli 7991 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) β β | ||
Theorem | 1red 7992 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ (π β 1 β β) | ||
Theorem | 1cnd 7993 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ (π β 1 β β) | ||
Theorem | mulridd 7994 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (π΄ Β· 1) = π΄) | ||
Theorem | mullidd 7995 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (1 Β· π΄) = π΄) | ||
Theorem | mulid2d 7996 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (1 Β· π΄) = π΄) | ||
Theorem | addcld 7997 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ + π΅) β β) | ||
Theorem | mulcld 7998 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· π΅) β β) | ||
Theorem | mulcomd 7999 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Theorem | addassd 8000 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |