Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lineelsb2 Unicode version

Theorem lineelsb2 24178
Description: If  S lies on  P Q, then  P Q  =  P S. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
lineelsb2  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  -> 
( S  e.  ( PLine Q )  -> 
( PLine Q )  =  ( PLine S
) ) )

Proof of Theorem lineelsb2
StepHypRef Expression
1 simpl1 963 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  N  e.  NN )
2 simpl3l 1015 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  S  e.  ( EE `  N
) )
3 simpl21 1038 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  P  e.  ( EE `  N
) )
4 simpl22 1039 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  Q  e.  ( EE `  N
) )
5 brcolinear 24089 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( S  e.  ( EE `  N )  /\  P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
) ) )  -> 
( S  Colinear  <. P ,  Q >. 
<->  ( S  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  S >.  \/  Q  Btwn  <. S ,  P >. ) ) )
61, 2, 3, 4, 5syl13anc 1189 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( S  Colinear  <. P ,  Q >.  <-> 
( S  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  S >.  \/  Q  Btwn  <. S ,  P >. ) ) )
76biimpa 472 . . . . . . 7  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Colinear  <. P ,  Q >. )  ->  ( S  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  S >.  \/  Q  Btwn  <. S ,  P >. ) )
8 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  x  e.  ( EE `  N
) )
9 brcolinear 24089 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
) ) )  -> 
( x  Colinear  <. P ,  Q >. 
<->  ( x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. ) ) )
101, 8, 3, 4, 9syl13anc 1189 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
x  Colinear  <. P ,  Q >.  <-> 
( x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. ) ) )
1110adantr 453 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Colinear  <. P ,  Q >.  <->  (
x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. ) ) )
12 btwnconn3 24133 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  S  e.  ( EE `  N ) )  /\  ( x  e.  ( EE `  N )  /\  Q  e.  ( EE `  N ) ) )  ->  ( ( S 
Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  Q >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
131, 3, 2, 8, 4, 12syl122anc 1196 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  Q >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
1413imp 420 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) )
15 btwncolinear3 24101 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  x  e.  ( EE `  N )  /\  S  e.  ( EE `  N
) ) )  -> 
( S  Btwn  <. P ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
161, 3, 8, 2, 15syl13anc 1189 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( S  Btwn  <. P ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
17 btwncolinear5 24103 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  S  e.  ( EE `  N )  /\  x  e.  ( EE `  N
) ) )  -> 
( x  Btwn  <. P ,  S >.  ->  x  Colinear  <. P ,  S >. ) )
181, 3, 2, 8, 17syl13anc 1189 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
x  Btwn  <. P ,  S >.  ->  x  Colinear  <. P ,  S >. ) )
1916, 18jaod 371 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. )  ->  x  Colinear  <. P ,  S >. ) )
2019adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  ( ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. )  ->  x  Colinear  <. P ,  S >. ) )
2114, 20mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Colinear  <. P ,  S >. )
2221expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Btwn  <. P ,  Q >.  ->  x  Colinear  <. P ,  S >. ) )
23 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  S  Btwn  <. P ,  Q >. )
241, 2, 3, 4, 23btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  S  Btwn  <. Q ,  P >. )
25 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  P  Btwn  <. Q ,  x >. )
261, 4, 2, 3, 8, 24, 25btwnexch3and 24051 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  P  Btwn  <. S ,  x >. )
27 btwncolinear4 24102 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  ( S  e.  ( EE `  N )  /\  x  e.  ( EE `  N )  /\  P  e.  ( EE `  N
) ) )  -> 
( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
281, 2, 8, 3, 27syl13anc 1189 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
2928adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  ( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
3026, 29mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  x  Colinear  <. P ,  S >. )
3130expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
32 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <. P ,  Q >. )
33 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <.
x ,  P >. )
341, 4, 8, 3, 33btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <. P ,  x >. )
351, 3, 2, 4, 8, 32, 34btwnexchand 24056 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <. P ,  x >. )
3616adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  ( S  Btwn  <. P ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
3735, 36mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  x  Colinear  <. P ,  S >. )
3837expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( Q  Btwn  <. x ,  P >.  ->  x  Colinear  <. P ,  S >. ) )
3922, 31, 383jaod 1251 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( (
x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. )  ->  x  Colinear  <. P ,  S >. ) )
4011, 39sylbid 208 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Colinear  <. P ,  Q >.  ->  x  Colinear  <. P ,  S >. ) )
41 brcolinear 24089 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  P  e.  ( EE `  N )  /\  S  e.  ( EE `  N
) ) )  -> 
( x  Colinear  <. P ,  S >. 
<->  ( x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. ) ) )
421, 8, 3, 2, 41syl13anc 1189 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
x  Colinear  <. P ,  S >.  <-> 
( x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. ) ) )
4342adantr 453 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Colinear  <. P ,  S >.  <->  (
x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. ) ) )
44 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Btwn  <. P ,  S >. )
45 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  S >. ) )  ->  S  Btwn  <. P ,  Q >. )
461, 3, 8, 2, 4, 44, 45btwnexchand 24056 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Btwn  <. P ,  Q >. )
47 btwncolinear5 24103 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  x  e.  ( EE `  N
) ) )  -> 
( x  Btwn  <. P ,  Q >.  ->  x  Colinear  <. P ,  Q >. ) )
481, 3, 4, 8, 47syl13anc 1189 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
x  Btwn  <. P ,  Q >.  ->  x  Colinear  <. P ,  Q >. ) )
4948adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  S >. ) )  ->  ( x  Btwn  <. P ,  Q >.  ->  x  Colinear  <. P ,  Q >. ) )
5046, 49mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Colinear  <. P ,  Q >. )
5150expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Btwn  <. P ,  S >.  ->  x  Colinear  <. P ,  Q >. ) )
52 simpl3r 1016 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  P  =/=  S )
5352necomd 2530 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  S  =/=  P )
5453adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  S  =/=  P )
55 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  S  Btwn  <. P ,  Q >. )
561, 2, 3, 4, 55btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  S  Btwn  <. Q ,  P >. )
57 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  P  Btwn  <. S ,  x >. )
58 btwnouttr2 24052 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( Q  e.  ( EE `  N )  /\  S  e.  ( EE `  N ) )  /\  ( P  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( S  =/=  P  /\  S  Btwn  <. Q ,  P >.  /\  P  Btwn  <. S ,  x >. )  ->  P  Btwn  <. Q ,  x >. ) )
591, 4, 2, 3, 8, 58syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( S  =/=  P  /\  S  Btwn  <. Q ,  P >.  /\  P  Btwn  <. S ,  x >. )  ->  P  Btwn  <. Q ,  x >. ) )
6059adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  ( ( S  =/=  P  /\  S  Btwn  <. Q ,  P >.  /\  P  Btwn  <. S ,  x >. )  ->  P  Btwn  <. Q ,  x >. ) )
6154, 56, 57, 60mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  P  Btwn  <. Q ,  x >. )
62 btwncolinear4 24102 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  ( Q  e.  ( EE `  N )  /\  x  e.  ( EE `  N )  /\  P  e.  ( EE `  N
) ) )  -> 
( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
631, 4, 8, 3, 62syl13anc 1189 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
6463adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  ( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
6561, 64mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  P  Btwn  <. S ,  x >. ) )  ->  x  Colinear  <. P ,  Q >. )
6665expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
6752adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  P  =/=  S )
68 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <. P ,  Q >. )
69 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <.
x ,  P >. )
701, 2, 8, 3, 69btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <. P ,  x >. )
71 btwnconn1 24131 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  S  e.  ( EE `  N ) )  /\  ( Q  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( P  =/=  S  /\  S  Btwn  <. P ,  Q >.  /\  S  Btwn  <. P ,  x >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
721, 3, 2, 4, 8, 71syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( P  =/=  S  /\  S  Btwn  <. P ,  Q >.  /\  S  Btwn  <. P ,  x >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
7372adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  ( ( P  =/=  S  /\  S  Btwn  <. P ,  Q >.  /\  S  Btwn  <. P ,  x >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
7467, 68, 70, 73mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) )
75 btwncolinear3 24101 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  x  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
) ) )  -> 
( Q  Btwn  <. P ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
761, 3, 8, 4, 75syl13anc 1189 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( Q  Btwn  <. P ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
7776, 48jaod 371 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. )  ->  x  Colinear  <. P ,  Q >. ) )
7877adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  ( ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. )  ->  x  Colinear  <. P ,  Q >. ) )
7974, 78mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( S  Btwn  <. P ,  Q >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  x  Colinear  <. P ,  Q >. )
8079expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( S  Btwn  <. x ,  P >.  ->  x  Colinear  <. P ,  Q >. ) )
8151, 66, 803jaod 1251 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( (
x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. )  ->  x  Colinear  <. P ,  Q >. ) )
8243, 81sylbid 208 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Colinear  <. P ,  S >.  ->  x  Colinear  <. P ,  Q >. ) )
8340, 82impbid 185 . . . . . . . 8  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  S  Btwn  <. P ,  Q >. )  ->  ( x  Colinear  <. P ,  Q >.  <->  x  Colinear  <. P ,  S >. ) )
8410adantr 453 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Colinear  <. P ,  Q >.  <->  (
x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. ) ) )
85 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Btwn  <. P ,  Q >. )
861, 8, 3, 4, 85btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Btwn  <. Q ,  P >. )
87 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  P  Btwn  <. Q ,  S >. )
881, 4, 8, 3, 2, 86, 87btwnexch3and 24051 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  P  Btwn  <.
x ,  S >. )
89 btwncolinear2 24100 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  S  e.  ( EE `  N )  /\  P  e.  ( EE `  N
) ) )  -> 
( P  Btwn  <. x ,  S >.  ->  x  Colinear  <. P ,  S >. )
)
901, 8, 2, 3, 89syl13anc 1189 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( P  Btwn  <. x ,  S >.  ->  x  Colinear  <. P ,  S >. ) )
9190adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  ( P  Btwn  <. x ,  S >.  ->  x  Colinear  <. P ,  S >. ) )
9288, 91mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Colinear  <. P ,  S >. )
9392expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Btwn  <. P ,  Q >.  ->  x  Colinear  <. P ,  S >. ) )
94 simpl23 1040 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  P  =/=  Q )
9594necomd 2530 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  Q  =/=  P )
9695adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  Q  =/=  P )
97 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  P  Btwn  <. Q ,  S >. )
98 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  P  Btwn  <. Q ,  x >. )
99 btwnconn2 24132 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( Q  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( S  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( Q  =/=  P  /\  P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
1001, 4, 3, 2, 8, 99syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( Q  =/=  P  /\  P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
101100adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  ( ( Q  =/=  P  /\  P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
10296, 97, 98, 101mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) )
10319adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  ( ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. )  ->  x  Colinear  <. P ,  S >. ) )
104102, 103mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  x  Colinear  <. P ,  S >. )
105104expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
10694adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  P  =/=  Q )
107 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  P  Btwn  <. Q ,  S >. )
1081, 3, 4, 2, 107btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  P  Btwn  <. S ,  Q >. )
109 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <.
x ,  P >. )
1101, 4, 8, 3, 109btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <. P ,  x >. )
111 btwnouttr 24054 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( S  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( Q  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( P  =/=  Q  /\  P  Btwn  <. S ,  Q >.  /\  Q  Btwn  <. P ,  x >. )  ->  P  Btwn  <. S ,  x >. ) )
1121, 2, 3, 4, 8, 111syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( P  =/=  Q  /\  P  Btwn  <. S ,  Q >.  /\  Q  Btwn  <. P ,  x >. )  ->  P  Btwn  <. S ,  x >. ) )
113112adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  ( ( P  =/=  Q  /\  P  Btwn  <. S ,  Q >.  /\  Q  Btwn  <. P ,  x >. )  ->  P  Btwn  <. S ,  x >. ) )
114106, 108, 110, 113mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  P  Btwn  <. S ,  x >. )
11528adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  ( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
116114, 115mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  x  Colinear  <. P ,  S >. )
117116expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( Q  Btwn  <. x ,  P >.  ->  x  Colinear  <. P ,  S >. ) )
11893, 105, 1173jaod 1251 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( (
x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. )  ->  x  Colinear  <. P ,  S >. ) )
11984, 118sylbid 208 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Colinear  <. P ,  Q >.  ->  x  Colinear  <. P ,  S >. ) )
12042adantr 453 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Colinear  <. P ,  S >.  <->  (
x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. ) ) )
121 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Btwn  <. P ,  S >. )
1221, 8, 3, 2, 121btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Btwn  <. S ,  P >. )
123 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  P  Btwn  <. Q ,  S >. )
1241, 3, 4, 2, 123btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  P  Btwn  <. S ,  Q >. )
1251, 2, 8, 3, 4, 122, 124btwnexch3and 24051 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  P  Btwn  <.
x ,  Q >. )
126 btwncolinear2 24100 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  e.  ( EE `  N
) ) )  -> 
( P  Btwn  <. x ,  Q >.  ->  x  Colinear  <. P ,  Q >. )
)
1271, 8, 4, 3, 126syl13anc 1189 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  ( P  Btwn  <. x ,  Q >.  ->  x  Colinear  <. P ,  Q >. ) )
128127adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  ( P  Btwn  <. x ,  Q >.  ->  x  Colinear  <. P ,  Q >. ) )
129125, 128mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Colinear  <. P ,  Q >. )
130129expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Btwn  <. P ,  S >.  ->  x  Colinear  <. P ,  Q >. ) )
13153adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  S  =/=  P )
132 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  P  Btwn  <. Q ,  S >. )
1331, 3, 4, 2, 132btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  P  Btwn  <. S ,  Q >. )
134 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  P  Btwn  <. S ,  x >. )
135 btwnconn2 24132 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( S  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( Q  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( S  =/=  P  /\  P  Btwn  <. S ,  Q >.  /\  P  Btwn  <. S ,  x >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
1361, 2, 3, 4, 8, 135syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( S  =/=  P  /\  P  Btwn  <. S ,  Q >.  /\  P  Btwn  <. S ,  x >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
137136adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  ( ( S  =/=  P  /\  P  Btwn  <. S ,  Q >.  /\  P  Btwn  <. S ,  x >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
138131, 133, 134, 137mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) )
13977adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  ( ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. )  ->  x  Colinear  <. P ,  Q >. ) )
140138, 139mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  P  Btwn  <. S ,  x >. ) )  ->  x  Colinear  <. P ,  Q >. )
141140expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
14252adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  P  =/=  S )
143 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  P  Btwn  <. Q ,  S >. )
144 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <.
x ,  P >. )
1451, 2, 8, 3, 144btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  S  Btwn  <. P ,  x >. )
146 btwnouttr 24054 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( Q  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( S  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( P  =/=  S  /\  P  Btwn  <. Q ,  S >.  /\  S  Btwn  <. P ,  x >. )  ->  P  Btwn  <. Q ,  x >. ) )
1471, 4, 3, 2, 8, 146syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( P  =/=  S  /\  P  Btwn  <. Q ,  S >.  /\  S  Btwn  <. P ,  x >. )  ->  P  Btwn  <. Q ,  x >. ) )
148147adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  ( ( P  =/=  S  /\  P  Btwn  <. Q ,  S >.  /\  S  Btwn  <. P ,  x >. )  ->  P  Btwn  <. Q ,  x >. ) )
149142, 143, 145, 148mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  P  Btwn  <. Q ,  x >. )
15063adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  ( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  Q >. ) )
151149, 150mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( P  Btwn  <. Q ,  S >.  /\  S  Btwn  <.
x ,  P >. ) )  ->  x  Colinear  <. P ,  Q >. )
152151expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( S  Btwn  <. x ,  P >.  ->  x  Colinear  <. P ,  Q >. ) )
153130, 141, 1523jaod 1251 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( (
x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. )  ->  x  Colinear  <. P ,  Q >. ) )
154120, 153sylbid 208 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Colinear  <. P ,  S >.  ->  x  Colinear  <. P ,  Q >. ) )
155119, 154impbid 185 . . . . . . . 8  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  P  Btwn  <. Q ,  S >. )  ->  ( x  Colinear  <. P ,  Q >.  <->  x  Colinear  <. P ,  S >. ) )
15610adantr 453 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( x  Colinear  <. P ,  Q >.  <->  (
x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. ) ) )
157 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Btwn  <. P ,  Q >. )
158 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  Q  Btwn  <. S ,  P >. )
1591, 4, 2, 3, 158btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  Q  Btwn  <. P ,  S >. )
1601, 3, 8, 4, 2, 157, 159btwnexchand 24056 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Btwn  <. P ,  S >. )
16118adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  ( x  Btwn  <. P ,  S >.  ->  x  Colinear  <. P ,  S >. ) )
162160, 161mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  Q >. ) )  ->  x  Colinear  <. P ,  S >. )
163162expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( x  Btwn  <. P ,  Q >.  ->  x  Colinear  <. P ,  S >. ) )
16495adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  Q  =/=  P )
165 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  Q  Btwn  <. S ,  P >. )
166 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  P  Btwn  <. Q ,  x >. )
167 btwnouttr2 24052 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( S  e.  ( EE `  N )  /\  Q  e.  ( EE `  N ) )  /\  ( P  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( Q  =/=  P  /\  Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. )  ->  P  Btwn  <. S ,  x >. ) )
1681, 2, 4, 3, 8, 167syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( Q  =/=  P  /\  Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. )  ->  P  Btwn  <. S ,  x >. ) )
169168adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  ( ( Q  =/=  P  /\  Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. )  ->  P  Btwn  <. S ,  x >. ) )
170164, 165, 166, 169mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  P  Btwn  <. S ,  x >. )
17128adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  ( P  Btwn  <. S ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
172170, 171mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  P  Btwn  <. Q ,  x >. ) )  ->  x  Colinear  <. P ,  S >. )
173172expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( P  Btwn  <. Q ,  x >.  ->  x  Colinear  <. P ,  S >. ) )
17494adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  P  =/=  Q )
175 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <. S ,  P >. )
1761, 4, 2, 3, 175btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <. P ,  S >. )
177 simprr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <.
x ,  P >. )
1781, 4, 8, 3, 177btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  Q  Btwn  <. P ,  x >. )
179 btwnconn1 24131 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N ) )  /\  ( S  e.  ( EE `  N )  /\  x  e.  ( EE `  N ) ) )  ->  ( ( P  =/=  Q  /\  Q  Btwn  <. P ,  S >.  /\  Q  Btwn  <. P ,  x >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
1801, 3, 4, 2, 8, 179syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( P  =/=  Q  /\  Q  Btwn  <. P ,  S >.  /\  Q  Btwn  <. P ,  x >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
181180adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  ( ( P  =/=  Q  /\  Q  Btwn  <. P ,  S >.  /\  Q  Btwn  <. P ,  x >. )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) ) )
182174, 176, 178, 181mp3and 1285 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. ) )
18319adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  ( ( S  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  S >. )  ->  x  Colinear  <. P ,  S >. ) )
184182, 183mpd 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  Q  Btwn  <.
x ,  P >. ) )  ->  x  Colinear  <. P ,  S >. )
185184expr 601 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( Q  Btwn  <. x ,  P >.  ->  x  Colinear  <. P ,  S >. ) )
186163, 173, 1853jaod 1251 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( (
x  Btwn  <. P ,  Q >.  \/  P  Btwn  <. Q ,  x >.  \/  Q  Btwn  <. x ,  P >. )  ->  x  Colinear  <. P ,  S >. ) )
187156, 186sylbid 208 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( x  Colinear  <. P ,  Q >.  ->  x  Colinear  <. P ,  S >. ) )
18842adantr 453 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  Q  Btwn  <. S ,  P >. )  ->  ( x  Colinear  <. P ,  S >.  <->  (
x  Btwn  <. P ,  S >.  \/  P  Btwn  <. S ,  x >.  \/  S  Btwn  <. x ,  P >. ) ) )
189 simprl 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  S >. ) )  ->  Q  Btwn  <. S ,  P >. )
1901, 4, 2, 3, 189btwncomand 24045 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  S >. ) )  ->  Q  Btwn  <. P ,  S >. )
191 simprr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  S >. ) )  ->  x  Btwn  <. P ,  S >. )
192 btwnconn3 24133 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N ) )  /\  ( x  e.  ( EE `  N )  /\  S  e.  ( EE `  N ) ) )  ->  ( ( Q 
Btwn  <. P ,  S >.  /\  x  Btwn  <. P ,  S >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
1931, 3, 4, 8, 2, 192syl122anc 1196 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  =/=  Q
)  /\  ( S  e.  ( EE `  N
)  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N
) )  ->  (
( Q  Btwn  <. P ,  S >.  /\  x  Btwn  <. P ,  S >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
194193adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  S >. ) )  ->  ( ( Q  Btwn  <. P ,  S >.  /\  x  Btwn  <. P ,  S >. )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) ) )
195190, 191, 194mp2and 663 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  S >. ) )  ->  ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,  Q >. ) )
19677adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  P  =/=  Q )  /\  ( S  e.  ( EE `  N )  /\  P  =/=  S ) )  /\  x  e.  ( EE `  N ) )  /\  ( Q  Btwn  <. S ,  P >.  /\  x  Btwn  <. P ,  S >. ) )  ->  ( ( Q  Btwn  <. P ,  x >.  \/  x  Btwn  <. P ,