Home | Intuitionistic Logic Explorer Theorem List (p. 70 of 102) | < 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 | ||
Definition | df-mul 6901* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) |
⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·_{R} 𝑢) +_{R} (-1_{R} ·_{R} (𝑣 ·_{R} 𝑓))), ((𝑣 ·_{R} 𝑢) +_{R} (𝑤 ·_{R} 𝑓))⟩))} | ||
Definition | df-lt 6902* | Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <_{ℝ} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0_{R}⟩ ∧ 𝑦 = ⟨𝑤, 0_{R}⟩) ∧ 𝑧 <_{R} 𝑤))} | ||
Theorem | opelcn 6903 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) |
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R)) | ||
Theorem | opelreal 6904 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ (⟨𝐴, 0_{R}⟩ ∈ ℝ ↔ 𝐴 ∈ R) | ||
Theorem | elreal 6905* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) |
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0_{R}⟩ = 𝐴) | ||
Theorem | elrealeu 6906* | The real number mapping in elreal 6905 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) |
⊢ (𝐴 ∈ ℝ ↔ ∃!𝑥 ∈ R ⟨𝑥, 0_{R}⟩ = 𝐴) | ||
Theorem | elreal2 6907 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) |
⊢ (𝐴 ∈ ℝ ↔ ((1^{st} ‘𝐴) ∈ R ∧ 𝐴 = ⟨(1^{st} ‘𝐴), 0_{R}⟩)) | ||
Theorem | 0ncn 6908 | The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by NM, 2-May-1996.) |
⊢ ¬ ∅ ∈ ℂ | ||
Theorem | ltrelre 6909 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <_{ℝ} ⊆ (ℝ × ℝ) | ||
Theorem | addcnsr 6910 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +_{R} 𝐶), (𝐵 +_{R} 𝐷)⟩) | ||
Theorem | mulcnsr 6911 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ · ⟨𝐶, 𝐷⟩) = ⟨((𝐴 ·_{R} 𝐶) +_{R} (-1_{R} ·_{R} (𝐵 ·_{R} 𝐷))), ((𝐵 ·_{R} 𝐶) +_{R} (𝐴 ·_{R} 𝐷))⟩) | ||
Theorem | eqresr 6912 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (⟨𝐴, 0_{R}⟩ = ⟨𝐵, 0_{R}⟩ ↔ 𝐴 = 𝐵) | ||
Theorem | addresr 6913 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0_{R}⟩ + ⟨𝐵, 0_{R}⟩) = ⟨(𝐴 +_{R} 𝐵), 0_{R}⟩) | ||
Theorem | mulresr 6914 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0_{R}⟩ · ⟨𝐵, 0_{R}⟩) = ⟨(𝐴 ·_{R} 𝐵), 0_{R}⟩) | ||
Theorem | ltresr 6915 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ (⟨𝐴, 0_{R}⟩ <_{ℝ} ⟨𝐵, 0_{R}⟩ ↔ 𝐴 <_{R} 𝐵) | ||
Theorem | ltresr2 6916 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 ↔ (1^{st} ‘𝐴) <_{R} (1^{st} ‘𝐵))) | ||
Theorem | dfcnqs 6917 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6171, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that ℂ is a quotient set, even though it is not (compare df-c 6895), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.) |
⊢ ℂ = ((R × R) / ^{◡} E ) | ||
Theorem | addcnsrec 6918 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 6917 and mulcnsrec 6919. (Contributed by NM, 13-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]^{◡} E + [⟨𝐶, 𝐷⟩]^{◡} E ) = [⟨(𝐴 +_{R} 𝐶), (𝐵 +_{R} 𝐷)⟩]^{◡} E ) | ||
Theorem | mulcnsrec 6919 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6170, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 6917. (Contributed by NM, 13-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]^{◡} E · [⟨𝐶, 𝐷⟩]^{◡} E ) = [⟨((𝐴 ·_{R} 𝐶) +_{R} (-1_{R} ·_{R} (𝐵 ·_{R} 𝐷))), ((𝐵 ·_{R} 𝐶) +_{R} (𝐴 ·_{R} 𝐷))⟩]^{◡} E ) | ||
Theorem | addvalex 6920 | Existence of a sum. This is dependent on how we define + so once we proceed to real number axioms we will replace it with theorems such as addcl 7006. (Contributed by Jim Kingdon, 14-Jul-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 + 𝐵) ∈ V) | ||
Theorem | pitonnlem1 6921* | Lemma for pitonn 6924. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨1_{𝑜}, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨1_{𝑜}, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ = 1 | ||
Theorem | pitonnlem1p1 6922 | Lemma for pitonn 6924. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ P → [⟨(𝐴 +_{P} (1_{P} +_{P} 1_{P})), (1_{P} +_{P} 1_{P})⟩] ~_{R} = [⟨(𝐴 +_{P} 1_{P}), 1_{P}⟩] ~_{R} ) | ||
Theorem | pitonnlem2 6923* | Lemma for pitonn 6924. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐾, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐾, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ + 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨(𝐾 +_{N} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨(𝐾 +_{N} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) | ||
Theorem | pitonn 6924* | Mapping from N to ℕ. (Contributed by Jim Kingdon, 22-Apr-2020.) |
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) | ||
Theorem | pitoregt0 6925* | Embedding from N to ℝ yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → 0 <_{ℝ} ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) | ||
Theorem | pitore 6926* | Embedding from N to ℝ. Similar to pitonn 6924 but separate in the sense that we have not proved nnssre 7918 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ ∈ ℝ) | ||
Theorem | recnnre 6927* | Embedding the reciprocal of a natural number into ℝ. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ ∈ ℝ) | ||
Theorem | peano1nnnn 6928* | One is an element of ℕ. This is a counterpart to 1nn 7925 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ 1 ∈ 𝑁 | ||
Theorem | peano2nnnn 6929* | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 7926 designed for real number axioms which involve to natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑁 → (𝐴 + 1) ∈ 𝑁) | ||
Theorem | ltrennb 6930* | Ordering of natural numbers with <_{N} or <_{ℝ}. (Contributed by Jim Kingdon, 13-Jul-2021.) |
⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <_{N} 𝐾 ↔ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐽, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐽, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ <_{ℝ} ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐾, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐾, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩)) | ||
Theorem | ltrenn 6931* | Ordering of natural numbers with <_{N} or <_{ℝ}. (Contributed by Jim Kingdon, 12-Jul-2021.) |
⊢ (𝐽 <_{N} 𝐾 → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐽, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐽, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ <_{ℝ} ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐾, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐾, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) | ||
Theorem | recidpipr 6932* | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) |
⊢ (𝑁 ∈ N → (⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ ·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩) = 1_{P}) | ||
Theorem | recidpirqlemcalc 6933 | Lemma for recidpirq 6934. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → (𝐴 ·_{P} 𝐵) = 1_{P}) ⇒ ⊢ (𝜑 → ((((𝐴 +_{P} 1_{P}) ·_{P} (𝐵 +_{P} 1_{P})) +_{P} (1_{P} ·_{P} 1_{P})) +_{P} 1_{P}) = ((((𝐴 +_{P} 1_{P}) ·_{P} 1_{P}) +_{P} (1_{P} ·_{P} (𝐵 +_{P} 1_{P}))) +_{P} (1_{P} +_{P} 1_{P}))) | ||
Theorem | recidpirq 6934* | A real number times its reciprocal is one, where reciprocal is expressed with *_{Q}. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ · ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = 1) | ||
Theorem | axcnex 6935 | The complex numbers form a set. Use cnex 7005 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | axresscn 6936 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 6976. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
⊢ ℝ ⊆ ℂ | ||
Theorem | ax1cn 6937 | 1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 6977. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
⊢ 1 ∈ ℂ | ||
Theorem | ax1re 6938 |
1 is a real number. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-1re 6978.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6977 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Theorem | axicn 6939 | i is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 6979. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
⊢ i ∈ ℂ | ||
Theorem | axaddcl 6940 | Closure law for addition of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 6980 be used later. Instead, in most cases use addcl 7006. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | axaddrcl 6941 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 6981 be used later. Instead, in most cases use readdcl 7007. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | axmulcl 6942 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 6982 be used later. Instead, in most cases use mulcl 7008. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | axmulrcl 6943 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 6983 be used later. Instead, in most cases use remulcl 7009. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | axaddcom 6944 |
Addition commutes. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly, nor should the proven axiom ax-addcom 6984 be used later.
Instead, use addcom 7150.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | axmulcom 6945 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 6985 be used later. Instead, use mulcom 7010. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | axaddass 6946 | Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 6986 be used later. Instead, use addass 7011. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | axmulass 6947 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 6987. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | axdistr 6948 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 6988 be used later. Instead, use adddi 7013. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | axi2m1 6949 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 6989. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax0lt1 6950 |
0 is less than 1. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-0lt1 6990.
The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 <_{ℝ} 1. The proof of 0 <_{ℝ} 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ 0 <_{ℝ} 1 | ||
Theorem | ax1rid 6951 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 6991. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Theorem | ax0id 6952 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, derived from set theory. This construction-dependent
theorem should not be referenced directly; instead, use ax-0id 6992.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Theorem | axrnegex 6953* | Existence of negative of real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 6993. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | axprecex 6954* |
Existence of positive reciprocal of positive real number. Axiom for
real and complex numbers, derived from set theory. This
construction-dependent theorem should not be referenced directly;
instead, use ax-precex 6994.
In treatments which assume excluded middle, the 0 <_{ℝ} 𝐴 condition is generally replaced by 𝐴 ≠ 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <_{ℝ} 𝐴) → ∃𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 ∧ (𝐴 · 𝑥) = 1)) | ||
Theorem | axcnre 6955* | 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, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 6995. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | axpre-ltirr 6956 | 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 6996. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <_{ℝ} 𝐴) | ||
Theorem | axpre-ltwlin 6957 | 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 6997. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐴 <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} 𝐵))) | ||
Theorem | axpre-lttrn 6958 | 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 6998. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <_{ℝ} 𝐵 ∧ 𝐵 <_{ℝ} 𝐶) → 𝐴 <_{ℝ} 𝐶)) | ||
Theorem | axpre-apti 6959 |
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 6999.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | axpre-ltadd 6960 | 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 7000. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐶 + 𝐴) <_{ℝ} (𝐶 + 𝐵))) | ||
Theorem | axpre-mulgt0 6961 | 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 7001. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <_{ℝ} 𝐴 ∧ 0 <_{ℝ} 𝐵) → 0 <_{ℝ} (𝐴 · 𝐵))) | ||
Theorem | axpre-mulext 6962 |
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 7002.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <_{ℝ} (𝐵 · 𝐶) → (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴))) | ||
Theorem | rereceu 6963* | The reciprocal from axprecex 6954 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <_{ℝ} 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Theorem | recriota 6964* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
⊢ (𝑁 ∈ N → (℩𝑟 ∈ ℝ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ · 𝑟) = 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑁, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) | ||
Theorem | axarch 6965* |
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 7916 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 7003. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <_{ℝ} 𝑛) | ||
Theorem | peano5nnnn 6966* | Peano's inductive postulate. This is a counterpart to peano5nni 7917 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ ((1 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴) | ||
Theorem | nnindnn 6967* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 7930 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝑧 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ 𝑁 → 𝜏) | ||
Theorem | nntopi 6968* | Mapping from ℕ to N. (Contributed by Jim Kingdon, 13-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑁 → ∃𝑧 ∈ N ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑧, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑧, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ = 𝐴) | ||
Theorem | axcaucvglemcl 6969* | Lemma for axcaucvg 6974. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐽, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐽, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩) ∈ R) | ||
Theorem | axcaucvglemf 6970* | Lemma for axcaucvg 6974. Mapping to N and R yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <_{ℝ} 𝑘 → ((𝐹‘𝑛) <_{ℝ} ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <_{ℝ} ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) & ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑗, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ (𝜑 → 𝐺:N⟶R) | ||
Theorem | axcaucvglemval 6971* | Lemma for axcaucvg 6974. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <_{ℝ} 𝑘 → ((𝐹‘𝑛) <_{ℝ} ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <_{ℝ} ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) & ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑗, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐽, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐽, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨(𝐺‘𝐽), 0_{R}⟩) | ||
Theorem | axcaucvglemcau 6972* | Lemma for axcaucvg 6974. 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} [⟨𝑗, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_{N} 𝑘 → ((𝐺‘𝑛) <_{R} ((𝐺‘𝑘) +_{R} [⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑛, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑛, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} ) ∧ (𝐺‘𝑘) <_{R} ((𝐺‘𝑛) +_{R} [⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑛, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑛, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} )))) | ||
Theorem | axcaucvglemres 6973* | Lemma for axcaucvg 6974. Mapping the limit from N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <_{ℝ} 𝑘 → ((𝐹‘𝑛) <_{ℝ} ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <_{ℝ} ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) & ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑗, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <_{ℝ} 𝑘 → ((𝐹‘𝑘) <_{ℝ} (𝑦 + 𝑥) ∧ 𝑦 <_{ℝ} ((𝐹‘𝑘) + 𝑥))))) | ||
Theorem | axcaucvg 6974* |
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 7004. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <_{ℝ} 𝑘 → ((𝐹‘𝑛) <_{ℝ} ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <_{ℝ} ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <_{ℝ} 𝑘 → ((𝐹‘𝑘) <_{ℝ} (𝑦 + 𝑥) ∧ 𝑦 <_{ℝ} ((𝐹‘𝑘) + 𝑥))))) | ||
Axiom | ax-cnex 6975 | The complex numbers form a set. Proofs should normally use cnex 7005 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
⊢ ℂ ∈ V | ||
Axiom | ax-resscn 6976 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6936. (Contributed by NM, 1-Mar-1995.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-1cn 6977 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6937. (Contributed by NM, 1-Mar-1995.) |
⊢ 1 ∈ ℂ | ||
Axiom | ax-1re 6978 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6938. Proofs should use 1re 7026 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Axiom | ax-icn 6979 | i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6939. (Contributed by NM, 1-Mar-1995.) |
⊢ i ∈ ℂ | ||
Axiom | ax-addcl 6980 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 6940. Proofs should normally use addcl 7006 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 6981 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 6941. Proofs should normally use readdcl 7007 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Axiom | ax-mulcl 6982 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 6942. Proofs should normally use mulcl 7008 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Axiom | ax-mulrcl 6983 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 6943. Proofs should normally use remulcl 7009 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Axiom | ax-addcom 6984 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6944. Proofs should normally use addcom 7150 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Axiom | ax-mulcom 6985 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 6945. Proofs should normally use mulcom 7010 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Axiom | ax-addass 6986 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 6946. Proofs should normally use addass 7011 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Axiom | ax-mulass 6987 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 6947. Proofs should normally use mulass 7012 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Axiom | ax-distr 6988 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 6948. Proofs should normally use adddi 7013 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Axiom | ax-i2m1 6989 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 6949. (Contributed by NM, 29-Jan-1995.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax-0lt1 6990 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6950. Proofs should normally use 0lt1 7141 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ 0 <_{ℝ} 1 | ||
Axiom | ax-1rid 6991 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 6951. (Contributed by NM, 29-Jan-1995.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Axiom | ax-0id 6992 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, justified by theorem ax0id 6952.
Proofs should normally use addid1 7151 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Axiom | ax-rnegex 6993* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 6953. (Contributed by Eric Schmidt, 21-May-2007.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Axiom | ax-precex 6994* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6954. (Contributed by Jim Kingdon, 6-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <_{ℝ} 𝐴) → ∃𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 ∧ (𝐴 · 𝑥) = 1)) | ||
Axiom | ax-cnre 6995* | 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 6955. For naming consistency, use cnre 7023 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Axiom | ax-pre-ltirr 6996 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6996. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <_{ℝ} 𝐴) | ||
Axiom | ax-pre-ltwlin 6997 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6957. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐴 <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} 𝐵))) | ||
Axiom | ax-pre-lttrn 6998 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 6958. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <_{ℝ} 𝐵 ∧ 𝐵 <_{ℝ} 𝐶) → 𝐴 <_{ℝ} 𝐶)) | ||
Axiom | ax-pre-apti 6999 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6959. (Contributed by Jim Kingdon, 29-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴)) → 𝐴 = 𝐵) | ||
Axiom | ax-pre-ltadd 7000 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 6960. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐶 + 𝐴) <_{ℝ} (𝐶 + 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |