Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 15-Oct-2017 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (4-Oct-2017) Alan Sare updated his completeusersproof program.
(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript.
(3-Oct-2017) Sean B. Palmer wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.
(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)
(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.
(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.
(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.
(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.
(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).
(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.
(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.
(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.
(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).
(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.
(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60. Older news...
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
14-Oct-2017 | cusgrauvtx 28168 | In a complete (undirected simple) graph, each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
ComplUSGrph UnivVertex | ||
14-Oct-2017 | uvtxnbgravtx 28167 | A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
USGrph UnivVertex Neighbors | ||
14-Oct-2017 | uvtxnm1nbgra 28166 | A universal vertex has neighbors in a graph with vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
USGrph UnivVertex Neighbors | ||
14-Oct-2017 | uvtxnbgra 28165 | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
USGrph UnivVertex Neighbors | ||
14-Oct-2017 | eqid 2283 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20: "Therefore, inquiring why a thing is itself, it's inquiring nothing; ... saying that the thing is itself constitutes the sole reasoning and the sole cause, in every case, to the question of why the man is man or the musician musician."). (Thanks to Stefan Allan and Benoit Jubin for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by Benoit Jubin, 14-Oct-2017.) |
13-Oct-2017 | cusgra1v 28157 | A graph with one vertex (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |
ComplUSGrph | ||
13-Oct-2017 | cusgra0v 28156 | A graph with no vertices (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |
ComplUSGrph | ||
13-Oct-2017 | cusisusgra 28155 | A complete (undirected simple) graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |
ComplUSGrph USGrph | ||
13-Oct-2017 | iscusgra0 28154 | The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |
ComplUSGrph USGrph | ||
13-Oct-2017 | usgra1v 28126 | A class with one (or no) vertex is a graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |
USGrph | ||
13-Oct-2017 | difprsng 28069 | Removal of a singleton from a (proper) unordered pair. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |
12-Oct-2017 | uvtx01vtx 28164 | If a graph/class has no edges, it has universal vertices if and only if it has at most one vertex. This theorem could have been stated UnivVertex , but a lot of auxiliary theorems would have been needed. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
UnivVertex | ||
12-Oct-2017 | uvtx0 28163 | There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
UnivVertex | ||
12-Oct-2017 | uvtxisvtx 28162 | A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
UnivVertex | ||
12-Oct-2017 | uvtxel 28161 | An element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
UnivVertex | ||
12-Oct-2017 | isuvtx 28160 | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
UnivVertex | ||
12-Oct-2017 | nbcusgra 28159 | In a complete (undirected simple) graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
ComplUSGrph Neighbors | ||
12-Oct-2017 | cusgra2v 28158 | A graph with two (different) vertices is complete if and only if there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph ComplUSGrph | ||
12-Oct-2017 | iscusgra 28153 | The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
ComplUSGrph USGrph | ||
12-Oct-2017 | nbgrasym 28152 | A vertex in a graph is a neighbor of a second vertex if and only if the second vertex is a neighbor of the first vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors Neighbors | ||
12-Oct-2017 | nbgranself2 28151 | A class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgrassovt 28150 | The neighbors of a vertex are a subset of the other vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgranself 28149 | A node in a graph (without loops!) is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgrassvt 28148 | The neighbors of a node in a graph are a subset of all nodes of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgra0edg 28147 | In a graph with no edges, every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgraisvtx 28146 | Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgra0nb 28144 | A vertex which is not endpoint of an edge has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
USGrph Neighbors | ||
12-Oct-2017 | nbgranv0 28142 | There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
Neighbors | ||
12-Oct-2017 | df-uvtx 28139 | Define the class of all universal vertices (in a graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph). (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
UnivVertex | ||
12-Oct-2017 | df-cusgra 28138 | Define the class of all complete (undirected simple) graphs. A undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
ComplUSGrph USGrph | ||
12-Oct-2017 | mpt2ndm0 28078 | The value of an operation given by a maps-to rule is the empty set if the arguments ar not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
12-Oct-2017 | repfuntw 25160 | Representation as a set of pairs of a function whose domain has two distinct elements. (Contributed by FL, 26-Jun-2011.) (Proof shortened by Scott Fenton, 12-Oct-2017.) |
11-Oct-2017 | nbgraeledg 28145 | A class/vertex is a neighbor of another class/vertex if and only if it is an endpoint of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
USGrph Neighbors | ||
11-Oct-2017 | mpt2xopoveqd 28087 | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
11-Oct-2017 | mpt2xopoveq 28085 | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
10-Oct-2017 | mpt2xopovel 28086 | Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.) |
10-Oct-2017 | mpt2xopynvov0 28084 | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
10-Oct-2017 | mpt2xopxprcov0 28083 | If the components of the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
10-Oct-2017 | mpt2xopx0ov0 28082 | If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
10-Oct-2017 | mpt2xopxnop0 28081 | If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
10-Oct-2017 | mpt2xopynvov0g 28080 | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
10-Oct-2017 | mpt2xopn0yelv 28079 | If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
9-Oct-2017 | nbusgra 28143 | The set of neighbors of a vertex in a graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) |
USGrph Neighbors | ||
9-Oct-2017 | nbgrael 28141 | The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) |
Neighbors | ||
8-Oct-2017 | rmo4f 23180 | Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
8-Oct-2017 | rmo3f 23178 | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
8-Oct-2017 | ssrmo 23148 | "At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
8-Oct-2017 | rmoxfrd 23147 | Transfer "at most one" restricted quantification from a variable to another variable contained in expression . (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
8-Oct-2017 | reuxfr3d 23138 | Transfer existential uniqueness from a variable to another variable contained in expression . Cf. reuxfr2d 4557 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
7-Oct-2017 | nbgraop 28140 | The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |
Neighbors | ||
7-Oct-2017 | df-nbgra 28137 | Define the class of all Neighbors of a vertex in a graph. The neighbors of a vertex are all vertices which are connected with this vertex by an edge. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) |
Neighbors | ||
7-Oct-2017 | usgraedgrnv 28123 | An edge of an undirected simple graph always connects to vertices. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |
USGrph | ||
7-Oct-2017 | elprchashprn2 28088 | If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |
7-Oct-2017 | eqri 23187 | Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.) |
7-Oct-2017 | brprcneu 5518 | If is a proper class, then there is no unique binary relationship with as the first element. (Contributed by Scott Fenton, 7-Oct-2017.) |
6-Oct-2017 | 1to3vfriendship 28186 | The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
FriendGrph | ||
6-Oct-2017 | 1to3vfriswmgra 28185 | Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
FriendGrph | ||
6-Oct-2017 | 1to2vfriswmgra 28184 | Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
FriendGrph | ||
6-Oct-2017 | 3vfriswmgra 28183 | Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
FriendGrph | ||
6-Oct-2017 | 3vfriswmgralem 28182 | Lemma for 3vfriswmgra 28183. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
USGrph | ||
6-Oct-2017 | tpprceq3 28072 | An unordered triple is an unordered pair if one of its elemets is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
6-Oct-2017 | tppreq3 28071 | An unordered triple is an unordered pair if one of its elemets is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
6-Oct-2017 | fveu 5517 | The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017.) |
6-Oct-2017 | df-fv 5263 | Define the value of a function, , also known as function application. For example, (we prove this in cos0 12430 after we define cosine in df-cos 12352). Typically function is defined using maps-to notation (see df-mpt 4079 and df-mpt2 5863), but this is not required. For example, (ex-fv 20830). Note that df-ov 5861 will define two-argument functions using ordered pairs as . This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv 5552 and fvprc 5519). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar notation for a function's value at , i.e. " of ," but without context-dependent notational ambiguity. Alternate definitions are dffv2 5592, dffv3 5521, fv2 5520, and fv3 5541 (the latter two previously required to be a set.) Restricted equivalents that require to be a function are shown in funfv 5586 and funfv2 5587. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5566. (Contributed by Scott Fenton, 6-Oct-2017.) |
6-Oct-2017 | csbiotag 5248 | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) |
6-Oct-2017 | dfiota4 5247 | The operation using the operator. (Contributed by Scott Fenton, 6-Oct-2017.) |
5-Oct-2017 | 1vwmgra 28181 | Every graph with one vertex is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
5-Oct-2017 | frgra3v 28180 | Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
USGrph FriendGrph | ||
5-Oct-2017 | diftpsneq 28070 | Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
5-Oct-2017 | difprsneq 28068 | Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
4-Oct-2017 | frgra3vlem2 28179 | Lemma 2 for frgra3v 28180. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
USGrph | ||
4-Oct-2017 | frgra3vlem1 28178 | Lemma 1 for frgra3v 28180. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
USGrph | ||
4-Oct-2017 | frgra1v 28176 | Any graph with only one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
USGrph FriendGrph | ||
4-Oct-2017 | frgra0v 28174 | Any graph with no vertex is a friendship graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
FriendGrph | ||
4-Oct-2017 | frisusgra 28173 | A friendship graph is an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
FriendGrph USGrph | ||
4-Oct-2017 | frisusgrapr 28172 | A friendship graph is an undirected simple graph without loops with special properties. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
FriendGrph USGrph | ||
4-Oct-2017 | isfrgra 28171 | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
FriendGrph USGrph | ||
2-Oct-2017 | df-frgra 28170 | Define the class of all Friendship Graphs. A graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) |
FriendGrph USGrph | ||
30-Sep-2017 | frgra2v 28177 | Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |
FriendGrph | ||
30-Sep-2017 | frgra0 28175 | Any empty graph (graph without vertices) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |
FriendGrph | ||
30-Sep-2017 | usgra0v 28117 | The empty graph with no vertices is a graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |
USGrph | ||
27-Sep-2017 | log2le1 23409 | is less than . This is just a weaker form of log2ub 20245 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
27-Sep-2017 | logblt 23408 | The general logarithm function is monotone. See logltb 19953 (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb logb | ||
27-Sep-2017 | logbrec 23407 | Logarithm of a reciprocal changes sign. See logrec 20117 (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb logb | ||
27-Sep-2017 | nnlogbexp 23406 | Identity law for general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb | ||
27-Sep-2017 | logb1 23405 | The natural logarithm of in base . See log1 19939 (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb | ||
27-Sep-2017 | relogbcl 23404 | Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb | ||
27-Sep-2017 | rnlogbcl 23403 | Closure of the general logarithm with integer base on positive reals. See logbcl 23399. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb | ||
27-Sep-2017 | rnlogbval 23402 | Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
logb | ||
27-Sep-2017 | cnre2csqima 23295 | Image of a centered square by the canonical bijection from to . (Contributed by Thierry Arnoux, 27-Sep-2017.) |
27-Sep-2017 | cnre2csqlem 23294 | Lemma for cnre2csqima 23295 (Contributed by Thierry Arnoux, 27-Sep-2017.) |
27-Sep-2017 | df2ndres 23244 | Definition for a restriction of the (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
27-Sep-2017 | df1stres 23243 | Definition for a restriction of the (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
26-Sep-2017 | rnlogblem 23401 | Useful lemma for working with integer logarithm bases (with is a common case, e.g. base 2, base 3 or base 10) (Contributed by Thierry Arnoux, 26-Sep-2017.) |
26-Sep-2017 | difioo 23275 | The difference between two opened intervals sharing the same lower bound (Contributed by Thierry Arnoux, 26-Sep-2017.) |
26-Sep-2017 | joiniooico 23265 | Disjoint joining an open interval with a closed below, open above interval to form a closed below, open above interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
26-Sep-2017 | ioossioo 23264 | Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
25-Sep-2017 | sqsscirc2 23293 | The complex square of side is a subset of the complex circle of radius . (Contributed by Thierry Arnoux, 25-Sep-2017.) |
25-Sep-2017 | sqsscirc1 23292 | The complex square of side is a subset of the complex circle of radius . (Contributed by Thierry Arnoux, 25-Sep-2017.) |
25-Sep-2017 | curry2ima 23247 | The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
25-Sep-2017 | rabss3d 23136 | Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
24-Sep-2017 | cevath 27859 |
Ceva's theorem. Let be a triangle and let
points ,
and lie on sides , ,
correspondingly. Suppose that cevians , and
intersect at one point . Then triangle's sides are partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 27858 three times and then using cevathlem1 27857 to multiply obtained identities and prove the theorem. In the theorem statement we are using function as a collinearity indicator. For justification of that use, see sigarcol 27854. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
24-Sep-2017 | cevathlem2 27858 | Ceva's theorem second lemma. Relate (doubled) areas of triangles and with of segments and . (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
24-Sep-2017 | cevathlem1 27857 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
24-Sep-2017 | sigariz 27853 | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. ( Contributed by Saveliy Skresanov, 23-Sep-2017.) (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
24-Sep-2017 | dya2iocrrnval 23582 | The value of a dyadic square cover of . (Contributed by Thierry Arnoux, 24-Sep-2017.) |
24-Sep-2017 | dya2iocival 23576 | The function returns closed below opened above dyadic rational intervals covering the the real line. This is the same construction as in dyadmbl 18955. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
24-Sep-2017 | xpct 23338 | The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
24-Sep-2017 | rnmptss 23238 | The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
24-Sep-2017 | difeq 23128 | Rewriting an equation with set difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
23-Sep-2017 | sigaradd 27856 | Subtracting (double) area of from yields the (double) area of . (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
23-Sep-2017 | sharhght 27855 | Let be a triangle, and let lie on the line . Then (doubled) areas of triangles and relate as lengths of corresponding bases and . (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
23-Sep-2017 | sigarimcd 27852 | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
23-Sep-2017 | sspreima 23210 | The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.) |
22-Sep-2017 | sigarcol 27854 | Given three points , and such that , the point lies on the line going through and iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
22-Sep-2017 | sigardiv 27851 | If signed area between vectors and is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
22-Sep-2017 | areacirc 24931 | The area of a circle of radius is . (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) |
area | ||
22-Sep-2017 | areacirclem6 24930 | Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) |
22-Sep-2017 | dya2iocbrsiga 23578 | Dyadic intervals are Borel sets of . (Contributed by Thierry Arnoux, 22-Sep-2017.) |
𝔅_{ℝ} | ||
22-Sep-2017 | br2base 23574 | The base set for the generator of the Borel sigma algebra on is indeed . (Contributed by Thierry Arnoux, 22-Sep-2017.) |
𝔅_{ℝ} 𝔅_{ℝ} | ||
22-Sep-2017 | sssigagen2 23507 | A subset of the generating set is also a subset of the generated sigma algebra. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
sigaGen | ||
22-Sep-2017 | xpinpreima2 23291 | Rewrite the cartesian product of two sets as the intersection of their preimage by and , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
22-Sep-2017 | xpinpreima 23290 | Rewrite the cartesian product of two sets as the intersection of their preimage by and , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
22-Sep-2017 | 2ndnpr 23246 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
22-Sep-2017 | 1stnpr 23245 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
22-Sep-2017 | ax16 1985 | Proof of older axiom ax-16 2083. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.) |
21-Sep-2017 | tpr2rico 23296 | For any point of an open set of the usual topology on there is a closed below opened above square which contains that point and is entirely in the open set. This is square is actually similar to a ball by the norm, closed below, centered on . (Contributed by Thierry Arnoux, 21-Sep-2017.) |
21-Sep-2017 | clduni 23289 | For any topology, the union of the closed sets is the base set. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
21-Sep-2017 | tpr2uni 23288 | The usual topology on is the product topology of the usual topology on . (Contributed by Thierry Arnoux, 21-Sep-2017.) |
21-Sep-2017 | tpr2tp 23287 | The usual topology on is the product topology of the usual topology on . (Contributed by Thierry Arnoux, 21-Sep-2017.) |
TopOn | ||
21-Sep-2017 | icossico 23263 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
20-Sep-2017 | sigarperm 27850 | Signed area acts as a double area of a triangle . Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
20-Sep-2017 | sigarexp 27849 | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
20-Sep-2017 | sigarid 27848 | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
19-Sep-2017 | chordthmALT 28710 | The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA PB and PC PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to . The result is proven by using chordthmlem5 20133 twice to show that PA PB and PC PD both equal BQ ^{2} PQ ^{2} . This is similar to the proof of the theorem given in Euclid's Elements_, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm 20134. http://www.virtualdeduction.com/chordthmaltvd.html is a Virtual Deduction User's Proof transcription of chordthm 20134. That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT 28710 Metamath proof. (Contributed by Alan Sare, 19-Sep-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
19-Sep-2017 | sigarls 27847 | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigarms 27846 | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigaras 27845 | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigarmf 27844 | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigaraf 27843 | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigarac 27842 | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigarim 27841 | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | sigarval 27840 | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
19-Sep-2017 | dya2iocrfn 23580 | The function returning dyadic square covering for a given size has domain . (Contributed by Thierry Arnoux, 19-Sep-2017.) |
19-Sep-2017 | dya2iocseg 23579 | For any point and any closed below, opened above interval of centered on that point, there is a closed below opened above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
logb | ||
19-Sep-2017 | dya2ub 23575 | An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
logb | ||
19-Sep-2017 | rexunirn 23140 | Restricted existential quantification over the union of the range of a function. Cf. rexrn 5667 and eluni2 3831. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
18-Sep-2017 | dya2iocct 23581 | The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017.) |
18-Sep-2017 | dya2iocress 23577 | Dyadic intervals are subsets of . (Contributed by Thierry Arnoux, 18-Sep-2017.) |
17-Sep-2017 | elsigagen2 23509 | A any countable union of elements of a set is also in the sigma algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
sigaGen | ||
17-Sep-2017 | mpt2cti 23346 | An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
13-Sep-2017 | ssnnssfz 23277 | For any finite subset of , find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017.) |
12-Sep-2017 | w5a 28368 | Extend wff definition to include 5-way conjunction ('and'). (Contributed by Alan Sare, 12-Sep-2017.) (New usage is discouraged.) |
12-Sep-2017 | wvhc5 28367 | Syntax for a 5-virtual hypotheses collection. (Contributed by Alan Sare, 12-Sep-2017.) (New usage is discouraged.) |
12-Sep-2017 | wvhc4 28366 | Syntax for a 4-virtual hypotheses collection. (Contributed by Alan Sare, 12-Sep-2017.) (New usage is discouraged.) |
12-Sep-2017 | xrlelttric 23250 | Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
7-Sep-2017 | nssdmovg 28077 | The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017.) |
5-Sep-2017 | ceqsrexv2 24078 | Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) |
5-Sep-2017 | esumcvg2 23455 | Simpler version of esumcvg 23454. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
↾_{s} Σ^{*} Σ^{*} | ||
5-Sep-2017 | esumcvg 23454 | The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 12200. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
↾_{s} Σ^{*} Σ^{*} | ||
5-Sep-2017 | esumex 23412 | An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
Σ^{*} | ||
2-Sep-2017 | usgraedgrn 28125 | An edge of an undirected simple graph without loops always connects two different vertices. (Contributed by Alexander van der Vekens, 2-Sep-2017.) |
USGrph | ||
31-Aug-2017 | areacirclem5 24929 | Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) |
arcsin | ||
31-Aug-2017 | esumpmono 23447 | The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
Σ^{*} Σ^{*} | ||
30-Aug-2017 | dffun10 24453 | Another potential definition of functionhood. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.) |
29-Aug-2017 | areacirclem4 24927 | Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) |
28-Aug-2017 | areacirclem3 24926 | Continuity of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) |
28-Aug-2017 | areacirclem2 24925 | Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) |
arcsin | ||
28-Aug-2017 | esumpfinvalf 23444 | Same as esumpfinval 23443, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
Σ^{*} | ||
26-Aug-2017 | areacirclem1 24928 | Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) |
23-Aug-2017 | indpreima 23608 | A function with range as an indicator of the preimage of (Contributed by Thierry Arnoux, 23-Aug-2017.) |
D7ED; | ||
23-Aug-2017 | indv 23596 | Value of the indicator function generator with domain . (Contributed by Thierry Arnoux, 23-Aug-2017.) |
D7ED; | ||
23-Aug-2017 | elpreq 23188 | Equality wihin a pair (Contributed by Thierry Arnoux, 23-Aug-2017.) |
22-Aug-2017 | indf1ofs 23609 | The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
D7ED; | ||
22-Aug-2017 | ind1a 23604 | Value of the indicator function where it is . (Contributed by Thierry Arnoux, 22-Aug-2017.) |
D7ED; | ||
21-Aug-2017 | indpi1 23605 | Preimage of the singleton by the indicator function. See i1f1lem 19044. (Contributed by Thierry Arnoux, 21-Aug-2017.) |
D7ED; | ||
21-Aug-2017 | nfequid 1645 | Bound-variable hypothesis builder for . This theorem tells us that any variable, including , is effectively not free in , even though is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.) |
21-Aug-2017 | axmeredith 1395 | Alias for meredith 1394 which "verify markup *" will match to ax-meredith 1396. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.) |
20-Aug-2017 | usisumgra 28114 | An undirected simple graph without loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) |
USGrph UMGrph | ||
20-Aug-2017 | uslgrav 28100 | The classes of vertices and edges of an undirected simple graph with loops are sets. (Contributed by Alexander van der Vekens, 20-Aug-2017.) |
USLGrph | ||
19-Aug-2017 | usgranloop 28124 | In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |
USGrph | ||
19-Aug-2017 | usgraedgprv 28122 | In an undirected graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |
USGrph | ||
19-Aug-2017 | usgrass 28110 | An edge is a subset of vertices, analogous to umgrass 23871. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |
USGrph | ||
19-Aug-2017 | usgrav 28101 | The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |
USGrph | ||
19-Aug-2017 | ax17o 2096 |
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of
the preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(This theorem simply repeats ax-17 1603 so that we can include the following note, which applies only to the obsolete axiomatization.) This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1533, ax-5o 2075, ax-4 2074, ax-7 1708, ax-6o 2076, ax-8 1643, ax-12o 2081, ax-9o 2077, ax-10o 2078, ax-13 1686, ax-14 1688, ax-15 2082, ax-11o 2080, and ax-16 2083: in that system, we can derive any instance of ax-17 1603 not containing wff variables by induction on formula length, using ax17eq 2122 and ax17el 2128 for the basis together hbn 1720, hbal 1710, and hbim 1725. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification discouraged.) |
18-Aug-2017 | usgrafun 28108 | The edge function of an undirected simple graph without loops is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) |
USGrph | ||
18-Aug-2017 | ax4 2084 | This theorem repeats sp 1716 under the name ax4 2084, so that the metamath program's "verify markup" command will check that it matches axiom scheme ax-4 2074. It is preferred that references to this theorem use the name sp 1716. (Contributed by NM, 18-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
17-Aug-2017 | usgraedgop 28109 | An edge of an undirected simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) |
USGrph | ||
15-Aug-2017 | usgraexmpl 28133 | is a graph of five vertices , with edges . (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
USGrph | ||
15-Aug-2017 | usgraexmpldifpr 28132 | Lemma for usgraexmpl 28133: all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
15-Aug-2017 | s4dom 28092 | The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
14-Aug-2017 | s4f1o 28093 | A length 4 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
14-Aug-2017 | s2f1o 28091 | A length 2 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
14-Aug-2017 | s4prop 28090 | A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
14-Aug-2017 | s2prop 28089 | A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
14-Aug-2017 | f1oun2prg 28076 | A union of unordered pairs of ordered pairs with different elements is a one-to-one onto function. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
14-Aug-2017 | f1oprg 28075 | An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap 5515. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
14-Aug-2017 | indf1o 23607 | The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
D7ED; | ||
14-Aug-2017 | indsum 23606 | Finite sum of a product with the indicator function / cross-product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
D7ED; | ||
14-Aug-2017 | ind0 23603 | Value of the indicator function where it is . (Contributed by Thierry Arnoux, 14-Aug-2017.) |
D7ED; | ||
14-Aug-2017 | ind1 23602 | Value of the indicator function where it is . (Contributed by Thierry Arnoux, 14-Aug-2017.) |
D7ED; | ||
14-Aug-2017 | pr01ssre 23601 | The range of the indicator function is a subset of . (Contributed by Thierry Arnoux, 14-Aug-2017.) |
13-Aug-2017 | usgraex3elv 28131 | Lemma 3 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | usgraex2elv 28130 | Lemma 2 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | usgraex1elv 28129 | Lemma 1 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | usgraex0elv 28128 | Lemma 0 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | usgraexvlem 28127 | Lemma for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | usgraf0 28107 | The edge function of an undirected simple graph without loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
USGrph | ||
13-Aug-2017 | isusgra0 28106 | The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
USGrph | ||
13-Aug-2017 | prelpw 28074 | A pair of elements of a set is an element of the set's power set. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | prneimg 28073 | Two pairs are not equal if one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
13-Aug-2017 | indfval 23600 | Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
D7ED; | ||
13-Aug-2017 | indf 23599 | An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
D7ED; | ||
13-Aug-2017 | spnfw 1640 | Weak version of sp 1716. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.) |
12-Aug-2017 | ax12b 1655 | Two equivalent ways of expressing ax-12 1866. See the comment for ax-12 1866. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 12-Aug-2017.) |
11-Aug-2017 | usgraedg2 28121 | The value of the "edge function" of a graph is a set containing two elements (the vertices the corresponding edge is connecting), analogous to umgrale 23873. (Contributed by Alexander van der Vekens, 11-Aug-2017.) |
USGrph | ||
11-Aug-2017 | usgraeq12d 28111 | Equality of simple graphs without loops. (Contributed by Alexander van der Vekens, 11-Aug-2017.) |
USGrph USGrph | ||
10-Aug-2017 | uslgraun 28120 | If and are (simple) graphs (with loops), then is a multigraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices), analogous to umgraun 23879. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph USLGrph UMGrph | ||
10-Aug-2017 | usgra1 28119 | The graph with one edge, analogous to umgra1 23878 ( with additional assumption that since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph | ||
10-Aug-2017 | uslgra1 28118 | The graph with one edge, analogous to umgra1 23878. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph | ||
10-Aug-2017 | usgra0 28116 | The empty graph, with vertices but no edges, is a graph, analogous to umgra0 23877. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph | ||
10-Aug-2017 | usgrares 28115 | A subgraph of a graph (formed by removing some edges from the original graph) is a graph, analogous to umgrares 23876. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph USGrph | ||
10-Aug-2017 | usisuslgra 28113 | An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph USLGrph | ||
10-Aug-2017 | uslisumgra 28112 | An undirected simple graph with loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph UMGrph | ||
10-Aug-2017 | usgraf 28105 | The edge function of an undirected simple graph without loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph | ||
10-Aug-2017 | uslgraf 28104 | The edge function of an undirected simple graph with loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph | ||
10-Aug-2017 | isusgra 28103 | The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph | ||
10-Aug-2017 | isuslgra 28102 | The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph | ||
10-Aug-2017 | relusgra 28099 | The class of all undirected simple graph without loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph | ||
10-Aug-2017 | reluslgra 28098 | The class of all undirected simple graph with loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph | ||
10-Aug-2017 | df-usgra 28097 | Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph where is an injective (one-to-one) function into subsets of of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itsself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USGrph | ||
10-Aug-2017 | df-uslgra 28096 | Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph where is an injective (one-to-one) function into subsets of of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |
USLGrph | ||
7-Aug-2017 | iocinif 23274 | Relate intersection of two opened below, closed above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
7-Aug-2017 | iocinioc2 23272 | Intersection between two opened below, closed above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
7-Aug-2017 | incexc2 12297 | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.) |
7-Aug-2017 | incexc 12296 | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.) |
7-Aug-2017 | incexclem 12295 | Lemma for incexc 12296. (Contributed by Mario Carneiro, 7-Aug-2017.) |
7-Aug-2017 | spimw 1638 | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
7-Aug-2017 | spimfw 1627 | Specialization, with additional weakening to allow bundling of and . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-1017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
6-Aug-2017 | hashun3 11366 | The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017.) |
5-Aug-2017 | speimfw 1626 | Specialization, with additional weakening to allow bundling of and . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Aug-2017.) |
4-Aug-2017 | lmdvg 23376 | If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
4-Aug-2017 | fzssnn 23276 | Finite sets of sequential integers starting from a natural are a subset of the natural numbers. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
4-Aug-2017 | equequ2 1649 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) |
3-Aug-2017 | dvreacos 24924 | Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.) |
arccos | ||
3-Aug-2017 | dvreasin 24923 | Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.) |
arcsin | ||
3-Aug-2017 | lmdvglim 23377 | If a monotonic real number sequence diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017.) |
↾_{s} | ||
3-Aug-2017 | a9ev 1637 | At least one individual exists. Weaker version of a9e 1891. When possible, use of this theorem rather than a9e 1891 is preferred since its derivation from axioms is much shorter. (Contributed by NM, 3-Aug-2017.) |
2-Aug-2017 | ralbinrald 27977 | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
2-Aug-2017 | lmxrge0 23375 | Express "sequence converges to plus infinity" (i.e. diverges), for a sequence of non-negative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.) |
↾_{s} | ||
2-Aug-2017 | 19.2 1671 | Theorem 19.2 of [Margaris] p. 89. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1780 for a more conventional proof. (Contributed by NM, 2-Aug-2017.) |
1-Aug-2017 | xrdifh 23273 | Set difference of a half-opened interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.) |
1-Aug-2017 | dvelimhw 1735 | Proof of dvelimh 1904 without using ax-12 1866 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.21h 1731 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." (Contributed by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.9v 1663 | Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.3v 1662 | Special case of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.8w 1659 | Weak version of 19.8a 1718. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) |
1-Aug-2017 | spnfwOLD 1658 | Weak version of sp 1716. Uses only Tarski's FOL axiom schemes. Obsolete version of spnfw 1640 as of 13-Aug-2017. (Contributed by NM, 1-Aug-2017.) (New usage is discouraged.) |
31-Jul-2017 | esumpcvgval 23446 | The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
Σ^{*} | ||
31-Jul-2017 | pnfneige0 23374 | A neighborhood of contains an unbounded interval based at a real number. See pnfnei 16950 (Contributed by Thierry Arnoux, 31-Jul-2017.) |
↾_{s} | ||
28-Jul-2017 | tz6.12-afv 28035 | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, , analogous to tz6.12-1 5544, but it is required for A to be a set. (Contributed by Alexander van der Vekens, 28-Jul-2017.) |
''' | ||
28-Jul-2017 | rge0scvg 23373 | Implication of convergence for a non-negative series. This could be used to shorten prmreclem6 12968 (Contributed by Thierry Arnoux, 28-Jul-2017.) |
26-Jul-2017 | xrge0haus 23326 | The topology of the extended non-negative real numbers is Hausdorf. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
↾_{s} | ||
25-Jul-2017 | funressnfv 27991 | A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
25-Jul-2017 | funcoressn 27990 | A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
25-Jul-2017 | fnresfnco 27989 | Composition of two functions, similar to fnco 5352. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
25-Jul-2017 | funresfunco 27988 | Composition of two functions, generalization of funco 5292. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
23-Jul-2017 | afvco2 28037 | Value of a function composition, analogous to fvco2 5594. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
''' '''''' | ||
23-Jul-2017 | dmfcoafv 28036 | Domains of a function composition, analogous to dmfco 5593. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
''' | ||
23-Jul-2017 | csbafv12g 28000 | Move class substitution in and out of a function value, analogous to csbfv12g 5535, with a direct proof proposed by Mario Carneiro, analogous to csbovg 5889. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
''' ''' | ||
23-Jul-2017 | sbcfun 27985 | Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
23-Jul-2017 | csbdmg 27980 | Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
23-Jul-2017 | sbcrel 27979 | Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
23-Jul-2017 | sbcss 3564 | Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.) |
22-Jul-2017 | afvres 28034 | The value of a restricted function, analogous to fvres 5542. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
''' ''' | ||
22-Jul-2017 | afveq2 27998 | Equality theorem for function value, analogous to fveq1 5524. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
''' ''' | ||
22-Jul-2017 | afveq1 27997 | Equality theorem for function value, analogous to fveq1 5524. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
''' ''' | ||
22-Jul-2017 | dfafv2 27995 | Alternative definition of ''' using directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
''' defAt | ||
22-Jul-2017 | dfdfat2 27994 | Alternate definition of the predicate "defined at" not using the predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
defAt | ||
22-Jul-2017 | logbid1 23400 | General logarithm when base and arg match (Contributed by David A. Wheeler, 22-Jul-2017.) |
logb | ||
22-Jul-2017 | logeq0im1 23396 | if then (Contributed by David A. Wheeler, 22-Jul-2017.) |
22-Jul-2017 | eldiftp 23395 | Membership in a set with three elements removed. Similar to eldifsn 3749 and eldifpr 23394. (Contributed by David A. Wheeler, 22-Jul-2017.) |
18-Jul-2017 | eldifpr 23394 | Membership in a set with two elements removed. Similar to eldifsn 3749 and eldiftp 23395. (Contributed by Mario Carneiro, 18-Jul-2017.) |
17-Jul-2017 | logbcl 23399 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) |
logb | ||
17-Jul-2017 | logccne0ALT 23398 | log isn't 0 if argument isn't 0 or 1. Unlike logne0 19956, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.) |
17-Jul-2017 | logccne0 23397 | log isn't 0 if argument isn't 0 or 1. Unlike logne0 19956, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.) |
16-Jul-2017 | logb2aval 23393 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) |
logb | ||
16-Jul-2017 | logbval 23392 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the other operand here. Proof is similar to modval 10975. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) |
logb | ||
16-Jul-2017 | prmz 12762 | A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.) |
14-Jul-2017 | df-log_ 28258 | Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as log_ for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.) |
log_ | ||
11-Jul-2017 | dstfrvclim1 23678 | The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.) |
Prob rRndVar ∘_{RV/𝑐} | ||
11-Jul-2017 | meascnbl 23546 | A measure is continuous from below. Cf. volsup 18913. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.) |
↾_{s} measures | ||
11-Jul-2017 | lmlimxrge0 23372 | Relate a limit in the non-negative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
↾_{s} | ||
11-Jul-2017 | lmlim 23371 | Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
TopOn ↾_{t} ℂ_{fld} ↾_{t} | ||
6-Jul-2017 | esumdivc 23451 | An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
Σ^{*} /_{𝑒} Σ^{*} /_{𝑒} | ||
6-Jul-2017 | esummulc2 23450 | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
Σ^{*} Σ^{*} | ||
6-Jul-2017 | esummulc1 23449 | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
Σ^{*} Σ^{*} | ||
6-Jul-2017 | xrge0addgt0 23331 | The sum of nonnegative and positive numbers is positive. See addgtge0 9262 (Contributed by Thierry Arnoux, 6-Jul-2017.) |
6-Jul-2017 | xrge0mulc1cn 23323 | The operation multiplying a non-negative real numbers by a non-negative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
ordTop ↾_{t} | ||
6-Jul-2017 | elicoelioo 23271 | Relate elementhood to a closed-below, opened-above interval with elementhood to the same opened interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
5-Jul-2017 | esumcst 23436 | The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.) |
Σ^{*} | ||
5-Jul-2017 | ishashinf 23389 | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 7076 (Contributed by Thierry Arnoux, 5-Jul-2017.) |
5-Jul-2017 | gsumconstf 23381 | Sum of a constant series (Contributed by Thierry Arnoux, 5-Jul-2017.) |
._{g} _{g} | ||
5-Jul-2017 | xrmulc1cn 23303 | The operation multiplying an extended real number by a non-negative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
ordTop | ||
5-Jul-2017 | xeqlelt 23269 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
5-Jul-2017 | xdivrec 23110 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
/_{𝑒} /_{𝑒} | ||
3-Jul-2017 | eliccelico 23270 | Relate elementhood to a closed interval with elementhood to the same closed-below, opened-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
3-Jul-2017 | or3dir 23124 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
3-Jul-2017 | or3di 23123 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
2-Jul-2017 | eldmressnsn 27984 | The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | dmressnsn 27983 | The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | eldmressn 27982 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | 2reu8 27970 | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2230. Curiously, we can put on either of the internal conjuncts but not both. We can also commute using 2reu7 27969. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |