Home | Intuitionistic Logic Explorer Theorem List (p. 78 of 133) | < 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 | nnindnn 7701* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8736 designed for real number axioms which involve natural numbers (notably, axcaucvg 7708). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝑧 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ 𝑁 → 𝜏) | ||
Theorem | nntopi 7702* | 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 7703* | Lemma for axcaucvg 7708. 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 7704* | Lemma for axcaucvg 7708. 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 7705* | Lemma for axcaucvg 7708. 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 7706* | Lemma for axcaucvg 7708. 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 7707* | Lemma for axcaucvg 7708. 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 7708* |
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 7740. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) | ||
Theorem | axpre-suploclemres 7709* | Lemma for axpre-suploc 7710. 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 7617. (Contributed by Jim Kingdon, 24-Jan-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))) & ⊢ 𝐵 = {𝑤 ∈ R ∣ 〈𝑤, 0R〉 ∈ 𝐴} ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
Theorem | axpre-suploc 7710* |
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 7741. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
Axiom | ax-cnex 7711 | The complex numbers form a set. Proofs should normally use cnex 7744 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
⊢ ℂ ∈ V | ||
Axiom | ax-resscn 7712 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7668. (Contributed by NM, 1-Mar-1995.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-1cn 7713 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7669. (Contributed by NM, 1-Mar-1995.) |
⊢ 1 ∈ ℂ | ||
Axiom | ax-1re 7714 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7670. Proofs should use 1re 7765 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Axiom | ax-icn 7715 | i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7671. (Contributed by NM, 1-Mar-1995.) |
⊢ i ∈ ℂ | ||
Axiom | ax-addcl 7716 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7672. Proofs should normally use addcl 7745 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 7717 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7673. Proofs should normally use readdcl 7746 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Axiom | ax-mulcl 7718 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7674. Proofs should normally use mulcl 7747 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Axiom | ax-mulrcl 7719 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7675. Proofs should normally use remulcl 7748 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Axiom | ax-addcom 7720 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7678. Proofs should normally use addcom 7899 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Axiom | ax-mulcom 7721 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7679. Proofs should normally use mulcom 7749 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Axiom | ax-addass 7722 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7680. Proofs should normally use addass 7750 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Axiom | ax-mulass 7723 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7681. Proofs should normally use mulass 7751 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Axiom | ax-distr 7724 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7682. Proofs should normally use adddi 7752 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Axiom | ax-i2m1 7725 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7683. (Contributed by NM, 29-Jan-1995.) |
⊢ ((i · i) + 1) = 0 | ||
Axiom | ax-0lt1 7726 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7684. Proofs should normally use 0lt1 7889 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ 0 <ℝ 1 | ||
Axiom | ax-1rid 7727 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7685. (Contributed by NM, 29-Jan-1995.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Axiom | ax-0id 7728 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, justified by theorem ax0id 7686.
Proofs should normally use addid1 7900 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Axiom | ax-rnegex 7729* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7687. (Contributed by Eric Schmidt, 21-May-2007.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Axiom | ax-precex 7730* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7688. (Contributed by Jim Kingdon, 6-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1)) | ||
Axiom | ax-cnre 7731* | 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 7689. For naming consistency, use cnre 7762 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Axiom | ax-pre-ltirr 7732 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7732. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) | ||
Axiom | ax-pre-ltwlin 7733 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7691. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) | ||
Axiom | ax-pre-lttrn 7734 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7692. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Axiom | ax-pre-apti 7735 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7693. (Contributed by Jim Kingdon, 29-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) | ||
Axiom | ax-pre-ltadd 7736 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7694. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Axiom | ax-pre-mulgt0 7737 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7695. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Axiom | ax-pre-mulext 7738 |
Strong extensionality of multiplication (expressed in terms of <ℝ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7696
(Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Axiom | ax-arch 7739* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7699.
This axiom should not be used directly; instead use arch 8974 (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 7740* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7708.
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 10753 (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 7741* |
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 7740 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7740. (Contributed by Jim Kingdon, 23-Jan-2024.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
Axiom | ax-addf 7742 |
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 7745 should be used. Note that uses of ax-addf 7742 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 7676. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Axiom | ax-mulf 7743 |
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 7718 should be used. Note that uses of ax-mulf 7743
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 7677. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | cnex 7744 | Alias for ax-cnex 7711. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 7745 | Alias for ax-addcl 7716, for naming consistency with addcli 7770. Use this theorem instead of ax-addcl 7716 or axaddcl 7672. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | readdcl 7746 | Alias for ax-addrcl 7717, for naming consistency with readdcli 7779. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | mulcl 7747 | Alias for ax-mulcl 7718, for naming consistency with mulcli 7771. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | remulcl 7748 | Alias for ax-mulrcl 7719, for naming consistency with remulcli 7780. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | mulcom 7749 | Alias for ax-mulcom 7721, for naming consistency with mulcomi 7772. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addass 7750 | Alias for ax-addass 7722, for naming consistency with addassi 7774. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulass 7751 | Alias for ax-mulass 7723, for naming consistency with mulassi 7775. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddi 7752 | Alias for ax-distr 7724, for naming consistency with adddii 7776. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | recn 7753 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) | ||
Theorem | reex 7754 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℝ ∈ V | ||
Theorem | reelprrecn 7755 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℝ ∈ {ℝ, ℂ} | ||
Theorem | cnelprrecn 7756 | 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 7757 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | 0cn 7758 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnd 7759 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℂ) | ||
Theorem | c0ex 7760 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ∈ V | ||
Theorem | 1ex 7761 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 1 ∈ V | ||
Theorem | cnre 7762* | Alias for ax-cnre 7731, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | mulid1 7763 | 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | ||
Theorem | mulid2 7764 | Identity law for multiplication. Note: see mulid1 7763 for commuted version. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | 1re 7765 | 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
⊢ 1 ∈ ℝ | ||
Theorem | 0re 7766 | 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 0 ∈ ℝ | ||
Theorem | 0red 7767 | 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℝ) | ||
Theorem | mulid1i 7768 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 1) = 𝐴 | ||
Theorem | mulid2i 7769 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (1 · 𝐴) = 𝐴 | ||
Theorem | addcli 7770 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℂ | ||
Theorem | mulcli 7771 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℂ | ||
Theorem | mulcomi 7772 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | mulcomli 7773 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (𝐵 · 𝐴) = 𝐶 | ||
Theorem | addassi 7774 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | mulassi 7775 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | adddii 7776 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) | ||
Theorem | adddiri 7777 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)) | ||
Theorem | recni 7778 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | readdcli 7779 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℝ | ||
Theorem | remulcli 7780 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℝ | ||
Theorem | 1red 7781 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 1 ∈ ℝ) | ||
Theorem | 1cnd 7782 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 1 ∈ ℂ) | ||
Theorem | mulid1d 7783 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐴) | ||
Theorem | mulid2d 7784 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐴) | ||
Theorem | addcld 7785 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | mulcld 7786 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | mulcomd 7787 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addassd 7788 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulassd 7789 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddid 7790 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | adddird 7791 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | adddirp1d 7792 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵)) | ||
Theorem | joinlmuladdmuld 7793 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷) | ||
Theorem | recnd 7794 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | readdcld 7795 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | remulcld 7796 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) | ||
Syntax | cpnf 7797 | Plus infinity. |
class +∞ | ||
Syntax | cmnf 7798 | Minus infinity. |
class -∞ | ||
Syntax | cxr 7799 | The set of extended reals (includes plus and minus infinity). |
class ℝ* | ||
Syntax | clt 7800 | 'Less than' predicate (extended to include the extended reals). |
class < |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |