![]() |
Metamath
Proof Explorer Theorem List (p. 337 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | btwndiff 33601* | There is always a 𝑐 distinct from 𝐵 such that 𝐵 lies between 𝐴 and 𝑐. Theorem 3.14 of [Schwabhauser] p. 32. (Contributed by Scott Fenton, 24-Sep-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑐〉 ∧ 𝐵 ≠ 𝑐)) | ||
Theorem | trisegint 33602* | 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 33603 | Declare the syntax for the segment transport function. |
class TransportTo | ||
Definition | df-transport 33604* | Define the segment transport function. See fvtransport 33606 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.) |
⊢ TransportTo = {〈〈𝑝, 𝑞〉, 𝑥〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn 〈(1st ‘𝑞), 𝑟〉 ∧ 〈(2nd ‘𝑞), 𝑟〉Cgr𝑝)))} | ||
Theorem | funtransport 33605 | The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun TransportTo | ||
Theorem | fvtransport 33606* | 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 33607 | Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → (〈𝐴, 𝐵〉TransportTo〈𝐶, 𝐷〉) ∈ (𝔼‘𝑁)) | ||
Theorem | transportprops 33608 | 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 33609 | Declare the syntax for the inner five segment predicate. |
class InnerFiveSeg | ||
Syntax | ccgr3 33610 | Declare the syntax for the three place congruence predicate. |
class Cgr3 | ||
Syntax | ccolin 33611 | Declare the syntax for the colinearity predicate. |
class Colinear | ||
Syntax | cfs 33612 | Declare the syntax for the five segment predicate. |
class FiveSeg | ||
Definition | df-colinear 33613* | 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 33614* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 33617 and ifscgr 33618 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 33615* | 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 33616* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 33653 and fscgr 33654 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ FiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ (𝑎 Colinear 〈𝑏, 𝑐〉 ∧ 〈𝑎, 〈𝑏, 𝑐〉〉Cgr3〈𝑥, 〈𝑦, 𝑧〉〉 ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
Theorem | brifs 33617 | 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 33618 | 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 33619 | 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 33620 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉))) | ||
Theorem | cgr3permute3 33621 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐶, 𝐴〉〉Cgr3〈𝐸, 〈𝐹, 𝐷〉〉)) | ||
Theorem | cgr3permute1 33622 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐴, 〈𝐶, 𝐵〉〉Cgr3〈𝐷, 〈𝐹, 𝐸〉〉)) | ||
Theorem | cgr3permute2 33623 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐴, 𝐶〉〉Cgr3〈𝐸, 〈𝐷, 𝐹〉〉)) | ||
Theorem | cgr3permute4 33624 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐴, 𝐵〉〉Cgr3〈𝐹, 〈𝐷, 𝐸〉〉)) | ||
Theorem | cgr3permute5 33625 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐵, 𝐴〉〉Cgr3〈𝐹, 〈𝐸, 𝐷〉〉)) | ||
Theorem | cgr3tr4 33626 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (𝔼‘𝑁)))) → ((〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉) → 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉)) | ||
Theorem | cgr3com 33627 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉)) | ||
Theorem | cgr3rflx 33628 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉) | ||
Theorem | cgrxfr 33629* | 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 33630 | 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 33631 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Rel Colinear | ||
Theorem | brcolinear2 33632* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) | ||
Theorem | brcolinear 33633 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉))) | ||
Theorem | colinearex 33634 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Colinear ∈ V | ||
Theorem | colineardim1 33635 | 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 33636 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | colinearperm3 33637 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | colinearperm2 33638 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | colinearperm4 33639 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | colinearperm5 33640 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colineartriv1 33641 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐴, 𝐵〉) | ||
Theorem | colineartriv2 33642 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐵, 𝐵〉) | ||
Theorem | btwncolinear1 33643 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐵, 𝐶〉)) | ||
Theorem | btwncolinear2 33644 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | btwncolinear3 33645 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | btwncolinear4 33646 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | btwncolinear5 33647 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | btwncolinear6 33648 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colinearxfr 33649 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Colinear 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉) → 𝐸 Colinear 〈𝐷, 𝐹〉)) | ||
Theorem | lineext 33650* | 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 33651 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | brifs2 33652 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 InnerFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) | ||
Theorem | brfs 33653 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 FiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐴 Colinear 〈𝐵, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | fscgr 33654 | 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 33655 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝐵 ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) ∧ (〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉 ∧ 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉)) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉)) | ||
Theorem | linecgrand 33656 | Deduction form of linecgr 33655. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑃 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑄 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≠ 𝐵) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Colinear 〈𝐵, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉) | ||
Theorem | lineid 33657 | 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 33658 | 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 33659 | If 𝐴, 𝐵, and 𝐶 fall in order on a line, and 𝐴𝐵 and 𝐴𝐶 are congruent, then 𝐶 = 𝐵. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐶 = 𝐵)) | ||
Theorem | endofsegidand 33660 | Deduction form of endofsegid 33659. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 = 𝐶) | ||
Theorem | btwnconn1lem1 33661 | Lemma for btwnconn1 33675. 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 33662 | Lemma for btwnconn1 33675. 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 33663 | Lemma for btwnconn1 33675. 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 33664 | Lemma for btwnconn1 33675. 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 33665 | Lemma for btwnconn1 33675. 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 33666 | Lemma for btwnconn1 33675. 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 33667 | Lemma for btwnconn1 33675. 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 33668 | Lemma for btwnconn1 33675. 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 33669 | Lemma for btwnconn1 33675. 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 33670 | Lemma for btwnconn1 33675. 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 33671 | Lemma for btwnconn1 33675. 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 33672 | Lemma for btwnconn1 33675. Using a long string of invocations of linecgr 33655, 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 33673 | Lemma for btwnconn1 33675. 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 33674 | Lemma for btwnconn1 33675. Final statement of the theorem when 𝐵 ≠ 𝐶. (Contributed by Scott Fenton, 9-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnconn1 33675 | 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 33676 | 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 33677 | 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 33678 | 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 33679* | Generalization of axsegcon 26721. This time, we generate an endpoint for a segment on the ray 𝑄𝐴 congruent to 𝐵𝐶 and starting at 𝑄, as opposed to axsegcon 26721, 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 33680 | Declare the constant for the segment less than or equal to relationship. |
class Seg≤ | ||
Definition | df-segle 33681* | 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 33682* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) | ||
Theorem | brsegle2 33683* | 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 33684 | 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 33685 | 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 33686 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐵〉) | ||
Theorem | seglemin 33687 | 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 33688 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) | ||
Theorem | segleantisym 33689 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
Theorem | seglelin 33690 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉)) | ||
Theorem | btwnsegle 33691 | 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 33692 | 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 33693 | Declare the syntax for the outside of constant. |
class OutsideOf | ||
Definition | df-outsideof 33694 | 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 33695 | 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 33696 | 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 33697 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐴 ≠ 𝑃)) | ||
Theorem | outsidene2 33698 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐵 ≠ 𝑃)) | ||
Theorem | btwnoutside 33699 | 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 33700* | 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 〈𝐵, 𝑐〉)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |