Metamath Proof Explorer

Theorem 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 ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear A B

Proof

Step Hyp Ref Expression
1 btwntriv1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn A B
2 1 3mix1d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn A B ∨ A Btwn B A ∨ B Btwn A A
3 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → N ∈ ℕ
4 simp2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
5 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
6 brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear A B ↔ A Btwn A B ∨ A Btwn B A ∨ B Btwn A A
7 3 4 4 5 6 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear A B ↔ A Btwn A B ∨ A Btwn B A ∨ B Btwn A A
8 2 7 mpbird ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear A B