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 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. -> ( B Btwn <. A , C >. <-> ( <. A , B >. Seg<_ <. A , C >. /\ <. B , C >. Seg<_ <. A , C >. ) ) ) )

Proof

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