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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 Colinear ⟨ 𝐴 , 𝐵 ⟩ )

Proof

Step Hyp Ref Expression
1 btwntriv1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 Btwn ⟨ 𝐴 , 𝐵 ⟩ )
2 1 3mix1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐴 ⟩ ∨ 𝐵 Btwn ⟨ 𝐴 , 𝐴 ⟩ ) )
3 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
4 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
6 brcolinear ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐴 ⟩ ∨ 𝐵 Btwn ⟨ 𝐴 , 𝐴 ⟩ ) ) )
7 3 4 4 5 6 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Colinear ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐴 ⟩ ∨ 𝐵 Btwn ⟨ 𝐴 , 𝐴 ⟩ ) ) )
8 2 7 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 Colinear ⟨ 𝐴 , 𝐵 ⟩ )