Home | Metamath
Proof Explorer Theorem List (p. 336 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-ifs 33501* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 33504 and ifscgr 33505 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 33502* | 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 33503* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 33540 and fscgr 33541 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ FiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ (𝑎 Colinear 〈𝑏, 𝑐〉 ∧ 〈𝑎, 〈𝑏, 𝑐〉〉Cgr3〈𝑥, 〈𝑦, 𝑧〉〉 ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
Theorem | brifs 33504 | 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 33505 | 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 33506 | 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 33507 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉))) | ||
Theorem | cgr3permute3 33508 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐶, 𝐴〉〉Cgr3〈𝐸, 〈𝐹, 𝐷〉〉)) | ||
Theorem | cgr3permute1 33509 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐴, 〈𝐶, 𝐵〉〉Cgr3〈𝐷, 〈𝐹, 𝐸〉〉)) | ||
Theorem | cgr3permute2 33510 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐴, 𝐶〉〉Cgr3〈𝐸, 〈𝐷, 𝐹〉〉)) | ||
Theorem | cgr3permute4 33511 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐴, 𝐵〉〉Cgr3〈𝐹, 〈𝐷, 𝐸〉〉)) | ||
Theorem | cgr3permute5 33512 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐵, 𝐴〉〉Cgr3〈𝐹, 〈𝐸, 𝐷〉〉)) | ||
Theorem | cgr3tr4 33513 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (𝔼‘𝑁)))) → ((〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉) → 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉)) | ||
Theorem | cgr3com 33514 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉)) | ||
Theorem | cgr3rflx 33515 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉) | ||
Theorem | cgrxfr 33516* | 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 33517 | 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 33518 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Rel Colinear | ||
Theorem | brcolinear2 33519* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) | ||
Theorem | brcolinear 33520 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉))) | ||
Theorem | colinearex 33521 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Colinear ∈ V | ||
Theorem | colineardim1 33522 | 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 33523 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | colinearperm3 33524 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | colinearperm2 33525 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | colinearperm4 33526 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | colinearperm5 33527 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colineartriv1 33528 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐴, 𝐵〉) | ||
Theorem | colineartriv2 33529 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐵, 𝐵〉) | ||
Theorem | btwncolinear1 33530 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐵, 𝐶〉)) | ||
Theorem | btwncolinear2 33531 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | btwncolinear3 33532 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | btwncolinear4 33533 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | btwncolinear5 33534 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | btwncolinear6 33535 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colinearxfr 33536 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Colinear 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉) → 𝐸 Colinear 〈𝐷, 𝐹〉)) | ||
Theorem | lineext 33537* | 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 33538 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | brifs2 33539 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 InnerFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) | ||
Theorem | brfs 33540 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 FiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐴 Colinear 〈𝐵, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | fscgr 33541 | 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 33542 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝐵 ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) ∧ (〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉 ∧ 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉)) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉)) | ||
Theorem | linecgrand 33543 | Deduction form of linecgr 33542. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑃 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑄 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≠ 𝐵) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Colinear 〈𝐵, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉) | ||
Theorem | lineid 33544 | 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 33545 | 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 33546 | If 𝐴, 𝐵, and 𝐶 fall in order on a line, and 𝐴𝐵 and 𝐴𝐶 are congruent, then 𝐶 = 𝐵. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐶 = 𝐵)) | ||
Theorem | endofsegidand 33547 | Deduction form of endofsegid 33546. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 = 𝐶) | ||
Theorem | btwnconn1lem1 33548 | Lemma for btwnconn1 33562. 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 33549 | Lemma for btwnconn1 33562. 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 33550 | Lemma for btwnconn1 33562. 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 33551 | Lemma for btwnconn1 33562. 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 33552 | Lemma for btwnconn1 33562. 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 33553 | Lemma for btwnconn1 33562. 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 33554 | Lemma for btwnconn1 33562. 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 33555 | Lemma for btwnconn1 33562. 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 33556 | Lemma for btwnconn1 33562. 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 33557 | Lemma for btwnconn1 33562. 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 33558 | Lemma for btwnconn1 33562. 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 33559 | Lemma for btwnconn1 33562. Using a long string of invocations of linecgr 33542, 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 33560 | Lemma for btwnconn1 33562. 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 33561 | Lemma for btwnconn1 33562. Final statement of the theorem when 𝐵 ≠ 𝐶. (Contributed by Scott Fenton, 9-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnconn1 33562 | 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 33563 | 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 33564 | 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 33565 | 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 33566* | Generalization of axsegcon 26713. This time, we generate an endpoint for a segment on the ray 𝑄𝐴 congruent to 𝐵𝐶 and starting at 𝑄, as opposed to axsegcon 26713, 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 33567 | Declare the constant for the segment less than or equal to relationship. |
class Seg≤ | ||
Definition | df-segle 33568* | 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 33569* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) | ||
Theorem | brsegle2 33570* | 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 33571 | 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 33572 | 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 33573 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐵〉) | ||
Theorem | seglemin 33574 | 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 33575 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) | ||
Theorem | segleantisym 33576 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
Theorem | seglelin 33577 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉)) | ||
Theorem | btwnsegle 33578 | 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 33579 | 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 33580 | Declare the syntax for the outside of constant. |
class OutsideOf | ||
Definition | df-outsideof 33581 | 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 33582 | 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 33583 | 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 33584 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐴 ≠ 𝑃)) | ||
Theorem | outsidene2 33585 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐵 ≠ 𝑃)) | ||
Theorem | btwnoutside 33586 | 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 33587* | 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 33588 | Reflexitivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴 ≠ 𝑃 → 𝑃OutsideOf〈𝐴, 𝐴〉)) | ||
Theorem | outsideofcom 33589 | Commutitivity law for outsideness. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ 𝑃OutsideOf〈𝐵, 𝐴〉)) | ||
Theorem | outsideoftr 33590 | Transitivity law for outsideness. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) → 𝑃OutsideOf〈𝐴, 𝐶〉)) | ||
Theorem | outsideofeq 33591 | Uniqueness law for OutsideOf. Analogue of segconeq 33471. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → (((𝐴OutsideOf〈𝑋, 𝑅〉 ∧ 〈𝐴, 𝑋〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑌, 𝑅〉 ∧ 〈𝐴, 𝑌〉Cgr〈𝐵, 𝐶〉)) → 𝑋 = 𝑌)) | ||
Theorem | outsideofeu 33592* | Given a nondegenerate ray, there is a unique point congruent to the segment 𝐵𝐶 lying on the ray 𝐴𝑅. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) | ||
Theorem | outsidele 33593 | Relate OutsideOf to Seg≤. Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ 𝐴 Btwn 〈𝑃, 𝐵〉))) | ||
Theorem | outsideofcol 33594 | Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝑃OutsideOf〈𝑄, 𝑅〉 → 𝑃 Colinear 〈𝑄, 𝑅〉) | ||
Syntax | cline2 33595 | Declare the constant for the line function. |
class Line | ||
Syntax | cray 33596 | Declare the constant for the ray function. |
class Ray | ||
Syntax | clines2 33597 | Declare the constant for the set of all lines. |
class LinesEE | ||
Definition | df-line2 33598* | Define the Line function. This function generates the line passing through the distinct points 𝑎 and 𝑏. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.) |
⊢ Line = {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} | ||
Definition | df-ray 33599* | Define the Ray function. This function generates the set of all points that lie on the ray starting at 𝑝 and passing through 𝑎. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.) |
⊢ Ray = {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} | ||
Definition | df-lines2 33600 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 33613 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
⊢ LinesEE = ran Line |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |