![]() |
Metamath
Proof Explorer Theorem List (p. 347 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | btwntriv1 34601 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Btwn 〈𝐴, 𝐵〉) | ||
Theorem | btwnswapid 34602 | If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) → 𝐴 = 𝐵)) | ||
Theorem | btwnswapid2 34603 | If you can swap arguments one and three of a betweenness statement, then those arguments are identical. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐴〉) → 𝐴 = 𝐶)) | ||
Theorem | btwnintr 34604 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnexch3 34605 | 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 34606 | Deduction form of btwnexch3 34605. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐵, 𝐷〉) | ||
Theorem | btwnouttr2 34607 | 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 34608 | 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 34609 | 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 34610 | 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 34611 | Deduction form of btwnexch 34610. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐷〉) | ||
Theorem | btwndiff 34612* | 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 34613* | 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 34614 | Declare the syntax for the segment transport function. |
class TransportTo | ||
Definition | df-transport 34615* | Define the segment transport function. See fvtransport 34617 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.) |
⊢ TransportTo = {〈〈𝑝, 𝑞〉, 𝑥〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn 〈(1st ‘𝑞), 𝑟〉 ∧ 〈(2nd ‘𝑞), 𝑟〉Cgr𝑝)))} | ||
Theorem | funtransport 34616 | The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun TransportTo | ||
Theorem | fvtransport 34617* | 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 34618 | Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → (〈𝐴, 𝐵〉TransportTo〈𝐶, 𝐷〉) ∈ (𝔼‘𝑁)) | ||
Theorem | transportprops 34619 | 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 34620 | Declare the syntax for the inner five segment predicate. |
class InnerFiveSeg | ||
Syntax | ccgr3 34621 | Declare the syntax for the three place congruence predicate. |
class Cgr3 | ||
Syntax | ccolin 34622 | Declare the syntax for the colinearity predicate. |
class Colinear | ||
Syntax | cfs 34623 | Declare the syntax for the five segment predicate. |
class FiveSeg | ||
Definition | df-colinear 34624* | 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 34625* | The inner five segment configuration is an abbreviation for another congruence condition. See brifs 34628 and ifscgr 34629 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 34626* | 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 34627* | The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs 34664 and fscgr 34665 for its use. Definition 4.15 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ FiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ (𝑎 Colinear 〈𝑏, 𝑐〉 ∧ 〈𝑎, 〈𝑏, 𝑐〉〉Cgr3〈𝑥, 〈𝑦, 𝑧〉〉 ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
Theorem | brifs 34628 | 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 34629 | 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 34630 | 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 34631 | Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉))) | ||
Theorem | cgr3permute3 34632 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐶, 𝐴〉〉Cgr3〈𝐸, 〈𝐹, 𝐷〉〉)) | ||
Theorem | cgr3permute1 34633 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐴, 〈𝐶, 𝐵〉〉Cgr3〈𝐷, 〈𝐹, 𝐸〉〉)) | ||
Theorem | cgr3permute2 34634 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐵, 〈𝐴, 𝐶〉〉Cgr3〈𝐸, 〈𝐷, 𝐹〉〉)) | ||
Theorem | cgr3permute4 34635 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐴, 𝐵〉〉Cgr3〈𝐹, 〈𝐷, 𝐸〉〉)) | ||
Theorem | cgr3permute5 34636 | Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐶, 〈𝐵, 𝐴〉〉Cgr3〈𝐹, 〈𝐸, 𝐷〉〉)) | ||
Theorem | cgr3tr4 34637 | Transitivity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (𝔼‘𝑁)))) → ((〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉) → 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐺, 〈𝐻, 𝐼〉〉)) | ||
Theorem | cgr3com 34638 | Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝐸, 𝐹〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉)) | ||
Theorem | cgr3rflx 34639 | Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐵, 𝐶〉〉) | ||
Theorem | cgrxfr 34640* | 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 34641 | 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 34642 | Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Rel Colinear | ||
Theorem | brcolinear2 34643* | Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) | ||
Theorem | brcolinear 34644 | The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉))) | ||
Theorem | colinearex 34645 | The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Colinear ∈ V | ||
Theorem | colineardim1 34646 | 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 34647 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | colinearperm3 34648 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | colinearperm2 34649 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | colinearperm4 34650 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | colinearperm5 34651 | Permutation law for colinearity. Part of theorem 4.11 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colineartriv1 34652 | Trivial case of colinearity. Theorem 4.12 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐴, 𝐵〉) | ||
Theorem | colineartriv2 34653 | Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Colinear 〈𝐵, 𝐵〉) | ||
Theorem | btwncolinear1 34654 | Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐵, 𝐶〉)) | ||
Theorem | btwncolinear2 34655 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐴 Colinear 〈𝐶, 𝐵〉)) | ||
Theorem | btwncolinear3 34656 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐴, 𝐶〉)) | ||
Theorem | btwncolinear4 34657 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐵 Colinear 〈𝐶, 𝐴〉)) | ||
Theorem | btwncolinear5 34658 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐴, 𝐵〉)) | ||
Theorem | btwncolinear6 34659 | Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 𝐶 Colinear 〈𝐵, 𝐴〉)) | ||
Theorem | colinearxfr 34660 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Colinear 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝐸, 𝐹〉〉) → 𝐸 Colinear 〈𝐷, 𝐹〉)) | ||
Theorem | lineext 34661* | 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 34662 | Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | brifs2 34663 | Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 InnerFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) | ||
Theorem | brfs 34664 | Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 FiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (𝐴 Colinear 〈𝐵, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐸, 〈𝐹, 𝐺〉〉 ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | fscgr 34665 | 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 34666 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Scott Fenton, 6-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝐵 ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) ∧ (〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉 ∧ 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉)) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉)) | ||
Theorem | linecgrand 34667 | Deduction form of linecgr 34666. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑃 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝑄 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≠ 𝐵) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Colinear 〈𝐵, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝑃〉Cgr〈𝐴, 𝑄〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝑃〉Cgr〈𝐵, 𝑄〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝑃〉Cgr〈𝐶, 𝑄〉) | ||
Theorem | lineid 34668 | 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 34669 | 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 34670 | If 𝐴, 𝐵, and 𝐶 fall in order on a line, and 𝐴𝐵 and 𝐴𝐶 are congruent, then 𝐶 = 𝐵. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐶 = 𝐵)) | ||
Theorem | endofsegidand 34671 | Deduction form of endofsegid 34670. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 = 𝐶) | ||
Theorem | btwnconn1lem1 34672 | Lemma for btwnconn1 34686. 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 34673 | Lemma for btwnconn1 34686. 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 34674 | Lemma for btwnconn1 34686. 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 34675 | Lemma for btwnconn1 34686. 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 34676 | Lemma for btwnconn1 34686. 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 34677 | Lemma for btwnconn1 34686. 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 34678 | Lemma for btwnconn1 34686. 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 34679 | Lemma for btwnconn1 34686. 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 34680 | Lemma for btwnconn1 34686. 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 34681 | Lemma for btwnconn1 34686. 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 34682 | Lemma for btwnconn1 34686. 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 34683 | Lemma for btwnconn1 34686. Using a long string of invocations of linecgr 34666, 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 34684 | Lemma for btwnconn1 34686. 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 34685 | Lemma for btwnconn1 34686. Final statement of the theorem when 𝐵 ≠ 𝐶. (Contributed by Scott Fenton, 9-Oct-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnconn1 34686 | 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 34687 | 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 34688 | 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 34689 | 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 34690* | Generalization of axsegcon 27876. This time, we generate an endpoint for a segment on the ray 𝑄𝐴 congruent to 𝐵𝐶 and starting at 𝑄, as opposed to axsegcon 27876, 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 34691 | Declare the constant for the segment less than or equal to relationship. |
class Seg≤ | ||
Definition | df-segle 34692* | 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 34693* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) | ||
Theorem | brsegle2 34694* | 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 34695 | 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 34696 | 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 34697 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐵〉) | ||
Theorem | seglemin 34698 | 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 34699 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) | ||
Theorem | segleantisym 34700 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |