Theorem btwncolinear1

Description: Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013)

	Ref	Expression
Assertion	btwncolinear1	$$⊢\left(N\in \mathbb{N}\wedge \left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\wedge C\in 𝔼\left(N\right)\right)\right)\to \left(C\mathrm{Btwn}⟨A,B⟩\to A\mathrm{Colinear}⟨B,C⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		3mix3	$$⊢C\mathrm{Btwn}⟨A,B⟩\to \left(A\mathrm{Btwn}⟨B,C⟩\vee B\mathrm{Btwn}⟨C,A⟩\vee C\mathrm{Btwn}⟨A,B⟩\right)$$
2		brcolinear	$$⊢\left(N\in \mathbb{N}\wedge \left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\wedge C\in 𝔼\left(N\right)\right)\right)\to \left(A\mathrm{Colinear}⟨B,C⟩\leftrightarrow \left(A\mathrm{Btwn}⟨B,C⟩\vee B\mathrm{Btwn}⟨C,A⟩\vee C\mathrm{Btwn}⟨A,B⟩\right)\right)$$
3	1 2	imbitrrid	$$⊢\left(N\in \mathbb{N}\wedge \left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\wedge C\in 𝔼\left(N\right)\right)\right)\to \left(C\mathrm{Btwn}⟨A,B⟩\to A\mathrm{Colinear}⟨B,C⟩\right)$$