Home | Metamath
Proof Explorer Theorem List (p. 323 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 | btwnconn1lem8 32201 | Lemma for btwnconn1 32208. Now, we introduce the last three points used in the construction: , , and will turn out to be equal further down, and will provide us with the key to the final statement. We begin by establishing congruence of and . (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem9 32202 | Lemma for btwnconn1 32208. Now, a quick use of transitivity to establish congruence on and . (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem10 32203 | Lemma for btwnconn1 32208. Now we establish a congruence that will give us when we compute later on. (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem11 32204 | Lemma for btwnconn1 32208. Now, we establish that and are equidistant from . (Contributed by Scott Fenton, 8-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem12 32205 | Lemma for btwnconn1 32208. Using a long string of invocations of linecgr 32188, we show that . (Contributed by Scott Fenton, 9-Oct-2013.) |
Cgr Cgr Cgr Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem13 32206 | Lemma for btwnconn1 32208. Begin back-filling and eliminating hypotheses. (Contributed by Scott Fenton, 9-Oct-2013.) |
Cgr Cgr Cgr Cgr | ||
Theorem | btwnconn1lem14 32207 | Lemma for btwnconn1 32208. Final statement of the theorem when . (Contributed by Scott Fenton, 9-Oct-2013.) |
Theorem | btwnconn1 32208 | Connectitivy law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. (Contributed by Scott Fenton, 9-Oct-2013.) |
Theorem | btwnconn2 32209 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 9-Oct-2013.) |
Theorem | btwnconn3 32210 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 9-Oct-2013.) |
Theorem | midofsegid 32211 | If two points fall in the same place in the middle of a segment, then they are identical. (Contributed by Scott Fenton, 16-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Cgr | ||
Theorem | segcon2 32212* | Generalization of axsegcon 25807. This time, we generate an endpoint for a segment on the ray congruent to and starting at , as opposed to axsegcon 25807, where the segment starts at (Contributed by Scott Fenton, 14-Oct-2013.) (Removed unneeded inequality, 15-Oct-2013.) |
Cgr | ||
Syntax | csegle 32213 | Declare the constant for the segment less than or equal to relationship. |
Definition | df-segle 32214* | Define the segment length comparison relationship. This relationship expresses that the segment is no longer than . In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 11-Oct-2013.) |
Cgr | ||
Theorem | brsegle 32215* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
Cgr | ||
Theorem | brsegle2 32216* | Alternate characterization of segment comparison. Theorem 5.5 of [Schwabhauser] p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013.) |
Cgr | ||
Theorem | seglecgr12im 32217 | Substitution law for segment comparison under congruence. Theorem 5.6 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
Cgr Cgr | ||
Theorem | seglecgr12 32218 | Substitution law for segment comparison under congruence. Biconditional version. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Cgr Cgr | ||
Theorem | seglerflx 32219 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
Theorem | seglemin 32220 | Any segment is at least as long as a degenerate segment. Theorem 5.11 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
Theorem | segletr 32221 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
Theorem | segleantisym 32222 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
Cgr | ||
Theorem | seglelin 32223 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
Theorem | btwnsegle 32224 | If falls between and , then is no longer than . (Contributed by Scott Fenton, 16-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | colinbtwnle 32225 | Given three colinear points , , and , falls in the middle iff the two segments to are no longer than . Theorem 5.12 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Syntax | coutsideof 32226 | Declare the syntax for the outside of constant. |
OutsideOf | ||
Definition | df-outsideof 32227 | The outside of relationship. This relationship expresses that , , and fall on a line, but is not on the segment . This definition is taken from theorem 6.4 of [Schwabhauser] p. 43, since it requires no dummy variables. (Contributed by Scott Fenton, 17-Oct-2013.) |
OutsideOf | ||
Theorem | broutsideof 32228 | Binary relation form of OutsideOf. Theorem 6.4 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | broutsideof2 32229 | Alternate form of OutsideOf. Definition 6.1 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | outsidene1 32230 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | outsidene2 32231 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | btwnoutside 32232 | A principle linking outsideness to betweenness. Theorem 6.2 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | broutsideof3 32233* | Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | outsideofrflx 32234 | Reflexitivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | outsideofcom 32235 | Commutitivity law for outsideness. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf OutsideOf | ||
Theorem | outsideoftr 32236 | Transitivity law for outsideness. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf OutsideOf OutsideOf | ||
Theorem | outsideofeq 32237 | Uniqueness law for OutsideOf. Analogue of segconeq 32117. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf Cgr OutsideOf Cgr | ||
Theorem | outsideofeu 32238* | Given a non-degenerate ray, there is a unique point congruent to the segment lying on the ray . Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf Cgr | ||
Theorem | outsidele 32239 | Relate OutsideOf to . Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Theorem | outsideofcol 32240 | Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
OutsideOf | ||
Syntax | cline2 32241 | Declare the constant for the line function. |
Line | ||
Syntax | cray 32242 | Declare the constant for the ray function. |
Ray | ||
Syntax | clines2 32243 | Declare the constant for the set of all lines. |
LinesEE | ||
Definition | df-line2 32244* | Define the Line function. This function generates the line passing through the distinct points and . Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.) |
Line | ||
Definition | df-ray 32245* | Define the Ray function. This function generates the set of all points that lie on the ray starting at and passing through . Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.) |
Ray OutsideOf | ||
Definition | df-lines2 32246 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 32259 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
LinesEE Line | ||
Theorem | funray 32247 | Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Ray | ||
Theorem | fvray 32248* | Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Ray OutsideOf | ||
Theorem | funline 32249 | Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | linedegen 32250 | When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | fvline 32251* | Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | liness 32252 | A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | fvline2 32253* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | lineunray 32254 | A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line Ray Ray | ||
Theorem | lineelsb2 32255 | If lies on , then . Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line Line Line | ||
Theorem | linerflx1 32256 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | linecom 32257 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line Line | ||
Theorem | linerflx2 32258 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Line | ||
Theorem | ellines 32259* | Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
LinesEE Line | ||
Theorem | linethru 32260 | If is a line containing two distinct points and , then is the line through and . Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
LinesEE Line | ||
Theorem | hilbert1.1 32261* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
LinesEE | ||
Theorem | hilbert1.2 32262* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
LinesEE | ||
Theorem | linethrueu 32263* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
LinesEE | ||
Theorem | lineintmo 32264* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
LinesEE LinesEE | ||
Syntax | cfwddif 32265 | Declare the syntax for the forward difference operator. |
Definition | df-fwddif 32266* | Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.) |
Syntax | cfwddifn 32267 | Declare the syntax for the nth forward difference operator. |
| ||
Definition | df-fwddifn 32268* | Define the nth forward difference operator. This works out to be the forward difference operator iterated times. (Contributed by Scott Fenton, 28-May-2020.) |
| ||
Theorem | fwddifval 32269 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
Theorem | fwddifnval 32270* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
| ||
Theorem | fwddifn0 32271 | The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.) |
| ||
Theorem | fwddifnp1 32272* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
| ||
Theorem | rankung 32273 | The rank of the union of two sets. Closed form of rankun 8719. (Contributed by Scott Fenton, 15-Jul-2015.) |
Theorem | ranksng 32274 | The rank of a singleton. Closed form of ranksn 8717. (Contributed by Scott Fenton, 15-Jul-2015.) |
Theorem | rankelg 32275 | The membership relation is inherited by the rank function. Closed form of rankel 8702. (Contributed by Scott Fenton, 16-Jul-2015.) |
Theorem | rankpwg 32276 | The rank of a power set. Closed form of rankpw 8706. (Contributed by Scott Fenton, 16-Jul-2015.) |
Theorem | rank0 32277 | The rank of the empty set is . (Contributed by Scott Fenton, 17-Jul-2015.) |
Theorem | rankeq1o 32278 | The only set with rank is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
Syntax | chf 32279 | The constant Hf is a class. |
Hf | ||
Definition | df-hf 32280 | Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.) |
Hf | ||
Theorem | elhf 32281* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
Hf | ||
Theorem | elhf2 32282 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
Hf | ||
Theorem | elhf2g 32283 | Hereditarily finiteness via rank. Closed form of elhf2 32282. (Contributed by Scott Fenton, 15-Jul-2015.) |
Hf | ||
Theorem | 0hf 32284 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
Hf | ||
Theorem | hfun 32285 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
Hf Hf Hf | ||
Theorem | hfsn 32286 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
Hf Hf | ||
Theorem | hfadj 32287 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
Hf Hf Hf | ||
Theorem | hfelhf 32288 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
Hf Hf | ||
Theorem | hftr 32289 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
Hf | ||
Theorem | hfext 32290* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
Hf Hf Hf | ||
Theorem | hfuni 32291 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
Hf Hf | ||
Theorem | hfpw 32292 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
Hf Hf | ||
Theorem | hfninf 32293 | is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
Hf | ||
Theorem | a1i14 32294 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
Theorem | a1i24 32295 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 5-Aug-2009.) |
Theorem | exp5d 32296 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp5g 32297 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp5k 32298 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp56 32299 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp58 32300 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |