![]() |
Metamath
Proof Explorer Theorem List (p. 361 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | btwnexch3 36001 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → 𝐶 Btwn 〈𝐵, 𝐷〉)) | ||
Theorem | btwnexch3and 36002 | Deduction form of btwnexch3 36001. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐵, 𝐷〉) | ||
Theorem | btwnouttr2 36003 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexch2 36004 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnouttr 36005 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexch 36006 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 24-Sep-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexchand 36007 | Deduction form of btwnexch 36006. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐷〉) | ||
Theorem | btwndiff 36008* | 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 36009* | 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 36010 | Declare the syntax for the segment transport function. |
class TransportTo | ||
Definition | df-transport 36011* | Define the segment transport function. See fvtransport 36013 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.) |
⊢ TransportTo = {〈〈𝑝, 𝑞〉, 𝑥〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn 〈(1st ‘𝑞), 𝑟〉 ∧ 〈(2nd ‘𝑞), 𝑟〉Cgr𝑝)))} | ||
Theorem | funtransport 36012 | The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun TransportTo | ||
Theorem | fvtransport 36013* | 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 36014 | Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → (〈𝐴, 𝐵〉TransportTo〈𝐶, 𝐷〉) ∈ (𝔼‘𝑁)) | ||
Theorem | transportprops 36015 | 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 36016 | Declare the syntax for the inner five segment predicate. |
class InnerFiveSeg | ||
Syntax | ccgr3 36017 | Declare the syntax for the three place congruence predicate. |
class Cgr3 | ||
Syntax | ccolin 36018 | Declare the syntax for the colinearity predicate. |
class Colinear | ||
Syntax | cfs 36019 | Declare the syntax for the five segment predicate. |
class FiveSeg | ||
Definition | df-colinear 36020* | 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 36021* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 36024 and ifscgr 36025 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 36022* | 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 36023* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 36060 and fscgr 36061 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ FiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ (𝑎 Colinear 〈𝑏, 𝑐〉 ∧ 〈𝑎, 〈𝑏, 𝑐〉〉Cgr3〈𝑥, 〈𝑦, 𝑧〉〉 ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
Theorem | brifs 36024 | 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 36025 | 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 36026 | 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 36027 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉))) | ||
Theorem | cgr3permute3 36028 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐶, 𝐴〉〉Cgr3〈𝐸, 〈𝐹, 𝐷〉〉)) | ||
Theorem | cgr3permute1 36029 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐴, 〈𝐶, 𝐵〉〉Cgr3〈𝐷, 〈𝐹, 𝐸〉〉)) | ||
Theorem | cgr3permute2 36030 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐴, 𝐶〉〉Cgr3〈𝐸, 〈𝐷, 𝐹〉〉)) | ||
Theorem | cgr3permute4 36031 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐴, 𝐵〉〉Cgr3〈𝐹, 〈𝐷, 𝐸〉〉)) | ||
Theorem | cgr3permute5 36032 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐵, 𝐴〉〉Cgr3〈𝐹, 〈𝐸, 𝐷〉〉)) | ||
Theorem | cgr3tr4 36033 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (𝔼‘𝑁)))) → ((〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉) → 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉)) | ||
Theorem | cgr3com 36034 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉)) | ||
Theorem | cgr3rflx 36035 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉) | ||
Theorem | cgrxfr 36036* | 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 36037 | 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 36038 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Rel Colinear | ||
Theorem | brcolinear2 36039* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) | ||
Theorem | brcolinear 36040 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉))) | ||
Theorem | colinearex 36041 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Colinear ∈ V | ||
Theorem | colineardim1 36042 | 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 36043 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | colinearperm3 36044 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | colinearperm2 36045 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | colinearperm4 36046 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | colinearperm5 36047 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colineartriv1 36048 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐴, 𝐵〉) | ||
Theorem | colineartriv2 36049 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐵, 𝐵〉) | ||
Theorem | btwncolinear1 36050 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐵, 𝐶〉)) | ||
Theorem | btwncolinear2 36051 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | btwncolinear3 36052 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | btwncolinear4 36053 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | btwncolinear5 36054 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | btwncolinear6 36055 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colinearxfr 36056 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Colinear 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉) → 𝐸 Colinear 〈𝐷, 𝐹〉)) | ||
Theorem | lineext 36057* | 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 36058 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | brifs2 36059 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 InnerFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) | ||
Theorem | brfs 36060 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 FiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐴 Colinear 〈𝐵, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | fscgr 36061 | 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 36062 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝐵 ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) ∧ (〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉 ∧ 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉)) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉)) | ||
Theorem | linecgrand 36063 | Deduction form of linecgr 36062. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑃 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑄 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≠ 𝐵) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Colinear 〈𝐵, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉) | ||
Theorem | lineid 36064 | 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 36065 | 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 36066 | If 𝐴, 𝐵, and 𝐶 fall in order on a line, and 𝐴𝐵 and 𝐴𝐶 are congruent, then 𝐶 = 𝐵. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐶 = 𝐵)) | ||
Theorem | endofsegidand 36067 | Deduction form of endofsegid 36066. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 = 𝐶) | ||
Theorem | btwnconn1lem1 36068 | Lemma for btwnconn1 36082. 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 36069 | Lemma for btwnconn1 36082. 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 36070 | Lemma for btwnconn1 36082. 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 36071 | Lemma for btwnconn1 36082. 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 36072 | Lemma for btwnconn1 36082. 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 36073 | Lemma for btwnconn1 36082. 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 36074 | Lemma for btwnconn1 36082. 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 36075 | Lemma for btwnconn1 36082. 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 36076 | Lemma for btwnconn1 36082. 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 36077 | Lemma for btwnconn1 36082. 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 36078 | Lemma for btwnconn1 36082. 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 36079 | Lemma for btwnconn1 36082. Using a long string of invocations of linecgr 36062, 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 36080 | Lemma for btwnconn1 36082. 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 36081 | Lemma for btwnconn1 36082. Final statement of the theorem when 𝐵 ≠ 𝐶. (Contributed by Scott Fenton, 9-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnconn1 36082 | 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 36083 | 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 36084 | 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 36085 | 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 36086* | Generalization of axsegcon 28956. This time, we generate an endpoint for a segment on the ray 𝑄𝐴 congruent to 𝐵𝐶 and starting at 𝑄, as opposed to axsegcon 28956, 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 36087 | Declare the constant for the segment less than or equal to relationship. |
class Seg≤ | ||
Definition | df-segle 36088* | 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 36089* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) | ||
Theorem | brsegle2 36090* | 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 36091 | 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 36092 | 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 36093 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐵〉) | ||
Theorem | seglemin 36094 | 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 36095 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) | ||
Theorem | segleantisym 36096 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
Theorem | seglelin 36097 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉)) | ||
Theorem | btwnsegle 36098 | 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 36099 | 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 36100 | Declare the syntax for the outside of constant. |
class OutsideOf |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |