![]() |
Metamath
Proof Explorer Theorem List (p. 354 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | trisegint 35301* | A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of [Schwabhauser] p. 33. (Contributed by Scott Fenton, 24-Sep-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©))) | ||
Syntax | ctransport 35302 | Declare the syntax for the segment transport function. |
class TransportTo | ||
Definition | df-transport 35303* | Define the segment transport function. See fvtransport 35305 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.) |
β’ TransportTo = {β¨β¨π, πβ©, π₯β© β£ βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st βπ), πβ© β§ β¨(2nd βπ), πβ©Cgrπ)))} | ||
Theorem | funtransport 35304 | The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun TransportTo | ||
Theorem | fvtransport 35305* | 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 35306 | Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β (β¨π΄, π΅β©TransportToβ¨πΆ, π·β©) β (πΌβπ)) | ||
Theorem | transportprops 35307 | 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 35308 | Declare the syntax for the inner five segment predicate. |
class InnerFiveSeg | ||
Syntax | ccgr3 35309 | Declare the syntax for the three place congruence predicate. |
class Cgr3 | ||
Syntax | ccolin 35310 | Declare the syntax for the colinearity predicate. |
class Colinear | ||
Syntax | cfs 35311 | Declare the syntax for the five segment predicate. |
class FiveSeg | ||
Definition | df-colinear 35312* | 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 35313* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 35316 and ifscgr 35317 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 35314* | 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 35315* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 35352 and fscgr 35353 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ FiveSeg = {β¨π, πβ© β£ βπ β β βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ₯ β (πΌβπ)βπ¦ β (πΌβπ)βπ§ β (πΌβπ)βπ€ β (πΌβπ)(π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π₯, π¦β©, β¨π§, π€β©β© β§ (π Colinear β¨π, πβ© β§ β¨π, β¨π, πβ©β©Cgr3β¨π₯, β¨π¦, π§β©β© β§ (β¨π, πβ©Cgrβ¨π₯, π€β© β§ β¨π, πβ©Cgrβ¨π¦, π€β©)))} | ||
Theorem | brifs 35316 | 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 35317 | 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 35318 | 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 35319 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β (β¨π΄, π΅β©Cgrβ¨π·, πΈβ© β§ β¨π΄, πΆβ©Cgrβ¨π·, πΉβ© β§ β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©))) | ||
Theorem | cgr3permute3 35320 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π΅, β¨πΆ, π΄β©β©Cgr3β¨πΈ, β¨πΉ, π·β©β©)) | ||
Theorem | cgr3permute1 35321 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π΄, β¨πΆ, π΅β©β©Cgr3β¨π·, β¨πΉ, πΈβ©β©)) | ||
Theorem | cgr3permute2 35322 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π΅, β¨π΄, πΆβ©β©Cgr3β¨πΈ, β¨π·, πΉβ©β©)) | ||
Theorem | cgr3permute4 35323 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨πΆ, β¨π΄, π΅β©β©Cgr3β¨πΉ, β¨π·, πΈβ©β©)) | ||
Theorem | cgr3permute5 35324 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨πΆ, β¨π΅, π΄β©β©Cgr3β¨πΉ, β¨πΈ, π·β©β©)) | ||
Theorem | cgr3tr4 35325 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ)) β§ (πΊ β (πΌβπ) β§ π» β (πΌβπ) β§ πΌ β (πΌβπ)))) β ((β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΊ, β¨π», πΌβ©β©) β β¨π·, β¨πΈ, πΉβ©β©Cgr3β¨πΊ, β¨π», πΌβ©β©)) | ||
Theorem | cgr3com 35326 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β© β β¨π·, β¨πΈ, πΉβ©β©Cgr3β¨π΄, β¨π΅, πΆβ©β©)) | ||
Theorem | cgr3rflx 35327 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π΄, β¨π΅, πΆβ©β©) | ||
Theorem | cgrxfr 35328* | 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 35329 | 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 35330 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Rel Colinear | ||
Theorem | brcolinear2 35331* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β π β§ π β π) β (π Colinear β¨π, π β© β βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ (π Btwn β¨π, π β© β¨ π Btwn β¨π , πβ© β¨ π Btwn β¨π, πβ©)))) | ||
Theorem | brcolinear 35332 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β (π΄ Btwn β¨π΅, πΆβ© β¨ π΅ Btwn β¨πΆ, π΄β© β¨ πΆ Btwn β¨π΄, π΅β©))) | ||
Theorem | colinearex 35333 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Colinear β V | ||
Theorem | colineardim1 35334 | 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 35335 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β π΄ Colinear β¨πΆ, π΅β©)) | ||
Theorem | colinearperm3 35336 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β π΅ Colinear β¨πΆ, π΄β©)) | ||
Theorem | colinearperm2 35337 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β π΅ Colinear β¨π΄, πΆβ©)) | ||
Theorem | colinearperm4 35338 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β πΆ Colinear β¨π΄, π΅β©)) | ||
Theorem | colinearperm5 35339 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Colinear β¨π΅, πΆβ© β πΆ Colinear β¨π΅, π΄β©)) | ||
Theorem | colineartriv1 35340 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Colinear β¨π΄, π΅β©) | ||
Theorem | colineartriv2 35341 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Colinear β¨π΅, π΅β©) | ||
Theorem | btwncolinear1 35342 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΄ Colinear β¨π΅, πΆβ©)) | ||
Theorem | btwncolinear2 35343 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΄ Colinear β¨πΆ, π΅β©)) | ||
Theorem | btwncolinear3 35344 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΅ Colinear β¨π΄, πΆβ©)) | ||
Theorem | btwncolinear4 35345 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β π΅ Colinear β¨πΆ, π΄β©)) | ||
Theorem | btwncolinear5 35346 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β πΆ Colinear β¨π΄, π΅β©)) | ||
Theorem | btwncolinear6 35347 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΆ Btwn β¨π΄, π΅β© β πΆ Colinear β¨π΅, π΄β©)) | ||
Theorem | colinearxfr 35348 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((π΅ Colinear β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨π·, β¨πΈ, πΉβ©β©) β πΈ Colinear β¨π·, πΉβ©)) | ||
Theorem | lineext 35349* | 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 35350 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β (π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΈ, β¨πΉ, πΊβ©β© β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨π΅, π·β©Cgrβ¨πΉ, π»β©)))) | ||
Theorem | brifs2 35351 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© InnerFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β (π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΈ, β¨πΉ, πΊβ©β© β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)))) | ||
Theorem | brfs 35352 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© FiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β (π΄ Colinear β¨π΅, πΆβ© β§ β¨π΄, β¨π΅, πΆβ©β©Cgr3β¨πΈ, β¨πΉ, πΊβ©β© β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨π΅, π·β©Cgrβ¨πΉ, π»β©)))) | ||
Theorem | fscgr 35353 | 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 35354 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β (((π΄ β π΅ β§ π΄ Colinear β¨π΅, πΆβ©) β§ (β¨π΄, πβ©Cgrβ¨π΄, πβ© β§ β¨π΅, πβ©Cgrβ¨π΅, πβ©)) β β¨πΆ, πβ©Cgrβ¨πΆ, πβ©)) | ||
Theorem | linecgrand 35355 | Deduction form of linecgr 35354. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π β (πΌβπ)) & β’ (π β π β (πΌβπ)) & β’ ((π β§ π) β π΄ β π΅) & β’ ((π β§ π) β π΄ Colinear β¨π΅, πΆβ©) & β’ ((π β§ π) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) & β’ ((π β§ π) β β¨π΅, πβ©Cgrβ¨π΅, πβ©) β β’ ((π β§ π) β β¨πΆ, πβ©Cgrβ¨πΆ, πβ©) | ||
Theorem | lineid 35356 | 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 35357 | 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 35358 | If π΄, π΅, and πΆ fall in order on a line, and π΄π΅ and π΄πΆ are congruent, then πΆ = π΅. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ β¨π΄, πΆβ©Cgrβ¨π΄, π΅β©) β πΆ = π΅)) | ||
Theorem | endofsegidand 35359 | Deduction form of endofsegid 35358. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ ((π β§ π) β πΆ Btwn β¨π΄, π΅β©) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨π΄, πΆβ©) β β’ ((π β§ π) β π΅ = πΆ) | ||
Theorem | btwnconn1lem1 35360 | Lemma for btwnconn1 35374. 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 35361 | Lemma for btwnconn1 35374. 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 35362 | Lemma for btwnconn1 35374. 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 35363 | Lemma for btwnconn1 35374. 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 35364 | Lemma for btwnconn1 35374. 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 35365 | Lemma for btwnconn1 35374. 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 35366 | Lemma for btwnconn1 35374. 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 35367 | Lemma for btwnconn1 35374. 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 35368 | Lemma for btwnconn1 35374. 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 35369 | Lemma for btwnconn1 35374. 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 35370 | Lemma for btwnconn1 35374. 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 35371 | Lemma for btwnconn1 35374. Using a long string of invocations of linecgr 35354, 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 35372 | Lemma for btwnconn1 35374. 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 35373 | Lemma for btwnconn1 35374. Final statement of the theorem when π΅ β πΆ. (Contributed by Scott Fenton, 9-Oct-2013.) |
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β§ ((π΄ β π΅ β§ π΅ β πΆ) β§ (π΅ Btwn β¨π΄, πΆβ© β§ π΅ Btwn β¨π΄, π·β©))) β (πΆ Btwn β¨π΄, π·β© β¨ π· Btwn β¨π΄, πΆβ©)) | ||
Theorem | btwnconn1 35374 | 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 35375 | 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 35376 | 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 35377 | 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 35378* | Generalization of axsegcon 28449. This time, we generate an endpoint for a segment on the ray ππ΄ congruent to π΅πΆ and starting at π, as opposed to axsegcon 28449, 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 35379 | Declare the constant for the segment less than or equal to relationship. |
class Segβ€ | ||
Definition | df-segle 35380* | 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 35381* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β βπ¦ β (πΌβπ)(π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©))) | ||
Theorem | brsegle2 35382* | 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 35383 | 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 35384 | 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 35385 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β© Segβ€ β¨π΄, π΅β©) | ||
Theorem | seglemin 35386 | 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 35387 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ©) β β¨π΄, π΅β© Segβ€ β¨πΈ, πΉβ©)) | ||
Theorem | segleantisym 35388 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨π΄, π΅β©) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©)) | ||
Theorem | seglelin 35389 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β¨ β¨πΆ, π·β© Segβ€ β¨π΄, π΅β©)) | ||
Theorem | btwnsegle 35390 | 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 35391 | 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 35392 | Declare the syntax for the outside of constant. |
class OutsideOf | ||
Definition | df-outsideof 35393 | 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 35394 | 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 35395 | 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 35396 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β π΄ β π)) | ||
Theorem | outsidene2 35397 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β π΅ β π)) | ||
Theorem | btwnoutside 35398 | 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 35399* | 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 35400 | 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β¨π΄, π΄β©)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |