Theorem colineartriv2

Description: Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	colineartriv2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 Colinear ⟨ 𝐵 , 𝐵 ⟩ )

Proof

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