 Home Intuitionistic Logic ExplorerTheorem List (p. 74 of 114) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 7301-7400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Definitiondf-0 7301 Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
0 = ⟨0R, 0R

Definitiondf-1 7302 Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
1 = ⟨1R, 0R

Definitiondf-i 7303 Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
i = ⟨0R, 1R

Definitiondf-r 7304 Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
ℝ = (R × {0R})

Definitiondf-add 7305* Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
+ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}

Definitiondf-mul 7306* Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
· = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}

Definitiondf-lt 7307* Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
< = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}

Theoremopelcn 7308 Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
(⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴R𝐵R))

Theoremopelreal 7309 Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
(⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴R)

Theoremelreal 7310* Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
(𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)

Theoremelrealeu 7311* The real number mapping in elreal 7310 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
(𝐴 ∈ ℝ ↔ ∃!𝑥R𝑥, 0R⟩ = 𝐴)

Theoremelreal2 7312 Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
(𝐴 ∈ ℝ ↔ ((1st𝐴) ∈ R𝐴 = ⟨(1st𝐴), 0R⟩))

Theorem0ncn 7313 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.)
¬ ∅ ∈ ℂ

Theoremltrelre 7314 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
< ⊆ (ℝ × ℝ)

Theoremaddcnsr 7315 Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
(((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩)

Theoremmulcnsr 7316 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 𝐷))⟩)

Theoremeqresr 7317 Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
𝐴 ∈ V       (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)

Theoremaddresr 7318 Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
((𝐴R𝐵R) → (⟨𝐴, 0R⟩ + ⟨𝐵, 0R⟩) = ⟨(𝐴 +R 𝐵), 0R⟩)

Theoremmulresr 7319 Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
((𝐴R𝐵R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)

Theoremltresr 7320 Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
(⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)

Theoremltresr2 7321 Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (1st𝐴) <R (1st𝐵)))

Theoremdfcnqs 7322 Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in R. The trick involves qsid 6309, 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 7300), 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 )

Theoremaddcnsrec 7323 Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7322 and mulcnsrec 7324. (Contributed by NM, 13-Aug-1995.)
(((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → ([⟨𝐴, 𝐵⟩] E + [⟨𝐶, 𝐷⟩] E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩] E )

Theoremmulcnsrec 7324 Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6308, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7322. (Contributed by NM, 13-Aug-1995.)
(((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → ([⟨𝐴, 𝐵⟩] E · [⟨𝐶, 𝐷⟩] E ) = [⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩] E )

Theoremaddvalex 7325 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 7411. (Contributed by Jim Kingdon, 14-Jul-2021.)
((𝐴𝑉𝐵𝑊) → (𝐴 + 𝐵) ∈ V)

Theorempitonnlem1 7326* Lemma for pitonn 7329. 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

Theorempitonnlem1p1 7327 Lemma for pitonn 7329. 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 )

Theorempitonnlem2 7328* Lemma for pitonn 7329. 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⟩)

Theorempitonn 7329* 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) ∈ 𝑥)})

Theorempitoregt0 7330* 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⟩)

Theorempitore 7331* Embedding from N to . Similar to pitonn 7329 but separate in the sense that we have not proved nnssre 8361 yet. (Contributed by Jim Kingdon, 15-Jul-2021.)
(𝑁N → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑁, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ℝ)

Theoremrecnnre 7332* 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⟩ ∈ ℝ)

Theorempeano1nnnn 7333* One is an element of . This is a counterpart to 1nn 8368 designed for real number axioms which involve natural numbers (notably, axcaucvg 7379). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}       1 ∈ 𝑁

Theorempeano2nnnn 7334* A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8369 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7379). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}       (𝐴𝑁 → (𝐴 + 1) ∈ 𝑁)

Theoremltrennb 7335* 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⟩))

Theoremltrenn 7336* 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⟩)

Theoremrecidpipr 7337* 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)

Theoremrecidpirqlemcalc 7338 Lemma for recidpirq 7339. 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)))

Theoremrecidpirq 7339* 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)

3.1.2  Final derivation of real and complex number postulates

Theoremaxcnex 7340 The complex numbers form a set. Use cnex 7410 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
ℂ ∈ V

Theoremaxresscn 7341 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 7381. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
ℝ ⊆ ℂ

Theoremax1cn 7342 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 7382. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
1 ∈ ℂ

Theoremax1re 7343 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 7383.

In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7382 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 ∈ ℝ

Theoremaxicn 7344 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 7384. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
i ∈ ℂ

Theoremaxaddcl 7345 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 7385 be used later. Instead, in most cases use addcl 7411. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Theoremaxaddrcl 7346 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 7386 be used later. Instead, in most cases use readdcl 7412. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Theoremaxmulcl 7347 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 7387 be used later. Instead, in most cases use mulcl 7413. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Theoremaxmulrcl 7348 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 7388 be used later. Instead, in most cases use remulcl 7414. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Theoremaxaddcom 7349 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 7389 be used later. Instead, use addcom 7563.

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.)

((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Theoremaxmulcom 7350 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 7390 be used later. Instead, use mulcom 7415. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Theoremaxaddass 7351 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 7391 be used later. Instead, use addass 7416. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Theoremaxmulass 7352 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 7392. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Theoremaxdistr 7353 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 7393 be used later. Instead, use adddi 7418. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Theoremaxi2m1 7354 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 7394. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
((i · i) + 1) = 0

Theoremax0lt1 7355 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 7395.

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

Theoremax1rid 7356 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 7396. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Theoremax0id 7357 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 7397.

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) = 𝐴)

Theoremaxrnegex 7358* 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 7398. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)

Theoremaxprecex 7359* 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 7399.

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))

Theoremaxcnre 7360* 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 7400. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Theoremaxpre-ltirr 7361 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 7401. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)

Theoremaxpre-ltwlin 7362 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 7402. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))

Theoremaxpre-lttrn 7363 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 7403. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremaxpre-apti 7364 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 7404.

(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)

Theoremaxpre-ltadd 7365 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 7405. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))

Theoremaxpre-mulgt0 7366 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 7406. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))

Theoremaxpre-mulext 7367 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 7407.

(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))

Theoremrereceu 7368* The reciprocal from axprecex 7359 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)

Theoremrecriota 7369* 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⟩)

Theoremaxarch 7370* 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 8359 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 7408. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)

(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)

Theorempeano5nnnn 7371* Peano's inductive postulate. This is a counterpart to peano5nni 8360 designed for real number axioms which involve natural numbers (notably, axcaucvg 7379). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}       ((1 ∈ 𝐴 ∧ ∀𝑧𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁𝐴)

Theoremnnindnn 7372* Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8373 designed for real number axioms which involve natural numbers (notably, axcaucvg 7379). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝑧 = 1 → (𝜑𝜓))    &   (𝑧 = 𝑘 → (𝜑𝜒))    &   (𝑧 = (𝑘 + 1) → (𝜑𝜃))    &   (𝑧 = 𝐴 → (𝜑𝜏))    &   𝜓    &   (𝑘𝑁 → (𝜒𝜃))       (𝐴𝑁𝜏)

Theoremnntopi 7373* 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⟩ = 𝐴)

Theoremaxcaucvglemcl 7374* Lemma for axcaucvg 7379. 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)

Theoremaxcaucvglemf 7375* Lemma for axcaucvg 7379. 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⟩))       (𝜑𝐺:NR)

Theoremaxcaucvglemval 7376* Lemma for axcaucvg 7379. 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⟩)

Theoremaxcaucvglemcau 7377* Lemma for axcaucvg 7379. 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 ))))

Theoremaxcaucvglemres 7378* Lemma for axcaucvg 7379. 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 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))

Theoremaxcaucvg 7379* 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 7409. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)

𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))

3.1.3  Real and complex number postulates restated as axioms

Axiomax-cnex 7380 The complex numbers form a set. Proofs should normally use cnex 7410 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
ℂ ∈ V

Axiomax-resscn 7381 The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7341. (Contributed by NM, 1-Mar-1995.)
ℝ ⊆ ℂ

Axiomax-1cn 7382 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7342. (Contributed by NM, 1-Mar-1995.)
1 ∈ ℂ

Axiomax-1re 7383 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7343. Proofs should use 1re 7431 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
1 ∈ ℝ

Axiomax-icn 7384 i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7344. (Contributed by NM, 1-Mar-1995.)
i ∈ ℂ

Axiomax-addcl 7385 Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7345. Proofs should normally use addcl 7411 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Axiomax-addrcl 7386 Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7346. Proofs should normally use readdcl 7412 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Axiomax-mulcl 7387 Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7347. Proofs should normally use mulcl 7413 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Axiomax-mulrcl 7388 Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7348. Proofs should normally use remulcl 7414 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Axiomax-addcom 7389 Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7349. Proofs should normally use addcom 7563 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Axiomax-mulcom 7390 Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7350. Proofs should normally use mulcom 7415 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Axiomax-addass 7391 Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7351. Proofs should normally use addass 7416 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Axiomax-mulass 7392 Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7352. Proofs should normally use mulass 7417 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Axiomax-distr 7393 Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7353. Proofs should normally use adddi 7418 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Axiomax-i2m1 7394 i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7354. (Contributed by NM, 29-Jan-1995.)
((i · i) + 1) = 0

Axiomax-0lt1 7395 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7355. Proofs should normally use 0lt1 7554 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
0 < 1

Axiomax-1rid 7396 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7356. (Contributed by NM, 29-Jan-1995.)
(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Axiomax-0id 7397 0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 7357.

Proofs should normally use addid1 7564 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Axiomax-rnegex 7398* Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7358. (Contributed by Eric Schmidt, 21-May-2007.)
(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)

Axiomax-precex 7399* Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7359. (Contributed by Jim Kingdon, 6-Feb-2020.)
((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))

Axiomax-cnre 7400* 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 7360. For naming consistency, use cnre 7428 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11363
 Copyright terms: Public domain < Previous  Next >