# 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 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Colinear}⟨{B},{C}⟩\to \left({B}\mathrm{Btwn}⟨{A},{C}⟩↔\left(⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{A},{C}⟩\wedge ⟨{B},{C}⟩{\mathrm{Seg}}_{\le }⟨{A},{C}⟩\right)\right)\right)$

### Proof

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