P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

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