HomeHome Intuitionistic Logic Explorer
Theorem List (p. 80 of 152)
< 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 - 7901-8000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremrereceu 7901* The reciprocal from axprecex 7892 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) β†’ βˆƒ!π‘₯ ∈ ℝ (𝐴 Β· π‘₯) = 1)
 
Theoremrecriota 7902* Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.)
(𝑁 ∈ N β†’ (β„©π‘Ÿ ∈ ℝ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [βŸ¨π‘, 1o⟩] ~Q }, {𝑒 ∣ [βŸ¨π‘, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩ Β· π‘Ÿ) = 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q (*Qβ€˜[βŸ¨π‘, 1o⟩] ~Q )}, {𝑒 ∣ (*Qβ€˜[βŸ¨π‘, 1o⟩] ~Q ) <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
 
Theoremaxarch 7903* 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 8934 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 7943. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)

(𝐴 ∈ ℝ β†’ βˆƒπ‘› ∈ ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}𝐴 <ℝ 𝑛)
 
Theorempeano5nnnn 7904* Peano's inductive postulate. This is a counterpart to peano5nni 8935 designed for real number axioms which involve natural numbers (notably, axcaucvg 7912). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    β‡’   ((1 ∈ 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) β†’ 𝑁 βŠ† 𝐴)
 
Theoremnnindnn 7905* Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8948 designed for real number axioms which involve natural numbers (notably, axcaucvg 7912). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (𝑧 = 1 β†’ (πœ‘ ↔ πœ“))    &   (𝑧 = π‘˜ β†’ (πœ‘ ↔ πœ’))    &   (𝑧 = (π‘˜ + 1) β†’ (πœ‘ ↔ πœƒ))    &   (𝑧 = 𝐴 β†’ (πœ‘ ↔ 𝜏))    &   πœ“    &   (π‘˜ ∈ 𝑁 β†’ (πœ’ β†’ πœƒ))    β‡’   (𝐴 ∈ 𝑁 β†’ 𝜏)
 
Theoremnntopi 7906* Mapping from β„• to N. (Contributed by Jim Kingdon, 13-Jul-2021.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    β‡’   (𝐴 ∈ 𝑁 β†’ βˆƒπ‘§ ∈ N ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [βŸ¨π‘§, 1o⟩] ~Q }, {𝑒 ∣ [βŸ¨π‘§, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 𝐴)
 
Theoremaxcaucvglemcl 7907* Lemma for axcaucvg 7912. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    β‡’   ((πœ‘ ∧ 𝐽 ∈ N) β†’ (℩𝑧 ∈ R (πΉβ€˜βŸ¨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑒 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = βŸ¨π‘§, 0R⟩) ∈ R)
 
Theoremaxcaucvglemf 7908* Lemma for axcaucvg 7912. Mapping to N and R yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    &   πΊ = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (πΉβ€˜βŸ¨[⟨(⟨{𝑙 ∣ 𝑙 <Q [βŸ¨π‘—, 1o⟩] ~Q }, {𝑒 ∣ [βŸ¨π‘—, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = βŸ¨π‘§, 0R⟩))    β‡’   (πœ‘ β†’ 𝐺:N⟢R)
 
Theoremaxcaucvglemval 7909* Lemma for axcaucvg 7912. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    &   πΊ = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (πΉβ€˜βŸ¨[⟨(⟨{𝑙 ∣ 𝑙 <Q [βŸ¨π‘—, 1o⟩] ~Q }, {𝑒 ∣ [βŸ¨π‘—, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = βŸ¨π‘§, 0R⟩))    β‡’   ((πœ‘ ∧ 𝐽 ∈ N) β†’ (πΉβ€˜βŸ¨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑒 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(πΊβ€˜π½), 0R⟩)
 
Theoremaxcaucvglemcau 7910* Lemma for axcaucvg 7912. The result of mapping to N and R satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    &   πΊ = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (πΉβ€˜βŸ¨[⟨(⟨{𝑙 ∣ 𝑙 <Q [βŸ¨π‘—, 1o⟩] ~Q }, {𝑒 ∣ [βŸ¨π‘—, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = βŸ¨π‘§, 0R⟩))    β‡’   (πœ‘ β†’ βˆ€π‘› ∈ N βˆ€π‘˜ ∈ N (𝑛 <N π‘˜ β†’ ((πΊβ€˜π‘›) <R ((πΊβ€˜π‘˜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Qβ€˜[βŸ¨π‘›, 1o⟩] ~Q )}, {𝑒 ∣ (*Qβ€˜[βŸ¨π‘›, 1o⟩] ~Q ) <Q 𝑒}⟩ +P 1P), 1P⟩] ~R ) ∧ (πΊβ€˜π‘˜) <R ((πΊβ€˜π‘›) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Qβ€˜[βŸ¨π‘›, 1o⟩] ~Q )}, {𝑒 ∣ (*Qβ€˜[βŸ¨π‘›, 1o⟩] ~Q ) <Q 𝑒}⟩ +P 1P), 1P⟩] ~R ))))
 
Theoremaxcaucvglemres 7911* Lemma for axcaucvg 7912. Mapping the limit from N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    &   πΊ = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (πΉβ€˜βŸ¨[⟨(⟨{𝑙 ∣ 𝑙 <Q [βŸ¨π‘—, 1o⟩] ~Q }, {𝑒 ∣ [βŸ¨π‘—, 1o⟩] ~Q <Q 𝑒}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = βŸ¨π‘§, 0R⟩))    β‡’   (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))))
 
Theoremaxcaucvg 7912* 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 7944. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)

𝑁 = ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}    &   (πœ‘ β†’ 𝐹:π‘βŸΆβ„)    &   (πœ‘ β†’ βˆ€π‘› ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑛 <ℝ π‘˜ β†’ ((πΉβ€˜π‘›) <ℝ ((πΉβ€˜π‘˜) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)) ∧ (πΉβ€˜π‘˜) <ℝ ((πΉβ€˜π‘›) + (β„©π‘Ÿ ∈ ℝ (𝑛 Β· π‘Ÿ) = 1)))))    β‡’   (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ ℝ (0 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))))
 
Theoremaxpre-suploclemres 7913* Lemma for axpre-suploc 7914. The result. The proof just needs to define 𝐡 as basically the same set as 𝐴 (but expressed as a subset of R rather than a subset of ℝ), and apply suplocsr 7821. (Contributed by Jim Kingdon, 24-Jan-2024.)
(πœ‘ β†’ 𝐴 βŠ† ℝ)    &   (πœ‘ β†’ 𝐢 ∈ 𝐴)    &   (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 <ℝ π‘₯)    &   (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ <ℝ 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ <ℝ 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 <ℝ 𝑦)))    &   π΅ = {𝑀 ∈ R ∣ βŸ¨π‘€, 0R⟩ ∈ 𝐴}    β‡’   (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <ℝ 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 <ℝ π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 <ℝ 𝑧)))
 
Theoremaxpre-suploc 7914* An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given π‘₯ < 𝑦, either there is an element of the set greater than π‘₯, or 𝑦 is an upper bound.

This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7945. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)

(((𝐴 βŠ† ℝ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴) ∧ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 <ℝ π‘₯ ∧ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ <ℝ 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ <ℝ 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 <ℝ 𝑦)))) β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <ℝ 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 <ℝ π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 <ℝ 𝑧)))
 
4.1.3  Real and complex number postulates restated as axioms
 
Axiomax-cnex 7915 The complex numbers form a set. Proofs should normally use cnex 7948 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
β„‚ ∈ V
 
Axiomax-resscn 7916 The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7872. (Contributed by NM, 1-Mar-1995.)
ℝ βŠ† β„‚
 
Axiomax-1cn 7917 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7873. (Contributed by NM, 1-Mar-1995.)
1 ∈ β„‚
 
Axiomax-1re 7918 1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7874. Proofs should use 1re 7969 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
1 ∈ ℝ
 
Axiomax-icn 7919 i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7875. (Contributed by NM, 1-Mar-1995.)
i ∈ β„‚
 
Axiomax-addcl 7920 Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 7876. Proofs should normally use addcl 7949 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 7921 Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 7877. Proofs should normally use readdcl 7950 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 + 𝐡) ∈ ℝ)
 
Axiomax-mulcl 7922 Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 7878. Proofs should normally use mulcl 7951 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) ∈ β„‚)
 
Axiomax-mulrcl 7923 Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 7879. Proofs should normally use remulcl 7952 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 Β· 𝐡) ∈ ℝ)
 
Axiomax-addcom 7924 Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 7882. Proofs should normally use addcom 8107 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 + 𝐡) = (𝐡 + 𝐴))
 
Axiomax-mulcom 7925 Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 7883. Proofs should normally use mulcom 7953 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) = (𝐡 Β· 𝐴))
 
Axiomax-addass 7926 Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 7884. Proofs should normally use addass 7954 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 + 𝐡) + 𝐢) = (𝐴 + (𝐡 + 𝐢)))
 
Axiomax-mulass 7927 Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 7885. Proofs should normally use mulass 7955 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 Β· 𝐡) Β· 𝐢) = (𝐴 Β· (𝐡 Β· 𝐢)))
 
Axiomax-distr 7928 Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7886. Proofs should normally use adddi 7956 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝐴 Β· (𝐡 + 𝐢)) = ((𝐴 Β· 𝐡) + (𝐴 Β· 𝐢)))
 
Axiomax-i2m1 7929 i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 7887. (Contributed by NM, 29-Jan-1995.)
((i Β· i) + 1) = 0
 
Axiomax-0lt1 7930 0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 7888. Proofs should normally use 0lt1 8097 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
0 <ℝ 1
 
Axiomax-1rid 7931 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7889. (Contributed by NM, 29-Jan-1995.)
(𝐴 ∈ ℝ β†’ (𝐴 Β· 1) = 𝐴)
 
Axiomax-0id 7932 0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 7890.

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

(𝐴 ∈ β„‚ β†’ (𝐴 + 0) = 𝐴)
 
Axiomax-rnegex 7933* Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7891. (Contributed by Eric Schmidt, 21-May-2007.)
(𝐴 ∈ ℝ β†’ βˆƒπ‘₯ ∈ ℝ (𝐴 + π‘₯) = 0)
 
Axiomax-precex 7934* Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 7892. (Contributed by Jim Kingdon, 6-Feb-2020.)
((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) β†’ βˆƒπ‘₯ ∈ ℝ (0 <ℝ π‘₯ ∧ (𝐴 Β· π‘₯) = 1))
 
Axiomax-cnre 7935* 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 7893. For naming consistency, use cnre 7966 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
(𝐴 ∈ β„‚ β†’ βˆƒπ‘₯ ∈ ℝ βˆƒπ‘¦ ∈ ℝ 𝐴 = (π‘₯ + (i Β· 𝑦)))
 
Axiomax-pre-ltirr 7936 Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7936. (Contributed by Jim Kingdon, 12-Jan-2020.)
(𝐴 ∈ ℝ β†’ Β¬ 𝐴 <ℝ 𝐴)
 
Axiomax-pre-ltwlin 7937 Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 7895. (Contributed by Jim Kingdon, 12-Jan-2020.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴 <ℝ 𝐡 β†’ (𝐴 <ℝ 𝐢 ∨ 𝐢 <ℝ 𝐡)))
 
Axiomax-pre-lttrn 7938 Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 7896. (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((𝐴 <ℝ 𝐡 ∧ 𝐡 <ℝ 𝐢) β†’ 𝐴 <ℝ 𝐢))
 
Axiomax-pre-apti 7939 Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 7897. (Contributed by Jim Kingdon, 29-Jan-2020.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ Β¬ (𝐴 <ℝ 𝐡 ∨ 𝐡 <ℝ 𝐴)) β†’ 𝐴 = 𝐡)
 
Axiomax-pre-ltadd 7940 Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 7898. (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐴 <ℝ 𝐡 β†’ (𝐢 + 𝐴) <ℝ (𝐢 + 𝐡)))
 
Axiomax-pre-mulgt0 7941 The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 7899. (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐡) β†’ 0 <ℝ (𝐴 Β· 𝐡)))
 
Axiomax-pre-mulext 7942 Strong extensionality of multiplication (expressed in terms of <ℝ). Axiom for real and complex numbers, justified by Theorem axpre-mulext 7900

(Contributed by Jim Kingdon, 18-Feb-2020.)

((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ ((𝐴 Β· 𝐢) <ℝ (𝐡 Β· 𝐢) β†’ (𝐴 <ℝ 𝐡 ∨ 𝐡 <ℝ 𝐴)))
 
Axiomax-arch 7943* Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 7903.

This axiom should not be used directly; instead use arch 9186 (which is the same, but stated in terms of β„• and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)

(𝐴 ∈ ℝ β†’ βˆƒπ‘› ∈ ∩ {π‘₯ ∣ (1 ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ (𝑦 + 1) ∈ π‘₯)}𝐴 <ℝ 𝑛)
 
Axiomax-caucvg 7944* Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7912.

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 11003 (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 <ℝ π‘₯ β†’ βˆƒπ‘— ∈ 𝑁 βˆ€π‘˜ ∈ 𝑁 (𝑗 <ℝ π‘˜ β†’ ((πΉβ€˜π‘˜) <ℝ (𝑦 + π‘₯) ∧ 𝑦 <ℝ ((πΉβ€˜π‘˜) + π‘₯)))))
 
Axiomax-pre-suploc 7945* An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given π‘₯ < 𝑦, either there is an element of the set greater than π‘₯, or 𝑦 is an upper bound.

Although this and ax-caucvg 7944 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7944.

(Contributed by Jim Kingdon, 23-Jan-2024.)

(((𝐴 βŠ† ℝ ∧ βˆƒπ‘₯ π‘₯ ∈ 𝐴) ∧ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ 𝐴 𝑦 <ℝ π‘₯ ∧ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ <ℝ 𝑦 β†’ (βˆƒπ‘§ ∈ 𝐴 π‘₯ <ℝ 𝑧 ∨ βˆ€π‘§ ∈ 𝐴 𝑧 <ℝ 𝑦)))) β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <ℝ 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 <ℝ π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 <ℝ 𝑧)))
 
Axiomax-addf 7946 Addition is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see https://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific addcl 7949 should be used. Note that uses of ax-addf 7946 can be eliminated by using the defined operation (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ + 𝑦)) in place of +, from which this axiom (with the defined operation in place of +) follows as a theorem.

This axiom is justified by Theorem axaddf 7880. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

+ :(β„‚ Γ— β„‚)βŸΆβ„‚
 
Axiomax-mulf 7947 Multiplication is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see https://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific ax-mulcl 7922 should be used. Note that uses of ax-mulf 7947 can be eliminated by using the defined operation (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) in place of Β·, from which this axiom (with the defined operation in place of Β·) follows as a theorem.

This axiom is justified by Theorem axmulf 7881. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

Β· :(β„‚ Γ— β„‚)βŸΆβ„‚
 
4.2  Derive the basic properties from the field axioms
 
4.2.1  Some deductions from the field axioms for complex numbers
 
Theoremcnex 7948 Alias for ax-cnex 7915. (Contributed by Mario Carneiro, 17-Nov-2014.)
β„‚ ∈ V
 
Theoremaddcl 7949 Alias for ax-addcl 7920, for naming consistency with addcli 7974. Use this theorem instead of ax-addcl 7920 or axaddcl 7876. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 + 𝐡) ∈ β„‚)
 
Theoremreaddcl 7950 Alias for ax-addrcl 7921, for naming consistency with readdcli 7983. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 + 𝐡) ∈ ℝ)
 
Theoremmulcl 7951 Alias for ax-mulcl 7922, for naming consistency with mulcli 7975. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) ∈ β„‚)
 
Theoremremulcl 7952 Alias for ax-mulrcl 7923, for naming consistency with remulcli 7984. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴 Β· 𝐡) ∈ ℝ)
 
Theoremmulcom 7953 Alias for ax-mulcom 7925, for naming consistency with mulcomi 7976. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (𝐴 Β· 𝐡) = (𝐡 Β· 𝐴))
 
Theoremaddass 7954 Alias for ax-addass 7926, for naming consistency with addassi 7978. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 + 𝐡) + 𝐢) = (𝐴 + (𝐡 + 𝐢)))
 
Theoremmulass 7955 Alias for ax-mulass 7927, for naming consistency with mulassi 7979. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 Β· 𝐡) Β· 𝐢) = (𝐴 Β· (𝐡 Β· 𝐢)))
 
Theoremadddi 7956 Alias for ax-distr 7928, for naming consistency with adddii 7980. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝐴 Β· (𝐡 + 𝐢)) = ((𝐴 Β· 𝐡) + (𝐴 Β· 𝐢)))
 
Theoremrecn 7957 A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
(𝐴 ∈ ℝ β†’ 𝐴 ∈ β„‚)
 
Theoremreex 7958 The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℝ ∈ V
 
Theoremreelprrecn 7959 Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
ℝ ∈ {ℝ, β„‚}
 
Theoremcnelprrecn 7960 Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
β„‚ ∈ {ℝ, β„‚}
 
Theoremadddir 7961 Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐴 + 𝐡) Β· 𝐢) = ((𝐴 Β· 𝐢) + (𝐡 Β· 𝐢)))
 
Theorem0cn 7962 0 is a complex number. (Contributed by NM, 19-Feb-2005.)
0 ∈ β„‚
 
Theorem0cnd 7963 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
(πœ‘ β†’ 0 ∈ β„‚)
 
Theoremc0ex 7964 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
0 ∈ V
 
Theorem1ex 7965 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
1 ∈ V
 
Theoremcnre 7966* Alias for ax-cnre 7935, for naming consistency. (Contributed by NM, 3-Jan-2013.)
(𝐴 ∈ β„‚ β†’ βˆƒπ‘₯ ∈ ℝ βˆƒπ‘¦ ∈ ℝ 𝐴 = (π‘₯ + (i Β· 𝑦)))
 
Theoremmulrid 7967 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
(𝐴 ∈ β„‚ β†’ (𝐴 Β· 1) = 𝐴)
 
Theoremmullid 7968 Identity law for multiplication. Note: see mulrid 7967 for commuted version. (Contributed by NM, 8-Oct-1999.)
(𝐴 ∈ β„‚ β†’ (1 Β· 𝐴) = 𝐴)
 
Theorem1re 7969 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1 ∈ ℝ
 
Theorem0re 7970 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
0 ∈ ℝ
 
Theorem0red 7971 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
(πœ‘ β†’ 0 ∈ ℝ)
 
Theoremmulid1i 7972 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
𝐴 ∈ β„‚    β‡’   (𝐴 Β· 1) = 𝐴
 
Theoremmullidi 7973 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
𝐴 ∈ β„‚    β‡’   (1 Β· 𝐴) = 𝐴
 
Theoremaddcli 7974 Closure law for addition. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   (𝐴 + 𝐡) ∈ β„‚
 
Theoremmulcli 7975 Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   (𝐴 Β· 𝐡) ∈ β„‚
 
Theoremmulcomi 7976 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   (𝐴 Β· 𝐡) = (𝐡 Β· 𝐴)
 
Theoremmulcomli 7977 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    &   (𝐴 Β· 𝐡) = 𝐢    β‡’   (𝐡 Β· 𝐴) = 𝐢
 
Theoremaddassi 7978 Associative law for addition. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    &   πΆ ∈ β„‚    β‡’   ((𝐴 + 𝐡) + 𝐢) = (𝐴 + (𝐡 + 𝐢))
 
Theoremmulassi 7979 Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    &   πΆ ∈ β„‚    β‡’   ((𝐴 Β· 𝐡) Β· 𝐢) = (𝐴 Β· (𝐡 Β· 𝐢))
 
Theoremadddii 7980 Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    &   πΆ ∈ β„‚    β‡’   (𝐴 Β· (𝐡 + 𝐢)) = ((𝐴 Β· 𝐡) + (𝐴 Β· 𝐢))
 
Theoremadddiri 7981 Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    &   πΆ ∈ β„‚    β‡’   ((𝐴 + 𝐡) Β· 𝐢) = ((𝐴 Β· 𝐢) + (𝐡 Β· 𝐢))
 
Theoremrecni 7982 A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
𝐴 ∈ ℝ    β‡’   π΄ ∈ β„‚
 
Theoremreaddcli 7983 Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
𝐴 ∈ ℝ    &   π΅ ∈ ℝ    β‡’   (𝐴 + 𝐡) ∈ ℝ
 
Theoremremulcli 7984 Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
𝐴 ∈ ℝ    &   π΅ ∈ ℝ    β‡’   (𝐴 Β· 𝐡) ∈ ℝ
 
Theorem1red 7985 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(πœ‘ β†’ 1 ∈ ℝ)
 
Theorem1cnd 7986 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(πœ‘ β†’ 1 ∈ β„‚)
 
Theoremmulridd 7987 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴 Β· 1) = 𝐴)
 
Theoremmullidd 7988 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (1 Β· 𝐴) = 𝐴)
 
Theoremmulid2d 7989 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (1 Β· 𝐴) = 𝐴)
 
Theoremaddcld 7990 Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴 + 𝐡) ∈ β„‚)
 
Theoremmulcld 7991 Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴 Β· 𝐡) ∈ β„‚)
 
Theoremmulcomd 7992 Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴 Β· 𝐡) = (𝐡 Β· 𝐴))
 
Theoremaddassd 7993 Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐢 ∈ β„‚)    β‡’   (πœ‘ β†’ ((𝐴 + 𝐡) + 𝐢) = (𝐴 + (𝐡 + 𝐢)))
 
Theoremmulassd 7994 Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐢 ∈ β„‚)    β‡’   (πœ‘ β†’ ((𝐴 Β· 𝐡) Β· 𝐢) = (𝐴 Β· (𝐡 Β· 𝐢)))
 
Theoremadddid 7995 Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐢 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴 Β· (𝐡 + 𝐢)) = ((𝐴 Β· 𝐡) + (𝐴 Β· 𝐢)))
 
Theoremadddird 7996 Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐢 ∈ β„‚)    β‡’   (πœ‘ β†’ ((𝐴 + 𝐡) Β· 𝐢) = ((𝐴 Β· 𝐢) + (𝐡 Β· 𝐢)))
 
Theoremadddirp1d 7997 Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    β‡’   (πœ‘ β†’ ((𝐴 + 1) Β· 𝐡) = ((𝐴 Β· 𝐡) + 𝐡))
 
Theoremjoinlmuladdmuld 7998 Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐢 ∈ β„‚)    &   (πœ‘ β†’ ((𝐴 Β· 𝐡) + (𝐢 Β· 𝐡)) = 𝐷)    β‡’   (πœ‘ β†’ ((𝐴 + 𝐢) Β· 𝐡) = 𝐷)
 
Theoremrecnd 7999 Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    β‡’   (πœ‘ β†’ 𝐴 ∈ β„‚)
 
Theoremreaddcld 8000 Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝐡 ∈ ℝ)    β‡’   (πœ‘ β†’ (𝐴 + 𝐡) ∈ ℝ)
    < Previous  Next >

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-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15104
  Copyright terms: Public domain < Previous  Next >