Theorem brcolinear

Description: The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013)

	Ref	Expression
Assertion	brcolinear	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		brcolinear2	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
2	1	3adant1	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
3	2	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
4		simpr	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
5	4	rexlimivw	⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
6		fveq2	⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
7	6	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
8	6	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
9	6	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
10	7 8 9	3anbi123d	⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
11	10	anbi1d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
12	11	rspcev	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
13	12	expr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
14	5 13	impbid2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
15	3 14	bitrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )