Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 108) | < 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 | ltrelre 7001 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <ℝ ⊆ (ℝ × ℝ) | ||
Theorem | addcnsr 7002 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉) = 〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉) | ||
Theorem | mulcnsr 7003 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉) | ||
Theorem | eqresr 7004 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (〈𝐴, 0R〉 = 〈𝐵, 0R〉 ↔ 𝐴 = 𝐵) | ||
Theorem | addresr 7005 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 + 〈𝐵, 0R〉) = 〈(𝐴 +R 𝐵), 0R〉) | ||
Theorem | mulresr 7006 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 · 〈𝐵, 0R〉) = 〈(𝐴 ·R 𝐵), 0R〉) | ||
Theorem | ltresr 7007 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ (〈𝐴, 0R〉 <ℝ 〈𝐵, 0R〉 ↔ 𝐴 <R 𝐵) | ||
Theorem | ltresr2 7008 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵))) | ||
Theorem | dfcnqs 7009 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6194, 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 6987), 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 7010 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7009 and mulcnsrec 7011. (Contributed by NM, 13-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E + [〈𝐶, 𝐷〉]◡ E ) = [〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉]◡ E ) | ||
Theorem | mulcnsrec 7011 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6193, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7009. (Contributed by NM, 13-Aug-1995.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E ) | ||
Theorem | addvalex 7012 | 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 7098. (Contributed by Jim Kingdon, 14-Jul-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 + 𝐵) ∈ V) | ||
Theorem | pitonnlem1 7013* | Lemma for pitonn 7016. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈1𝑜, 1𝑜〉] ~Q }, {𝑢 ∣ [〈1𝑜, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 = 1 | ||
Theorem | pitonnlem1p1 7014 | Lemma for pitonn 7016. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ P → [〈(𝐴 +P (1P +P 1P)), (1P +P 1P)〉] ~R = [〈(𝐴 +P 1P), 1P〉] ~R ) | ||
Theorem | pitonnlem2 7015* | Lemma for pitonn 7016. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ (𝐾 ∈ N → (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐾, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 + 1) = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈(𝐾 +N 1𝑜), 1𝑜〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N 1𝑜), 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | pitonn 7016* | Mapping from N to ℕ. (Contributed by Jim Kingdon, 22-Apr-2020.) |
⊢ (𝑁 ∈ N → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝑁, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) | ||
Theorem | pitoregt0 7017* | 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 1P), 1P〉] ~R , 0R〉) | ||
Theorem | pitore 7018* | Embedding from N to ℝ. Similar to pitonn 7016 but separate in the sense that we have not proved nnssre 8043 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ (𝑁 ∈ N → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝑁, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 ∈ ℝ) | ||
Theorem | recnnre 7019* | 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 1P), 1P〉] ~R , 0R〉 ∈ ℝ) | ||
Theorem | peano1nnnn 7020* | One is an element of ℕ. This is a counterpart to 1nn 8050 designed for real number axioms which involve natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ 1 ∈ 𝑁 | ||
Theorem | peano2nnnn 7021* | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8051 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑁 → (𝐴 + 1) ∈ 𝑁) | ||
Theorem | ltrennb 7022* | Ordering of natural numbers with <N or <ℝ. (Contributed by Jim Kingdon, 13-Jul-2021.) |
⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <N 𝐾 ↔ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐽, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐽, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 <ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐾, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉)) | ||
Theorem | ltrenn 7023* | Ordering of natural numbers with <N or <ℝ. (Contributed by Jim Kingdon, 12-Jul-2021.) |
⊢ (𝐽 <N 𝐾 → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐽, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐽, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 <ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐾, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | recidpipr 7024* | 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 𝑢}〉) = 1P) | ||
Theorem | recidpirqlemcalc 7025 | Lemma for recidpirq 7026. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → (𝐴 ·P 𝐵) = 1P) ⇒ ⊢ (𝜑 → ((((𝐴 +P 1P) ·P (𝐵 +P 1P)) +P (1P ·P 1P)) +P 1P) = ((((𝐴 +P 1P) ·P 1P) +P (1P ·P (𝐵 +P 1P))) +P (1P +P 1P))) | ||
Theorem | recidpirq 7026* | 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 1P), 1P〉] ~R , 0R〉 · 〈[〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑁, 1𝑜〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑁, 1𝑜〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) = 1) | ||
Theorem | axcnex 7027 | The complex numbers form a set. Use cnex 7097 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | axresscn 7028 | 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 7068. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
⊢ ℝ ⊆ ℂ | ||
Theorem | ax1cn 7029 | 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 7069. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
⊢ 1 ∈ ℂ | ||
Theorem | ax1re 7030 |
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 7070.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7069 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 7031 | 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 7071. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
⊢ i ∈ ℂ | ||
Theorem | axaddcl 7032 | 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 7072 be used later. Instead, in most cases use addcl 7098. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | axaddrcl 7033 | 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 7073 be used later. Instead, in most cases use readdcl 7099. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | axmulcl 7034 | 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 7074 be used later. Instead, in most cases use mulcl 7100. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | axmulrcl 7035 | 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 7075 be used later. Instead, in most cases use remulcl 7101. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | axaddcom 7036 |
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 7076 be used later.
Instead, use addcom 7245.
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 7037 | 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 7077 be used later. Instead, use mulcom 7102. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | axaddass 7038 | 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 7078 be used later. Instead, use addass 7103. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | axmulass 7039 | 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 7079. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | axdistr 7040 | 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 7080 be used later. Instead, use adddi 7105. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | axi2m1 7041 | 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 7081. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax0lt1 7042 |
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 7082.
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 7043 | 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 7083. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Theorem | ax0id 7044 |
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 7084.
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 7045* | 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 7085. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | axprecex 7046* |
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 7086.
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 7047* | 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 7087. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | axpre-ltirr 7048 | 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 7088. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) | ||
Theorem | axpre-ltwlin 7049 | 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 7089. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) | ||
Theorem | axpre-lttrn 7050 | 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 7090. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Theorem | axpre-apti 7051 |
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 7091.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | axpre-ltadd 7052 | 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 7092. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Theorem | axpre-mulgt0 7053 | 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 7093. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Theorem | axpre-mulext 7054 |
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 7094.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Theorem | rereceu 7055* | The reciprocal from axprecex 7046 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Theorem | recriota 7056* | 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 1P), 1P〉] ~R , 0R〉 · 𝑟) = 1) = 〈[〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑁, 1𝑜〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑁, 1𝑜〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) | ||
Theorem | axarch 7057* |
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 8041 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 7095. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛) | ||
Theorem | peano5nnnn 7058* | Peano's inductive postulate. This is a counterpart to peano5nni 8042 designed for real number axioms which involve natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ ((1 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴) | ||
Theorem | nnindnn 7059* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8055 designed for real number axioms which involve natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝑧 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ 𝑁 → 𝜏) | ||
Theorem | nntopi 7060* | Mapping from ℕ to N. (Contributed by Jim Kingdon, 13-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑁 → ∃𝑧 ∈ N 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑧, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝑧, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉 = 𝐴) | ||
Theorem | axcaucvglemcl 7061* | Lemma for axcaucvg 7066. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (℩𝑧 ∈ R (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐽, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐽, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) = 〈𝑧, 0R〉) ∈ R) | ||
Theorem | axcaucvglemf 7062* | Lemma for axcaucvg 7066. 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 1P), 1P〉] ~R , 0R〉) = 〈𝑧, 0R〉)) ⇒ ⊢ (𝜑 → 𝐺:N⟶R) | ||
Theorem | axcaucvglemval 7063* | Lemma for axcaucvg 7066. 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 1P), 1P〉] ~R , 0R〉) = 〈𝑧, 0R〉)) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐽, 1𝑜〉] ~Q }, {𝑢 ∣ [〈𝐽, 1𝑜〉] ~Q <Q 𝑢}〉 +P 1P), 1P〉] ~R , 0R〉) = 〈(𝐺‘𝐽), 0R〉) | ||
Theorem | axcaucvglemcau 7064* | Lemma for axcaucvg 7066. 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 1P), 1P〉] ~R , 0R〉) = 〈𝑧, 0R〉)) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1𝑜〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1𝑜〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) | ||
Theorem | axcaucvglemres 7065* | Lemma for axcaucvg 7066. 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 1P), 1P〉] ~R , 0R〉) = 〈𝑧, 0R〉)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) | ||
Theorem | axcaucvg 7066* |
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 7096. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) | ||
Axiom | ax-cnex 7067 | The complex numbers form a set. Proofs should normally use cnex 7097 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
⊢ ℂ ∈ V | ||
Axiom | ax-resscn 7068 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7028. (Contributed by NM, 1-Mar-1995.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-1cn 7069 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7029. (Contributed by NM, 1-Mar-1995.) |
⊢ 1 ∈ ℂ | ||
Axiom | ax-1re 7070 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7030. Proofs should use 1re 7118 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Axiom | ax-icn 7071 | i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7031. (Contributed by NM, 1-Mar-1995.) |
⊢ i ∈ ℂ | ||
Axiom | ax-addcl 7072 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7032. Proofs should normally use addcl 7098 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 7073 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7033. Proofs should normally use readdcl 7099 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Axiom | ax-mulcl 7074 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7034. Proofs should normally use mulcl 7100 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Axiom | ax-mulrcl 7075 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7035. Proofs should normally use remulcl 7101 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Axiom | ax-addcom 7076 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7036. Proofs should normally use addcom 7245 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Axiom | ax-mulcom 7077 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7037. Proofs should normally use mulcom 7102 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Axiom | ax-addass 7078 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7038. Proofs should normally use addass 7103 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Axiom | ax-mulass 7079 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7039. Proofs should normally use mulass 7104 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Axiom | ax-distr 7080 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7040. Proofs should normally use adddi 7105 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Axiom | ax-i2m1 7081 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7041. (Contributed by NM, 29-Jan-1995.) |
⊢ ((i · i) + 1) = 0 | ||
Axiom | ax-0lt1 7082 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7042. Proofs should normally use 0lt1 7236 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ 0 <ℝ 1 | ||
Axiom | ax-1rid 7083 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7043. (Contributed by NM, 29-Jan-1995.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Axiom | ax-0id 7084 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, justified by theorem ax0id 7044.
Proofs should normally use addid1 7246 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Axiom | ax-rnegex 7085* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7045. (Contributed by Eric Schmidt, 21-May-2007.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Axiom | ax-precex 7086* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7046. (Contributed by Jim Kingdon, 6-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1)) | ||
Axiom | ax-cnre 7087* | 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 7047. For naming consistency, use cnre 7115 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Axiom | ax-pre-ltirr 7088 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7088. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) | ||
Axiom | ax-pre-ltwlin 7089 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7049. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) | ||
Axiom | ax-pre-lttrn 7090 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7050. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Axiom | ax-pre-apti 7091 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7051. (Contributed by Jim Kingdon, 29-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) | ||
Axiom | ax-pre-ltadd 7092 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7052. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Axiom | ax-pre-mulgt0 7093 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7053. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Axiom | ax-pre-mulext 7094 |
Strong extensionality of multiplication (expressed in terms of <ℝ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7054
(Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Axiom | ax-arch 7095* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7057.
This axiom should not be used directly; instead use arch 8285 (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 7096* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7066.
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 9867 (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 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) | ||
Theorem | cnex 7097 | Alias for ax-cnex 7067. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 7098 | Alias for ax-addcl 7072, for naming consistency with addcli 7123. Use this theorem instead of ax-addcl 7072 or axaddcl 7032. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | readdcl 7099 | Alias for ax-addrcl 7073, for naming consistency with readdcli 7132. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | mulcl 7100 | Alias for ax-mulcl 7074, for naming consistency with mulcli 7124. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |