Home | Metamath
Proof Explorer Theorem List (p. 332 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-elccinfty 33101 | A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
inftyexpi CCinfty | ||
Syntax | cccbar 33102 | Syntax for the set of extended complex numbers CCbar. |
CCbar | ||
Definition | df-bj-ccbar 33103 | Definition of the set of extended complex numbers CCbar. (Contributed by BJ, 22-Jun-2019.) |
CCbar CCinfty | ||
Theorem | bj-ccssccbar 33104 | Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
CCbar | ||
Theorem | bj-ccinftyssccbar 33105 | Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
CCinfty CCbar | ||
Syntax | cpinfty 33106 | Syntax for pinfty. |
pinfty | ||
Definition | df-bj-pinfty 33107 | Definition of pinfty. (Contributed by BJ, 27-Jun-2019.) |
pinfty inftyexpi | ||
Theorem | bj-pinftyccb 33108 | The class pinfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
pinfty CCbar | ||
Theorem | bj-pinftynrr 33109 | The extended complex number pinfty is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
pinfty | ||
Syntax | cminfty 33110 | Syntax for minfty. |
minfty | ||
Definition | df-bj-minfty 33111 | Definition of minfty. (Contributed by BJ, 27-Jun-2019.) |
minfty inftyexpi | ||
Theorem | bj-minftyccb 33112 | The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
minfty CCbar | ||
Theorem | bj-minftynrr 33113 | The extended complex number minfty is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
minfty | ||
Theorem | bj-pinftynminfty 33114 | The extended complex numbers pinfty and minfty are different. (Contributed by BJ, 27-Jun-2019.) |
pinfty minfty | ||
Syntax | crrbar 33115 | Syntax for the set of extended real numbers RRbar. |
RRbar | ||
Definition | df-bj-rrbar 33116 | Definition of the set of extended real numbers RRbar. See df-xr 10078. (Contributed by BJ, 29-Jun-2019.) |
RRbar minfty pinfty | ||
Syntax | cinfty 33117 | Syntax for infty. |
infty | ||
Definition | df-bj-infty 33118 | Definition of infty, the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
infty | ||
Syntax | ccchat 33119 | Syntax for CChat. |
CChat | ||
Definition | df-bj-cchat 33120 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
CChat infty | ||
Syntax | crrhat 33121 | Syntax for RRhat. |
RRhat | ||
Definition | df-bj-rrhat 33122 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
RRhat infty | ||
Theorem | bj-rrhatsscchat 33123 | The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.) |
RRhat CChat | ||
We define the operations on the extended real and complex numbers and on the real and complex projective lines simultaneously, thus "overloading" the operations. | ||
Syntax | caddcc 33124 | Syntax for the addition of extended complex numbers. |
+cc | ||
Definition | df-bj-addc 33125 | Define the additions on the extended complex numbers (on the subset of CCbar CCbar where it makes sense) and on the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.) |
+cc CCbar CCbar CChat CChat DiagCCinfty infty infty infty | ||
Syntax | coppcc 33126 | Syntax for the opposite of extended complex numbers. |
-cc | ||
Definition | df-bj-oppc 33127 | Define the negation (operation givin the opposite) the set of extended complex numbers and the complex projective line (Riemann sphere). One could use the prcpal function in the infinite case, but we want to use only basic functions at this point. (Contributed by BJ, 22-Jun-2019.) |
-cc CCbar CChat infty infty inftyexpi | ||
Since one needs arguments in order to define multiplication in CCbar, it seems harder to put this at the very beginning of the introduction of complex numbers. | ||
Syntax | cprcpal 33128 | Syntax for the function prcpal. |
prcpal | ||
Definition | df-bj-prcpal 33129 | Define the function prcpal. (Contributed by BJ, 22-Jun-2019.) |
prcpal | ||
Syntax | carg 33130 | Syntax for the argument of a nonzero extended complex number. |
Arg | ||
Definition | df-bj-arg 33131 | Define the argument of a nonzero extended complex number. By convention, it has values in . Another convention chooses but the present one simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.) |
Arg CCbar | ||
Syntax | cmulc 33132 | Syntax for the multiplication of extended complex numbers. |
.cc | ||
Definition | df-bj-mulc 33133 | Define the multiplication of extended complex numbers and of the complex projective line (Riemann sphere). In our convention, a product with 0 is 0, even when the other factor is infinite. An alternate convention leaves products of 0 with an infinite number undefined since the multiplication is not continuous at these points. Note that our convention entails . (Contributed by BJ, 22-Jun-2019.) |
.cc CCbar CCbar CChat CChat infty infty infty inftyexpi prcpalArg Arg | ||
Syntax | cinvc 33134 | Syntax for the inverse of nonzero extended complex numbers. |
invc | ||
Definition | df-bj-invc 33135 | Define inversion, which maps a nonzero extended complex number or element of the complex projective line (Riemann sphere) to its inverse. Beware of the overloading: the equality invc infty is to be understood in the complex projective line, but 0 as an extended complex number does not have an inverse, which we can state as invc CCbar. (Contributed by BJ, 22-Jun-2019.) |
invc CCbar CChat infty | ||
See ccmn 18193 and subsequents. The first few statements of this subsection can be put very early after ccmn 18193. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 18194 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-cmnssmnd 33136 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
CMnd | ||
Theorem | bj-cmnssmndel 33137 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 18208, which relies on iscmn 18200. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
CMnd | ||
Theorem | bj-ablssgrp 33138 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
Theorem | bj-ablssgrpel 33139 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 18198. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
Theorem | bj-ablsscmn 33140 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
CMnd | ||
Theorem | bj-ablsscmnel 33141 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 18199. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
CMnd | ||
Theorem | bj-modssabl 33142 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 18910; see also lmodgrp 18870 and lmodcmn 18911.) (Contributed by BJ, 9-Jun-2019.) |
Theorem | bj-vecssmod 33143 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
Theorem | bj-vecssmodel 33144 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 19106. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
UPDATE: a similar summation is already defined as df-gsum 16103 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 33145 | Syntax for the class "finite summation in monoids". |
FinSum | ||
Definition | df-bj-finsum 33146* | Finite summation in commutative monoids. This finite summation function can be extended to pairs where is a left-unital magma and is defined on a totally ordered set (choosing left-associative composition), or dropping unitality and requiring nonempty families, or on any monoids for families of permutable elements, etc. We use the term "summation", even though the definition stands for any unital, commutative and associative composition law. (Contributed by BJ, 9-Jun-2019.) |
FinSum CMnd | ||
Theorem | bj-finsumval0 33147* | Value of a finite sum. (Contributed by BJ, 9-Jun-2019.) (Proof shortened by AV, 5-May-2021.) |
CMnd FinSum | ||
A few basic theorems to start affine, Euclidean, and Cartesian geometry. | ||
A few basic definitions and theorems about convex hulls in real vector spaces. TODO: prove inclusion in the class of subcomplex vector spaces. | ||
Syntax | crrvec 33148 | Syntax for the class of real vector spaces. |
RR-Vec | ||
Definition | df-bj-rrvec 33149 | Definition of the class of real vector spaces. (Contributed by BJ, 9-Jun-2019.) |
RR-Vec Scalar RRfld | ||
Theorem | bj-rrvecssvec 33150 | Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.) |
RR-Vec | ||
Theorem | bj-rrvecssvecel 33151 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 9-Jun-2019.) |
RR-Vec | ||
Theorem | bj-rrvecsscmn 33152 | (The additive groups of) real vector spaces are commutative monoids. (Contributed by BJ, 9-Jun-2019.) |
RR-Vec CMnd | ||
Theorem | bj-rrvecsscmnel 33153 | (The additive groups of) real vector spaces are commutative monoids (elemental version). (Contributed by BJ, 9-Jun-2019.) |
RR-Vec CMnd | ||
Some lemmas to ease algebraic manipulations. | ||
Theorem | bj-subcom 33154 | A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-ldiv 33155 | Left-division. (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-rdiv 33156 | Right-division. (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-mdiv 33157 | A division law. (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-lineq 33158 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-lineqi 33159 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
Lemmas about barycentric coordinates. For the moment, this is limited to the one-dimensional case (complex line), where existence and uniqueness of barycentric coordinates are proved by bj-bary1 33162 (which computes them). It would be nice to prove the two-dimensional case (is it easier to use ad hoc computations, or Cramer formulas?), in order to do some planar geometry. | ||
Theorem | bj-bary1lem 33160 | A lemma for barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-bary1lem1 33161 | Existence and uniqueness (and actual computation) of barycentric coordinates in dimension 1 (complex line). (Contributed by BJ, 6-Jun-2019.) |
Theorem | bj-bary1 33162 | Barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.) |
Syntax | ctau 33163 | Extend class notation to include tau = 6.283185.... |
Definition | df-tau 33164 | Define tau = 6.283185..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including , a three-legged variant of , or . Note the difference between this constant and the variable which is a variable representing a propositional logic formula. Only the latter is italic, and the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.) |
inf | ||
Theorem | taupilem3 33165 | Lemma for tau-related theorems . (Contributed by Jim Kingdon, 16-Feb-2019.) |
Theorem | taupilemrplb 33166* | A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.) |
Theorem | taupilem1 33167 | Lemma for taupi 33169. A positive real whose cosine is one is at least . (Contributed by Jim Kingdon, 19-Feb-2019.) |
Theorem | taupilem2 33168 | Lemma for taupi 33169. The smallest positive real whose cosine is one is at most . (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
Theorem | taupi 33169 | Relationship between and . This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
Theorem | dfgcd3 33170* | Alternate definition of the operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
Theorem | csbdif 33171 | Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.) |
Theorem | csbpredg 33172 | Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020.) |
Theorem | csbwrecsg 33173 | Move class substitution in and out of the well-founded recursive function generator . (Contributed by ML, 25-Oct-2020.) |
wrecs wrecs | ||
Theorem | csbrecsg 33174 | Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.) |
recs recs | ||
Theorem | csbrdgg 33175 | Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.) |
Theorem | csboprabg 33176* | Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.) |
Theorem | csbmpt22g 33177* | Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.) |
Theorem | mpnanrd 33178 | Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.) |
Theorem | con1bii2 33179 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
Theorem | con2bii2 33180 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
Theorem | vtoclefex 33181* | Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.) |
Theorem | rnmptsn 33182* | The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.) |
Theorem | f1omptsnlem 33183* | This is the core of the proof of f1omptsn 33184, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.) |
Theorem | f1omptsn 33184* | A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.) |
Theorem | mptsnunlem 33185* | This is the core of the proof of mptsnun 33186, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
Theorem | mptsnun 33186* | A class is equal to the union of the class of all singletons of elements of . (Contributed by ML, 16-Jul-2020.) |
Theorem | dissneqlem 33187* | This is the core of the proof of dissneq 33188, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
TopOn | ||
Theorem | dissneq 33188* | Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.) |
TopOn | ||
Theorem | exlimim 33189* | Closed form of exlimimd 33190. (Contributed by ML, 17-Jul-2020.) |
Theorem | exlimimd 33190* | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
Theorem | exlimimdd 33191 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
Theorem | exellim 33192* | Closed form of exellimddv 33193. See also exlimim 33189 for a more general theorem. (Contributed by ML, 17-Jul-2020.) |
Theorem | exellimddv 33193* | Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 33192 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.) |
Theorem | topdifinfindis 33194* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets of such that the complement of in is infinite, or is the empty set, or is all of , is the trivial topology when is finite. (Contributed by ML, 14-Jul-2020.) |
Theorem | topdifinffinlem 33195* | This is the core of the proof of topdifinffin 33196, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.) |
TopOn | ||
Theorem | topdifinffin 33196* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets of such that the complement of in is infinite, or is the empty set, or is all of , is a topology only if is finite. (Contributed by ML, 17-Jul-2020.) |
TopOn | ||
Theorem | topdifinf 33197* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets of such that the complement of in is infinite, or is the empty set, or is all of , is a topology if and only if is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020.) |
TopOn TopOn | ||
Theorem | topdifinfeq 33198* | Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.) |
Theorem | icorempt2 33199* | Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.) |
Theorem | icoreresf 33200 | Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |