![]() |
Metamath
Proof Explorer Theorem List (p. 351 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ctransport 35001 | Declare the syntax for the segment transport function. |
class TransportTo | ||
Definition | df-transport 35002* | Define the segment transport function. See fvtransport 35004 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.) |
β’ TransportTo = {β¨β¨π, πβ©, π₯β© β£ βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st βπ), πβ© β§ β¨(2nd βπ), πβ©Cgrπ)))} | ||
Theorem | funtransport 35003 | The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun TransportTo | ||
Theorem | fvtransport 35004* | Calculate the value of the TransportTo function. This function takes four points, π΄ through π·, where πΆ and π· are distinct. It then returns the point that extends πΆπ· by the length of π΄π΅. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β (β¨π΄, π΅β©TransportToβ¨πΆ, π·β©) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) | ||
Theorem | transportcl 35005 | Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β (β¨π΄, π΅β©TransportToβ¨πΆ, π·β©) β (πΌβπ)) | ||
Theorem | transportprops 35006 | Calculate the defining properties of the transport function. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β (π· Btwn β¨πΆ, (β¨π΄, π΅β©TransportToβ¨πΆ, π·β©)β© β§ β¨π·, (β¨π΄, π΅β©TransportToβ¨πΆ, π·β©)β©Cgrβ¨π΄, π΅β©)) | ||
Syntax | cifs 35007 | Declare the syntax for the inner five segment predicate. |
class InnerFiveSeg | ||
Syntax | ccgr3 35008 | Declare the syntax for the three place congruence predicate. |
class Cgr3 | ||
Syntax | ccolin 35009 | Declare the syntax for the colinearity predicate. |
class Colinear | ||
Syntax | cfs 35010 | Declare the syntax for the five segment predicate. |
class FiveSeg | ||
Definition | df-colinear 35011* | The colinearity predicate states that the three points in its arguments sit on one line. Definition 4.10 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 25-Oct-2013.) |
β’ Colinear = β‘{β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ (π Btwn β¨π, πβ© β¨ π Btwn β¨π, πβ© β¨ π Btwn β¨π, πβ©))} | ||
Definition | df-ifs 35012* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 35015 and ifscgr 35016 for how it is used. Definition 4.1 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 26-Sep-2013.) |
β’ InnerFiveSeg = {β¨π, πβ© β£ βπ β β βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ₯ β (πΌβπ)βπ¦ β (πΌβπ)βπ§ β (πΌβπ)βπ€ β (πΌβπ)(π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π₯, π¦β©, β¨π§, π€β©β© β§ ((π Btwn β¨π, πβ© β§ π¦ Btwn β¨π₯, π§β©) β§ (β¨π, πβ©Cgrβ¨π₯, π§β© β§ β¨π, πβ©Cgrβ¨π¦, π§β©) β§ (β¨π, πβ©Cgrβ¨π₯, π€β© β§ β¨π, πβ©Cgrβ¨π§, π€β©)))} | ||
Definition | df-cgr3 35013* | The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.) |
β’ Cgr3 = {β¨π, πβ© β£ βπ β β βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)(π = β¨π, β¨π, πβ©β© β§ π = β¨π, β¨π, πβ©β© β§ (β¨π, πβ©Cgrβ¨π, πβ© β§ β¨π, πβ©Cgrβ¨π, πβ© β§ β¨π, πβ©Cgrβ¨π, πβ©))} | ||
Definition | df-fs 35014* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 35051 and fscgr 35052 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ FiveSeg = {β¨π, πβ© β£ βπ β β βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ₯ β (πΌβπ)βπ¦ β (πΌβπ)βπ§ β (πΌβπ)βπ€ β (πΌβπ)(π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π₯, π¦β©, β¨π§, π€β©β© β§ (π Colinear β¨π, πβ© β§ β¨π, β¨π, πβ©β©Cgr3β¨π₯, β¨π¦, π§β©β© β§ (β¨π, πβ©Cgrβ¨π₯, π€β© β§ β¨π, πβ©Cgrβ¨π¦, π€β©)))} | ||
Theorem | brifs 35015 | Binary relation form of the inner five segment predicate. (Contributed by Scott Fenton, 26-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© InnerFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β ((π΅ Btwn β¨π΄, πΆβ© β§ πΉ Btwn β¨πΈ, πΊβ©) β§ (β¨π΄, πΆβ©Cgrβ¨πΈ, πΊβ© β§ β¨π΅, πΆβ©Cgrβ¨πΉ, πΊβ©) β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)))) | ||
Theorem | ifscgr 35016 | Inner five segment congruence. Take two triangles, π΄π·πΆ and πΈπ»πΊ, with π΅ between π΄ and πΆ and πΉ between πΈ and πΊ. If the other components of the triangles are congruent, then so are π΅π· and πΉπ». Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 27-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© InnerFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β β¨π΅, π·β©Cgrβ¨πΉ, π»β©)) | ||
Theorem | cgrsub 35017 | Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (((π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΉβ©) β§ (β¨π΄, πΆβ©Cgrβ¨π·, πΉβ© β§ β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©)) β β¨π΄, π΅β©Cgrβ¨π·, πΈβ©)) | ||
Theorem | brcgr3 35018 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β (β¨π΄, π΅β©Cgrβ¨π·, πΈβ© β§ β¨π΄, πΆβ©Cgrβ¨π·, πΉβ© β§ β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©))) | ||
Theorem | cgr3permute3 35019 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π΅, β¨πΆ, π΄β©β©Cgr3β¨πΈ, β¨πΉ, π·β©β©)) | ||
Theorem | cgr3permute1 35020 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π΄, β¨πΆ, π΅β©β©Cgr3β¨π·, β¨πΉ, πΈβ©β©)) | ||
Theorem | cgr3permute2 35021 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π΅, β¨π΄, πΆβ©β©Cgr3β¨πΈ, β¨π·, πΉβ©β©)) | ||
Theorem | cgr3permute4 35022 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨πΆ, β¨π΄, π΅β©β©Cgr3β¨πΉ, β¨π·, πΈβ©β©)) | ||
Theorem | cgr3permute5 35023 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨πΆ, β¨π΅, π΄β©β©Cgr3β¨πΉ, β¨πΈ, π·β©β©)) | ||
Theorem | cgr3tr4 35024 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ)) β§ (πΊ β (πΌβπ) β§ π» β (πΌβπ) β§ πΌ β (πΌβπ)))) β ((β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΊ, β¨π», πΌβ©β©) β β¨π·, β¨πΈ, πΉβ©β©Cgr3β¨πΊ, β¨π», πΌβ©β©)) | ||
Theorem | cgr3com 35025 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π·, β¨πΈ, πΉβ©β©Cgr3β¨π΄, β¨π΅, πΆβ©β©)) | ||
Theorem | cgr3rflx 35026 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π΄, β¨π΅, πΆβ©β©) | ||
Theorem | cgrxfr 35027* | A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΉ β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, πΆβ©Cgrβ¨π·, πΉβ©) β βπ β (πΌβπ)(π Btwn β¨π·, πΉβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨π, πΉβ©β©))) | ||
Theorem | btwnxfr 35028 | A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 4-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β©) β πΈ Btwn β¨π·, πΉβ©)) | ||
Theorem | colinrel 35029 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Rel Colinear | ||
Theorem | brcolinear2 35030* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β π β§ π β π) β (π Colinear β¨π, π β© β βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ (π Btwn β¨π, π β© β¨ π Btwn β¨π , πβ© β¨ π Btwn β¨π, πβ©)))) | ||
Theorem | brcolinear 35031 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β (π΄ Btwn β¨π΅, πΆβ© β¨ π΅ Btwn β¨πΆ, π΄β© β¨ πΆ Btwn β¨π΄, π΅β©))) | ||
Theorem | colinearex 35032 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Colinear β V | ||
Theorem | colineardim1 35033 | If π΄ is colinear with π΅ and πΆ, then π΄ is in the same space as π΅. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β π β§ π΅ β (πΌβπ) β§ πΆ β π)) β (π΄ Colinear β¨π΅, πΆβ© β π΄ β (πΌβπ))) | ||
Theorem | colinearperm1 35034 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β π΄ Colinear β¨πΆ, π΅β©)) | ||
Theorem | colinearperm3 35035 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β π΅ Colinear β¨πΆ, π΄β©)) | ||
Theorem | colinearperm2 35036 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β π΅ Colinear β¨π΄, πΆβ©)) | ||
Theorem | colinearperm4 35037 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β πΆ Colinear β¨π΄, π΅β©)) | ||
Theorem | colinearperm5 35038 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β πΆ Colinear β¨π΅, π΄β©)) | ||
Theorem | colineartriv1 35039 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Colinear β¨π΄, π΅β©) | ||
Theorem | colineartriv2 35040 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Colinear β¨π΅, π΅β©) | ||
Theorem | btwncolinear1 35041 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΄ Colinear β¨π΅, πΆβ©)) | ||
Theorem | btwncolinear2 35042 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΄ Colinear β¨πΆ, π΅β©)) | ||
Theorem | btwncolinear3 35043 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΅ Colinear β¨π΄, πΆβ©)) | ||
Theorem | btwncolinear4 35044 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΅ Colinear β¨πΆ, π΄β©)) | ||
Theorem | btwncolinear5 35045 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β πΆ Colinear β¨π΄, π΅β©)) | ||
Theorem | btwncolinear6 35046 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β πΆ Colinear β¨π΅, π΄β©)) | ||
Theorem | colinearxfr 35047 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((π΅ Colinear β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β©) β πΈ Colinear β¨π·, πΉβ©)) | ||
Theorem | lineext 35048* | Extend a line with a missing point. Theorem 4.14 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ))) β ((π΄ Colinear β¨π΅, πΆβ© β§ β¨π΄, π΅β©Cgrβ¨π·, πΈβ©) β βπ β (πΌβπ)β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πβ©β©)) | ||
Theorem | brofs2 35049 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β (π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΈ, β¨πΉ, πΊβ©β© β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨π΅, π·β©Cgrβ¨πΉ, π»β©)))) | ||
Theorem | brifs2 35050 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© InnerFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β (π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΈ, β¨πΉ, πΊβ©β© β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)))) | ||
Theorem | brfs 35051 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© FiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β (π΄ Colinear β¨π΅, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΈ, β¨πΉ, πΊβ©β© β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨π΅, π·β©Cgrβ¨πΉ, π»β©)))) | ||
Theorem | fscgr 35052 | Congruence law for the general five segment configuration. Theorem 4.16 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β ((β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© FiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β§ π΄ β π΅) β β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)) | ||
Theorem | linecgr 35053 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β (((π΄ β π΅ β§ π΄ Colinear β¨π΅, πΆβ©) β§ (β¨π΄, πβ©Cgrβ¨π΄, πβ© β§ β¨π΅, πβ©Cgrβ¨π΅, πβ©)) β β¨πΆ, πβ©Cgrβ¨πΆ, πβ©)) | ||
Theorem | linecgrand 35054 | Deduction form of linecgr 35053. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π β (πΌβπ)) & β’ (π β π β (πΌβπ)) & β’ ((π β§ π) β π΄ β π΅) & β’ ((π β§ π) β π΄ Colinear β¨π΅, πΆβ©) & β’ ((π β§ π) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) & β’ ((π β§ π) β β¨π΅, πβ©Cgrβ¨π΅, πβ©) β β’ ((π β§ π) β β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) | ||
Theorem | lineid 35055 | Identity law for points on lines. Theorem 4.18 of [Schwabhauser] p. 38. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (((π΄ β π΅ β§ π΄ Colinear β¨π΅, πΆβ©) β§ (β¨π΄, πΆβ©Cgrβ¨π΄, π·β© β§ β¨π΅, πΆβ©Cgrβ¨π΅, π·β©)) β πΆ = π·)) | ||
Theorem | idinside 35056 | Law for finding a point inside a segment. Theorem 4.19 of [Schwabhauser] p. 38. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((πΆ Btwn β¨π΄, π΅β© β§ β¨π΄, πΆβ©Cgrβ¨π΄, π·β© β§ β¨π΅, πΆβ©Cgrβ¨π΅, π·β©) β πΆ = π·)) | ||
Theorem | endofsegid 35057 | If π΄, π΅, and πΆ fall in order on a line, and π΄π΅ and π΄πΆ are congruent, then πΆ = π΅. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, πΆβ©Cgrβ¨π΄, π΅β©) β πΆ = π΅)) | ||
Theorem | endofsegidand 35058 | Deduction form of endofsegid 35057. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ ((π β§ π) β πΆ Btwn β¨π΄, π΅β©) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨π΄, πΆβ©) β β’ ((π β§ π) β π΅ = πΆ) | ||
Theorem | btwnconn1lem1 35059 | Lemma for btwnconn1 35073. The next several lemmas introduce various properties of hypothetical points that end up eliminating alternatives to connectivity. We begin by showing a congruence property of those hypothetical points. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π΅ β§ π΅ β πΆ) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©)))) β β¨π΅, πβ©Cgrβ¨π, πΆβ©) | ||
Theorem | btwnconn1lem2 35060 | Lemma for btwnconn1 35073. Now, we show that two of the hypotheticals we introduced in the first lemma are identical. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π΅ β§ π΅ β πΆ) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©)))) β π = π) | ||
Theorem | btwnconn1lem3 35061 | Lemma for btwnconn1 35073. Establish the next congruence in the series. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π΅ β§ π΅ β πΆ) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©)))) β β¨π΅, πβ©Cgrβ¨π, π·β©) | ||
Theorem | btwnconn1lem4 35062 | Lemma for btwnconn1 35073. Assuming πΆ β π, we now attempt to force π· = π from here out via a series of congruences. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©)))) β β¨π, πβ©Cgrβ¨π·, πΆβ©) | ||
Theorem | btwnconn1lem5 35063 | Lemma for btwnconn1 35073. Now, we introduce πΈ, the intersection of πΆπ and π·π. We begin by showing that it is the midpoint of πΆ and π. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ (πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©))) β β¨πΈ, πΆβ©Cgrβ¨πΈ, πβ©) | ||
Theorem | btwnconn1lem6 35064 | Lemma for btwnconn1 35073. Next, we show that πΈ is the midpoint of π· and π. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ (πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©))) β β¨πΈ, π·β©Cgrβ¨πΈ, πβ©) | ||
Theorem | btwnconn1lem7 35065 | Lemma for btwnconn1 35073. Under our assumptions, πΆ and π are distinct. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ (πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©))) β πΆ β π) | ||
Theorem | btwnconn1lem8 35066 | Lemma for btwnconn1 35073. 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.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ ((πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ ((πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©) β§ ((πΆ Btwn β¨π, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) β§ (πΆ Btwn β¨π, π β© β§ β¨πΆ, π β©Cgrβ¨πΆ, πΈβ©) β§ (π Btwn β¨π, πβ© β§ β¨π , πβ©Cgrβ¨π , πβ©))))) β β¨π , πβ©Cgrβ¨πΈ, πβ©) | ||
Theorem | btwnconn1lem9 35067 | Lemma for btwnconn1 35073. Now, a quick use of transitivity to establish congruence on π π and πΈπ·. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ ((πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ ((πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©) β§ ((πΆ Btwn β¨π, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) β§ (πΆ Btwn β¨π, π β© β§ β¨πΆ, π β©Cgrβ¨πΆ, πΈβ©) β§ (π Btwn β¨π, πβ© β§ β¨π , πβ©Cgrβ¨π , πβ©))))) β β¨π , πβ©Cgrβ¨πΈ, π·β©) | ||
Theorem | btwnconn1lem10 35068 | Lemma for btwnconn1 35073. Now we establish a congruence that will give us π· = π when we compute π = π later on. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ ((πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ ((πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©) β§ ((πΆ Btwn β¨π, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) β§ (πΆ Btwn β¨π, π β© β§ β¨πΆ, π β©Cgrβ¨πΆ, πΈβ©) β§ (π Btwn β¨π, πβ© β§ β¨π , πβ©Cgrβ¨π , πβ©))))) β β¨π, π·β©Cgrβ¨π, πβ©) | ||
Theorem | btwnconn1lem11 35069 | Lemma for btwnconn1 35073. Now, we establish that π· and π are equidistant from πΆ. (Contributed by Scott Fenton, 8-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ ((πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ ((πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©) β§ ((πΆ Btwn β¨π, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) β§ (πΆ Btwn β¨π, π β© β§ β¨πΆ, π β©Cgrβ¨πΆ, πΈβ©) β§ (π Btwn β¨π, πβ© β§ β¨π , πβ©Cgrβ¨π , πβ©))))) β β¨π·, πΆβ©Cgrβ¨π, πΆβ©) | ||
Theorem | btwnconn1lem12 35070 | Lemma for btwnconn1 35073. Using a long string of invocations of linecgr 35053, we show that π· = π. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ ((πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ πΈ β (πΌβπ))) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©))) β§ ((πΈ Btwn β¨πΆ, πβ© β§ πΈ Btwn β¨π·, πβ©) β§ ((πΆ Btwn β¨π, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) β§ (πΆ Btwn β¨π, π β© β§ β¨πΆ, π β©Cgrβ¨πΆ, πΈβ©) β§ (π Btwn β¨π, πβ© β§ β¨π , πβ©Cgrβ¨π , πβ©))))) β π· = π) | ||
Theorem | btwnconn1lem13 35071 | Lemma for btwnconn1 35073. Begin back-filling and eliminating hypotheses. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ ((((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ ((πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ)))) β§ (((π΄ β π΅ β§ π΅ β πΆ) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©)) β§ ((π· Btwn β¨π΄, πβ© β§ β¨π·, πβ©Cgrβ¨πΆ, π·β©) β§ (πΆ Btwn β¨π΄, πβ© β§ β¨πΆ, πβ©Cgrβ¨πΆ, π·β©)) β§ ((π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨πΆ, π΅β©) β§ (π Btwn β¨π΄, πβ© β§ β¨π, πβ©Cgrβ¨π·, π΅β©)))) β (πΆ = π β¨ π· = π)) | ||
Theorem | btwnconn1lem14 35072 | Lemma for btwnconn1 35073. Final statement of the theorem when π΅ β πΆ. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β§ ((π΄ β π΅ β§ π΅ β πΆ) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©))) β (πΆ Btwn β¨π΄, π·β© β¨ π· Btwn β¨π΄, πΆβ©)) | ||
Theorem | btwnconn1 35073 | Connectitivy law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΄ β π΅ β§ π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©) β (πΆ Btwn β¨π΄, π·β© β¨ π· Btwn β¨π΄, πΆβ©))) | ||
Theorem | btwnconn2 35074 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΄ β π΅ β§ π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©) β (πΆ Btwn β¨π΅, π·β© β¨ π· Btwn β¨π΅, πΆβ©))) | ||
Theorem | btwnconn3 35075 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ Btwn β¨π΄, π·β© β§ πΆ Btwn β¨π΄, π·β©) β (π΅ Btwn β¨π΄, πΆβ© β¨ πΆ Btwn β¨π΄, π΅β©))) | ||
Theorem | midofsegid 35076 | 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.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ))) β ((π· Btwn β¨π΄, π΅β© β§ πΈ Btwn β¨π΄, π΅β© β§ β¨π΄, π·β©Cgrβ¨π΄, πΈβ©) β π· = πΈ)) | ||
Theorem | segcon2 35077* | Generalization of axsegcon 28185. This time, we generate an endpoint for a segment on the ray ππ΄ congruent to π΅πΆ and starting at π, as opposed to axsegcon 28185, where the segment starts at π΄ (Contributed by Scott Fenton, 14-Oct-2013.) Remove unneeded inequality. (Revised by Scott Fenton, 15-Oct-2013.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β βπ₯ β (πΌβπ)((π΄ Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π΄β©) β§ β¨π, π₯β©Cgrβ¨π΅, πΆβ©)) | ||
Syntax | csegle 35078 | Declare the constant for the segment less than or equal to relationship. |
class Segβ€ | ||
Definition | df-segle 35079* | 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.) |
β’ Segβ€ = {β¨π, πβ© β£ βπ β β βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)(π = β¨π, πβ© β§ π = β¨π, πβ© β§ βπ¦ β (πΌβπ)(π¦ Btwn β¨π, πβ© β§ β¨π, πβ©Cgrβ¨π, π¦β©))} | ||
Theorem | brsegle 35080* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β βπ¦ β (πΌβπ)(π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©))) | ||
Theorem | brsegle2 35081* | Alternate characterization of segment comparison. Theorem 5.5 of [Schwabhauser] p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β βπ₯ β (πΌβπ)(π΅ Btwn β¨π΄, π₯β© β§ β¨π΄, π₯β©Cgrβ¨πΆ, π·β©))) | ||
Theorem | seglecgr12im 35082 | Substitution law for segment comparison under congruence. Theorem 5.6 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΊ, π»β© β§ β¨π΄, π΅β© Segβ€ β¨πΆ, π·β©) β β¨πΈ, πΉβ© Segβ€ β¨πΊ, π»β©)) | ||
Theorem | seglecgr12 35083 | 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β¨πΊ, π»β©) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β β¨πΈ, πΉβ© Segβ€ β¨πΊ, π»β©))) | ||
Theorem | seglerflx 35084 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β© Segβ€ β¨π΄, π΅β©) | ||
Theorem | seglemin 35085 | 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.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β β¨π΄, π΄β© Segβ€ β¨π΅, πΆβ©) | ||
Theorem | segletr 35086 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ©) β β¨π΄, π΅β© Segβ€ β¨πΈ, πΉβ©)) | ||
Theorem | segleantisym 35087 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨π΄, π΅β©) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©)) | ||
Theorem | seglelin 35088 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β¨ β¨πΆ, π·β© Segβ€ β¨π΄, π΅β©)) | ||
Theorem | btwnsegle 35089 | If π΅ falls between π΄ and πΆ, then π΄π΅ is no longer than π΄πΆ. (Contributed by Scott Fenton, 16-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΅ Btwn β¨π΄, πΆβ© β β¨π΄, π΅β© Segβ€ β¨π΄, πΆβ©)) | ||
Theorem | colinbtwnle 35090 | 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.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β (π΅ Btwn β¨π΄, πΆβ© β (β¨π΄, π΅β© Segβ€ β¨π΄, πΆβ© β§ β¨π΅, πΆβ© Segβ€ β¨π΄, πΆβ©)))) | ||
Syntax | coutsideof 35091 | Declare the syntax for the outside of constant. |
class OutsideOf | ||
Definition | df-outsideof 35092 | 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 = ( Colinear β Btwn ) | ||
Theorem | broutsideof 35093 | 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β¨π΄, π΅β© β (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) | ||
Theorem | broutsideof2 35094 | 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β¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) | ||
Theorem | outsidene1 35095 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β π΄ β π)) | ||
Theorem | outsidene2 35096 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β π΅ β π)) | ||
Theorem | btwnoutside 35097 | 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.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π Btwn β¨π΄, πΆβ©) β (π Btwn β¨π΅, πΆβ© β πOutsideOfβ¨π΄, π΅β©))) | ||
Theorem | broutsideof3 35098* | 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β¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) | ||
Theorem | outsideofrflx 35099 | Reflexivity 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 35100 | Commutativity 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β¨π΅, π΄β©)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |