Metamath Proof Explorer

Theorem colinbtwnle

Description: Given three colinear points A , B , and C , B falls in the middle iff the two segments to B are no longer than A C . Theorem 5.12 of Schwabhauser p. 42. (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion colinbtwnle ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 btwnsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) )
2 3anrev ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
3 btwnsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ → ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ) )
4 2 3 sylan2b ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ → ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ) )
5 3ancoma ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
6 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
7 5 6 sylan2b ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
8 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
9 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
11 8 9 10 cgrrflx2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ )
12 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
13 8 12 10 cgrrflx2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ )
14 seglecgr12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ ) → ( ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ↔ ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ) ) )
15 8 9 10 12 10 10 9 10 12 14 syl333anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ ) → ( ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ↔ ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ) ) )
16 11 13 15 mp2and ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ↔ ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ) )
17 4 7 16 3imtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ → ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) )
18 1 17 jcad ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) )
19 18 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) )
20 brcolinear ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
21 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ )
22 8 12 9 10 21 btwncomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐴 Btwn ⟨ 𝐶 , 𝐵 ⟩ )
23 16 biimpa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ )
24 23 adantrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ )
25 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 Btwn ⟨ 𝐶 , 𝐵 ⟩ ) )
26 3anrot ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
27 btwnsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝐶 , 𝐵 ⟩ → ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ ) )
28 26 27 sylan2br ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝐶 , 𝐵 ⟩ → ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ ) )
29 25 28 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ → ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ ) )
30 29 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) → ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ )
31 30 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ )
32 segleantisym ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ ) → ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ ) )
33 8 10 9 10 12 32 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ ) → ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ ) )
34 33 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( ( ⟨ 𝐶 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐴 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Seg≤ ⟨ 𝐶 , 𝐵 ⟩ ) → ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ ) )
35 24 31 34 mp2and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐴 ⟩ )
36 8 10 9 12 22 35 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐵 = 𝐴 )
37 btwntriv1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
38 37 3adant3r2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
39 breq1 ⊢ ( 𝐵 = 𝐴 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐴 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
40 38 39 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 = 𝐴 → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
41 40 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝐵 = 𝐴 → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
42 36 41 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
43 42 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) → ( ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
44 43 adantld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
45 44 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
46 7 biimprd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
47 46 a1dd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
48 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ )
49 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ )
50 3ancomb ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
51 btwnsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) )
52 50 51 sylan2b ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) )
53 52 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ )
54 53 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ )
55 segleantisym ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) )
56 8 12 9 12 10 55 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) )
57 56 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) )
58 49 54 57 mp2and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
59 8 12 9 10 48 58 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐵 = 𝐶 )
60 btwntriv2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
61 60 3adant3r2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
62 breq1 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐶 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
63 61 62 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 = 𝐶 → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
64 63 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝐵 = 𝐶 → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
65 59 64 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
66 65 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
67 66 adantrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
68 67 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
69 45 47 68 3jaod ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
70 20 69 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
71 70 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
72 19 71 impbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) )
73 72 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) ) ) )