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

Theorem lineelsb2 24771
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 simpl1 958 . . . . . . . . 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 1010 . . . . . . . . 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 1033 . . . . . . . . 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 1034 . . . . . . . . 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 24682 . . . . . . . . 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 1184 . . . . . . . 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 470 . . . . . . 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 447 . . . . . . . . . . . 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 24682 . . . . . . . . . . . 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 1184 . . . . . . . . . . 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 451 . . . . . . . . . 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 24726 . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . 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 418 . . . . . . . . . . . . 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 24694 . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . 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 24696 . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . 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 369 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 24644 . . . . . . . . . . . . 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 24695 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24649 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1246 . . . . . . . . . 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 206 . . . . . . . . 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 24682 . . . . . . . . . . . 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 1184 . . . . . . . . . . 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 451 . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 24649 . . . . . . . . . . . . 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 24696 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1011 . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 24645 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 24695 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24724 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 24694 . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . 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 369 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1246 . . . . . . . . . 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 206 . . . . . . . . 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 183 . . . . . . . 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 451 . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 24644 . . . . . . . . . . . . 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 24693 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1035 . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 24725 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24647 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1246 . . . . . . . . . 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 206 . . . . . . . . 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 451 . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24644 . . . . . . . . . . . . 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 24693 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 24725 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24647 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1246 . . . . . . . . . 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 206 . . . . . . . . 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 183 . . . . . . . 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 451 . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24649 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 24645 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 24724 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 1280 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 598 . . . . . . . . . . 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 1246 . . . . . . . . . 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 206 . . . . . . . . 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 451 . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24638 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 24726 . . . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . 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 451 . . . . . . . . . . . . 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 >. )  ->  x  Colinear  <. P ,  Q >. ) )
197195, 196mpd 14 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e. <