Home | Intuitionistic Logic Explorer Theorem List (p. 75 of 116) | < 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 | axpre-mulgt0 7401 | 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 7441. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulext 7402 |
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 7442.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
Theorem | rereceu 7403* | The reciprocal from axprecex 7394 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recriota 7404* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | axarch 7405* |
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 8396 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 7443. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
Theorem | peano5nnnn 7406* | Peano's inductive postulate. This is a counterpart to peano5nni 8397 designed for real number axioms which involve natural numbers (notably, axcaucvg 7414). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nnindnn 7407* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8410 designed for real number axioms which involve natural numbers (notably, axcaucvg 7414). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nntopi 7408* | Mapping from to . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | axcaucvglemcl 7409* | Lemma for axcaucvg 7414. Mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemf 7410* | Lemma for axcaucvg 7414. Mapping to and yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemval 7411* | Lemma for axcaucvg 7414. Value of sequence when mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemcau 7412* | Lemma for axcaucvg 7414. The result of mapping to and satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemres 7413* | Lemma for axcaucvg 7414. Mapping the limit from and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvg 7414* |
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 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 7444. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
Axiom | ax-cnex 7415 | The complex numbers form a set. Proofs should normally use cnex 7445 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-resscn 7416 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7376. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1cn 7417 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7377. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1re 7418 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7378. Proofs should use 1re 7466 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
Axiom | ax-icn 7419 | is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7379. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-addcl 7420 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7380. Proofs should normally use addcl 7446 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 7421 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7381. Proofs should normally use readdcl 7447 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulcl 7422 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7382. Proofs should normally use mulcl 7448 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulrcl 7423 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7383. Proofs should normally use remulcl 7449 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addcom 7424 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7384. Proofs should normally use addcom 7598 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
Axiom | ax-mulcom 7425 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7385. Proofs should normally use mulcom 7450 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addass 7426 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7386. Proofs should normally use addass 7451 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulass 7427 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7387. Proofs should normally use mulass 7452 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-distr 7428 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7388. Proofs should normally use adddi 7453 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-i2m1 7429 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7389. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0lt1 7430 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7390. Proofs should normally use 0lt1 7589 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-1rid 7431 | is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7391. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0id 7432 |
is an identity element
for real addition. Axiom for real and
complex numbers, justified by theorem ax0id 7392.
Proofs should normally use addid1 7599 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
Axiom | ax-rnegex 7433* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7393. (Contributed by Eric Schmidt, 21-May-2007.) |
Axiom | ax-precex 7434* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7394. (Contributed by Jim Kingdon, 6-Feb-2020.) |
Axiom | ax-cnre 7435* | 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 7395. For naming consistency, use cnre 7463 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
Axiom | ax-pre-ltirr 7436 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7436. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-ltwlin 7437 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7397. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-lttrn 7438 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7398. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-apti 7439 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7399. (Contributed by Jim Kingdon, 29-Jan-2020.) |
Axiom | ax-pre-ltadd 7440 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7400. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulgt0 7441 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7401. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulext 7442 |
Strong extensionality of multiplication (expressed in terms of ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7402
(Contributed by Jim Kingdon, 18-Feb-2020.) |
Axiom | ax-arch 7443* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7405.
This axiom should not be used directly; instead use arch 8640 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
Axiom | ax-caucvg 7444* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7414.
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 of the nth term. This axiom should not be used directly; instead use caucvgre 10379 (which is the same, but stated in terms of the and notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) |
Theorem | cnex 7445 | Alias for ax-cnex 7415. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | addcl 7446 | Alias for ax-addcl 7420, for naming consistency with addcli 7471. Use this theorem instead of ax-addcl 7420 or axaddcl 7380. (Contributed by NM, 10-Mar-2008.) |
Theorem | readdcl 7447 | Alias for ax-addrcl 7421, for naming consistency with readdcli 7480. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcl 7448 | Alias for ax-mulcl 7422, for naming consistency with mulcli 7472. (Contributed by NM, 10-Mar-2008.) |
Theorem | remulcl 7449 | Alias for ax-mulrcl 7423, for naming consistency with remulcli 7481. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcom 7450 | Alias for ax-mulcom 7425, for naming consistency with mulcomi 7473. (Contributed by NM, 10-Mar-2008.) |
Theorem | addass 7451 | Alias for ax-addass 7426, for naming consistency with addassi 7475. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulass 7452 | Alias for ax-mulass 7427, for naming consistency with mulassi 7476. (Contributed by NM, 10-Mar-2008.) |
Theorem | adddi 7453 | Alias for ax-distr 7428, for naming consistency with adddii 7477. (Contributed by NM, 10-Mar-2008.) |
Theorem | recn 7454 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Theorem | reex 7455 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | reelprrecn 7456 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | cnelprrecn 7457 | 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 7458 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
Theorem | 0cn 7459 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
Theorem | 0cnd 7460 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | c0ex 7461 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1ex 7462 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | cnre 7463* | Alias for ax-cnre 7435, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Theorem | mulid1 7464 | is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mulid2 7465 | Identity law for multiplication. Note: see mulid1 7464 for commuted version. (Contributed by NM, 8-Oct-1999.) |
Theorem | 1re 7466 | is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
Theorem | 0re 7467 | is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | 0red 7468 | is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1i 7469 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | mulid2i 7470 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | addcli 7471 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcli 7472 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomi 7473 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomli 7474 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | addassi 7475 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulassi 7476 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | adddii 7477 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
Theorem | adddiri 7478 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
Theorem | recni 7479 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Theorem | readdcli 7480 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | remulcli 7481 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | 1red 7482 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 1cnd 7483 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1d 7484 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulid2d 7485 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcld 7486 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcld 7487 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcomd 7488 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addassd 7489 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulassd 7490 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddid 7491 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddird 7492 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddirp1d 7493 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | joinlmuladdmuld 7494 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
Theorem | recnd 7495 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
Theorem | readdcld 7496 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | remulcld 7497 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Syntax | cpnf 7498 | Plus infinity. |
Syntax | cmnf 7499 | Minus infinity. |
Syntax | cxr 7500 | The set of extended reals (includes plus and minus infinity). |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |