colineartriv1

Description: Trivial case of colinearity. Theorem 4.12 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

		Ref	Expression
	Assertion	colineartriv1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to A Colinear ⟨A, B⟩$

Step	Hyp	Ref	Expression
1		btwntriv1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to A Btwn ⟨A, B⟩$
2	1	3mix1d	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (A Btwn ⟨A, B⟩ \lor A Btwn ⟨B, A⟩ \lor B Btwn ⟨A, A⟩)$
3		simp1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to N \in ℕ$
4		simp2	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to A \in 𝔼 (N)$
5		simp3	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to B \in 𝔼 (N)$
6		brcolinear	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (A Colinear ⟨A, B⟩ \leftrightarrow (A Btwn ⟨A, B⟩ \lor A Btwn ⟨B, A⟩ \lor B Btwn ⟨A, A⟩))$
7	3 4 4 5 6	syl13anc	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (A Colinear ⟨A, B⟩ \leftrightarrow (A Btwn ⟨A, B⟩ \lor A Btwn ⟨B, A⟩ \lor B Btwn ⟨A, A⟩))$
8	2 7	mpbird	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to A Colinear ⟨A, B⟩$

Metamath Proof Explorer