P. 72 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axpre-lttrn 7101	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 7141. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Theorem	axpre-apti 7102	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 7142. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
Theorem	axpre-ltadd 7103	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 7143. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Theorem	axpre-mulgt0 7104	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 7144. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Theorem	axpre-mulext 7105	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 7145. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Theorem	rereceu 7106*	The reciprocal from axprecex 7097 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Theorem	recriota 7107*	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 7108*	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 8097 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 7146. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
Theorem	peano5nnnn 7109*	Peano's inductive postulate. This is a counterpart to peano5nni 8098 designed for real number axioms which involve natural numbers (notably, axcaucvg 7117). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ ((1 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴)
Theorem	nnindnn 7110*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8111 designed for real number axioms which involve natural numbers (notably, axcaucvg 7117). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝑧 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ 𝑁 → 𝜏)
Theorem	nntopi 7111*	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 7112*	Lemma for axcaucvg 7117. 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 7113*	Lemma for axcaucvg 7117. 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 7114*	Lemma for axcaucvg 7117. 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 7115*	Lemma for axcaucvg 7117. 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 7116*	Lemma for axcaucvg 7117. 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 7117*	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 7147. (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
Axiom	ax-cnex 7118	The complex numbers form a set. Proofs should normally use cnex 7148 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
⊢ ℂ ∈ V
Axiom	ax-resscn 7119	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7079. (Contributed by NM, 1-Mar-1995.)
⊢ ℝ ⊆ ℂ
Axiom	ax-1cn 7120	1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7080. (Contributed by NM, 1-Mar-1995.)
⊢ 1 ∈ ℂ
Axiom	ax-1re 7121	1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7081. Proofs should use 1re 7169 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
⊢ 1 ∈ ℝ
Axiom	ax-icn 7122	i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7082. (Contributed by NM, 1-Mar-1995.)
⊢ i ∈ ℂ
Axiom	ax-addcl 7123	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7083. Proofs should normally use addcl 7149 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 7124	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7084. Proofs should normally use readdcl 7150 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Axiom	ax-mulcl 7125	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7085. Proofs should normally use mulcl 7151 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Axiom	ax-mulrcl 7126	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7086. Proofs should normally use remulcl 7152 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Axiom	ax-addcom 7127	Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7087. Proofs should normally use addcom 7301 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Axiom	ax-mulcom 7128	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7088. Proofs should normally use mulcom 7153 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Axiom	ax-addass 7129	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7089. Proofs should normally use addass 7154 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Axiom	ax-mulass 7130	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7090. Proofs should normally use mulass 7155 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Axiom	ax-distr 7131	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7091. Proofs should normally use adddi 7156 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Axiom	ax-i2m1 7132	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7092. (Contributed by NM, 29-Jan-1995.)
⊢ ((i · i) + 1) = 0
Axiom	ax-0lt1 7133	0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7093. Proofs should normally use 0lt1 7292 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ 0 <ℝ 1
Axiom	ax-1rid 7134	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7094. (Contributed by NM, 29-Jan-1995.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Axiom	ax-0id 7135	0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 7095. Proofs should normally use addid1 7302 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Axiom	ax-rnegex 7136*	Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7096. (Contributed by Eric Schmidt, 21-May-2007.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Axiom	ax-precex 7137*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7097. (Contributed by Jim Kingdon, 6-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1))
Axiom	ax-cnre 7138*	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 7098. For naming consistency, use cnre 7166 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Axiom	ax-pre-ltirr 7139	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7139. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
Axiom	ax-pre-ltwlin 7140	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7100. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
Axiom	ax-pre-lttrn 7141	Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7101. (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Axiom	ax-pre-apti 7142	Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7102. (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
Axiom	ax-pre-ltadd 7143	Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7103. (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Axiom	ax-pre-mulgt0 7144	The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7104. (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Axiom	ax-pre-mulext 7145	Strong extensionality of multiplication (expressed in terms of <ℝ). Axiom for real and complex numbers, justified by theorem axpre-mulext 7105 (Contributed by Jim Kingdon, 18-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Axiom	ax-arch 7146*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 7108. This axiom should not be used directly; instead use arch 8341 (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 7147*	Completeness. Axiom for real and complex numbers, justified by theorem axcaucvg 7117. 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 9994 (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 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
3.2  Derive the basic properties from the field axioms
3.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 7148	Alias for ax-cnex 7118. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℂ ∈ V
Theorem	addcl 7149	Alias for ax-addcl 7123, for naming consistency with addcli 7174. Use this theorem instead of ax-addcl 7123 or axaddcl 7083. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	readdcl 7150	Alias for ax-addrcl 7124, for naming consistency with readdcli 7183. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	mulcl 7151	Alias for ax-mulcl 7125, for naming consistency with mulcli 7175. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	remulcl 7152	Alias for ax-mulrcl 7126, for naming consistency with remulcli 7184. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 7153	Alias for ax-mulcom 7128, for naming consistency with mulcomi 7176. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 7154	Alias for ax-addass 7129, for naming consistency with addassi 7178. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 7155	Alias for ax-mulass 7130, for naming consistency with mulassi 7179. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 7156	Alias for ax-distr 7131, for naming consistency with adddii 7180. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 7157	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 7158	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 7159	Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 7160	Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	adddir 7161	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 7162	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ
Theorem	0cnd 7163	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℂ)
Theorem	c0ex 7164	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ∈ V
Theorem	1ex 7165	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 1 ∈ V
Theorem	cnre 7166*	Alias for ax-cnre 7138, for naming consistency. (Contributed by NM, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	mulid1 7167	1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Theorem	mulid2 7168	Identity law for multiplication. Note: see mulid1 7167 for commuted version. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	1re 7169	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
⊢ 1 ∈ ℝ
Theorem	0re 7170	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 0 ∈ ℝ
Theorem	0red 7171	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℝ)
Theorem	mulid1i 7172	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 1) = 𝐴
Theorem	mulid2i 7173	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (1 · 𝐴) = 𝐴
Theorem	addcli 7174	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℂ
Theorem	mulcli 7175	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℂ
Theorem	mulcomi 7176	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	mulcomli 7177	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (𝐵 · 𝐴) = 𝐶
Theorem	addassi 7178	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	mulassi 7179	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	adddii 7180	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Theorem	adddiri 7181	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
Theorem	recni 7182	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	readdcli 7183	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℝ
Theorem	remulcli 7184	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℝ
Theorem	1red 7185	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℝ)
Theorem	1cnd 7186	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℂ)
Theorem	mulid1d 7187	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐴)
Theorem	mulid2d 7188	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	addcld 7189	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Theorem	mulcld 7190	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Theorem	mulcomd 7191	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addassd 7192	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulassd 7193	Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddid 7194	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	adddird 7195	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	adddirp1d 7196	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Theorem	joinlmuladdmuld 7197	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
Theorem	recnd 7198	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	readdcld 7199	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Theorem	remulcld 7200	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)