Metamath Proof Explorer

Theorem lineelsb2

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)

Ref Expression
Assertion lineelsb2 
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( S e. ( P Line Q ) -> ( P Line Q ) = ( P Line S ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 >. ) ) )
6 1 2 3 4 5 syl13anc 
 |-  ( ( ( 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 >. ) ) )
7 6 biimpa 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 >. ) ) )
10 1 8 3 4 9 syl13anc 
 |-  ( ( ( 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 >. ) ) )
11 10 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
13 1 3 2 8 4 12 syl122anc 
 |-  ( ( ( 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 >. ) ) )
14 13 imp 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ x e. ( EE ` N ) /\ S e. ( EE ` N ) ) ) -> ( S Btwn <. P , x >. -> x Colinear <. P , S >. ) )
16 1 3 8 2 15 syl13anc 
 |-  ( ( ( 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 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ S e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( x Btwn <. P , S >. -> x Colinear <. P , S >. ) )
18 1 3 2 8 17 syl13anc 
 |-  ( ( ( 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 >. ) )
19 16 18 jaod 
 |-  ( ( ( 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 >. ) )
20 19 adantr 
 |-  ( ( ( ( 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 >. ) )
21 14 20 mpd 
 |-  ( ( ( ( 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 >. )
22 21 expr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
24 1 2 3 4 23 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
26 1 4 2 3 8 24 25 btwnexch3and 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( S e. ( EE ` N ) /\ x e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P Btwn <. S , x >. -> x Colinear <. P , S >. ) )
28 1 2 8 3 27 syl13anc 
 |-  ( ( ( 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 >. ) )
29 28 adantr 
 |-  ( ( ( ( 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 >. ) )
30 26 29 mpd 
 |-  ( ( ( ( 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 >. )
31 30 expr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
34 1 4 8 3 33 btwncomand 
 |-  ( ( ( ( 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 >. )
35 1 3 2 4 8 32 34 btwnexchand 
 |-  ( ( ( ( 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 >. )
36 16 adantr 
 |-  ( ( ( ( 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 >. ) )
37 35 36 mpd 
 |-  ( ( ( ( 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 >. )
38 37 expr 
 |-  ( ( ( ( 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 >. ) )
39 22 31 38 3jaod 
 |-  ( ( ( ( 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 >. ) )
40 11 39 sylbid 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
42 1 8 3 2 41 syl13anc 
 |-  ( ( ( 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 >. ) ) )
43 42 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
46 1 3 8 2 4 44 45 btwnexchand 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( x Btwn <. P , Q >. -> x Colinear <. P , Q >. ) )
48 1 3 4 8 47 syl13anc 
 |-  ( ( ( 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 >. ) )
49 48 adantr 
 |-  ( ( ( ( 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 >. ) )
50 46 49 mpd 
 |-  ( ( ( ( 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 >. )
51 50 expr 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 )
53 52 necomd 
 |-  ( ( ( 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 )
54 53 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
56 1 2 3 4 55 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) )
59 1 4 2 3 8 58 syl122anc 
 |-  ( ( ( 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 >. ) )
60 59 adantr 
 |-  ( ( ( ( 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 >. ) )
61 54 56 57 60 mp3and 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ x e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P Btwn <. Q , x >. -> x Colinear <. P , Q >. ) )
63 1 4 8 3 62 syl13anc 
 |-  ( ( ( 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 >. ) )
64 63 adantr 
 |-  ( ( ( ( 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 >. ) )
65 61 64 mpd 
 |-  ( ( ( ( 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 >. )
66 65 expr 
 |-  ( ( ( ( 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 >. ) )
67 52 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
70 1 2 8 3 69 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
72 1 3 2 4 8 71 syl122anc 
 |-  ( ( ( 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 >. ) ) )
73 72 adantr 
 |-  ( ( ( ( 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 >. ) ) )
74 67 68 70 73 mp3and 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ x e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( Q Btwn <. P , x >. -> x Colinear <. P , Q >. ) )
76 1 3 8 4 75 syl13anc 
 |-  ( ( ( 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 >. ) )
77 76 48 jaod 
 |-  ( ( ( 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 >. ) )
78 77 adantr 
 |-  ( ( ( ( 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 >. ) )
79 74 78 mpd 
 |-  ( ( ( ( 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 >. )
80 79 expr 
 |-  ( ( ( ( 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 >. ) )
81 51 66 80 3jaod 
 |-  ( ( ( ( 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 >. ) )
82 43 81 sylbid 
 |-  ( ( ( ( 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 >. ) )
83 40 82 impbid 
 |-  ( ( ( ( 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 >. ) )
84 10 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
86 1 8 3 4 85 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
88 1 4 8 3 2 86 87 btwnexch3and 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ S e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P Btwn <. x , S >. -> x Colinear <. P , S >. ) )
90 1 8 2 3 89 syl13anc 
 |-  ( ( ( 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 >. ) )
91 90 adantr 
 |-  ( ( ( ( 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 >. ) )
92 88 91 mpd 
 |-  ( ( ( ( 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 >. )
93 92 expr 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 )
95 94 necomd 
 |-  ( ( ( 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 )
96 95 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
100 1 4 3 2 8 99 syl122anc 
 |-  ( ( ( 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 >. ) ) )
101 100 adantr 
 |-  ( ( ( ( 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 >. ) ) )
102 96 97 98 101 mp3and 
 |-  ( ( ( ( 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 >. ) )
103 19 adantr 
 |-  ( ( ( ( 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 >. ) )
104 102 103 mpd 
 |-  ( ( ( ( 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 >. )
105 104 expr 
 |-  ( ( ( ( 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 >. ) )
106 94 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
108 1 3 4 2 107 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
110 1 4 8 3 109 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) )
112 1 2 3 4 8 111 syl122anc 
 |-  ( ( ( 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 >. ) )
113 112 adantr 
 |-  ( ( ( ( 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 >. ) )
114 106 108 110 113 mp3and 
 |-  ( ( ( ( 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 >. )
115 28 adantr 
 |-  ( ( ( ( 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 >. ) )
116 114 115 mpd 
 |-  ( ( ( ( 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 >. )
117 116 expr 
 |-  ( ( ( ( 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 >. ) )
118 93 105 117 3jaod 
 |-  ( ( ( ( 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 >. ) )
119 84 118 sylbid 
 |-  ( ( ( ( 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 >. ) )
120 42 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
122 1 8 3 2 121 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
124 1 3 4 2 123 btwncomand 
 |-  ( ( ( ( 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 >. )
125 1 2 8 3 4 122 124 btwnexch3and 
 |-  ( ( ( ( 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 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P Btwn <. x , Q >. -> x Colinear <. P , Q >. ) )
127 1 8 4 3 126 syl13anc 
 |-  ( ( ( 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 >. ) )
128 127 adantr 
 |-  ( ( ( ( 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 >. ) )
129 125 128 mpd 
 |-  ( ( ( ( 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 >. )
130 129 expr 
 |-  ( ( ( ( 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 >. ) )
131 53 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
133 1 3 4 2 132 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
136 1 2 3 4 8 135 syl122anc 
 |-  ( ( ( 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 >. ) ) )
137 136 adantr 
 |-  ( ( ( ( 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 >. ) ) )
138 131 133 134 137 mp3and 
 |-  ( ( ( ( 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 >. ) )
139 77 adantr 
 |-  ( ( ( ( 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 >. ) )
140 138 139 mpd 
 |-  ( ( ( ( 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 >. )
141 140 expr 
 |-  ( ( ( ( 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 >. ) )
142 52 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
145 1 2 8 3 144 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) )
147 1 4 3 2 8 146 syl122anc 
 |-  ( ( ( 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 >. ) )
148 147 adantr 
 |-  ( ( ( ( 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 >. ) )
149 142 143 145 148 mp3and 
 |-  ( ( ( ( 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 >. )
150 63 adantr 
 |-  ( ( ( ( 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 >. ) )
151 149 150 mpd 
 |-  ( ( ( ( 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 >. )
152 151 expr 
 |-  ( ( ( ( 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 >. ) )
153 130 141 152 3jaod 
 |-  ( ( ( ( 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 >. ) )
154 120 153 sylbid 
 |-  ( ( ( ( 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 >. ) )
155 119 154 impbid 
 |-  ( ( ( ( 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 >. ) )
156 10 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
159 1 4 2 3 158 btwncomand 
 |-  ( ( ( ( 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 >. )
160 1 3 8 4 2 157 159 btwnexchand 
 |-  ( ( ( ( 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 >. )
161 18 adantr 
 |-  ( ( ( ( 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 >. ) )
162 160 161 mpd 
 |-  ( ( ( ( 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 >. )
163 162 expr 
 |-  ( ( ( ( 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 >. ) )
164 95 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) )
168 1 2 4 3 8 167 syl122anc 
 |-  ( ( ( 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 >. ) )
169 168 adantr 
 |-  ( ( ( ( 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 >. ) )
170 164 165 166 169 mp3and 
 |-  ( ( ( ( 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 >. )
171 28 adantr 
 |-  ( ( ( ( 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 >. ) )
172 170 171 mpd 
 |-  ( ( ( ( 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 >. )
173 172 expr 
 |-  ( ( ( ( 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 >. ) )
174 94 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
176 1 4 2 3 175 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
178 1 4 8 3 177 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
180 1 3 4 2 8 179 syl122anc 
 |-  ( ( ( 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 >. ) ) )
181 180 adantr 
 |-  ( ( ( ( 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 >. ) ) )
182 174 176 178 181 mp3and 
 |-  ( ( ( ( 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 >. ) )
183 19 adantr 
 |-  ( ( ( ( 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 >. ) )
184 182 183 mpd 
 |-  ( ( ( ( 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 >. )
185 184 expr 
 |-  ( ( ( ( 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 >. ) )
186 163 173 185 3jaod 
 |-  ( ( ( ( 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 >. ) )
187 156 186 sylbid 
 |-  ( ( ( ( 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 >. ) )
188 42 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 >. )
190 1 4 2 3 189 btwncomand 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( 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 >. ) ) )
193 1 3 4 8 2 192 syl122anc 
 |-  ( ( ( 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 >. ) ) )
194 193 adantr 
 |-  ( ( ( ( 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 >. ) ) )
195 190 191 194 mp2and 
 |-  ( ( ( ( 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 >. ) )
196 77 adantr 
 |-  ( ( ( ( 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 >. ) )
197 195 196 mpd 
 |-  ( ( ( ( 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 Colinear <. P , Q >. )
198 197 expr 
 |-  ( ( ( ( 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 Colinear <. P , Q >. ) )
199 simprl 
 |-  ( ( ( ( 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 <. S , x >. ) ) -> Q Btwn <. S , P >. )
200 simprr 
 |-  ( ( ( ( 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 <. S , x >. ) ) -> P Btwn <. S , x >. )
201 1 2 4 3 8 199 200 btwnexch3and 
 |-  ( ( ( ( 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 <. S , x >. ) ) -> P Btwn <. Q , x >. )
202 63 adantr 
 |-  ( ( ( ( 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 <. S , x >. ) ) -> ( P Btwn <. Q , x >. -> x Colinear <. P , Q >. ) )
203 201 202 mpd 
 |-  ( ( ( ( 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 <. S , x >. ) ) -> x Colinear <. P , Q >. )
204 203 expr 
 |-  ( ( ( ( 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 <. S , x >. -> x Colinear <. P , Q >. ) )
205 simprl 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> Q Btwn <. S , P >. )
206 1 4 2 3 205 btwncomand 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> Q Btwn <. P , S >. )
207 simprr 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> S Btwn <. x , P >. )
208 1 2 8 3 207 btwncomand 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> S Btwn <. P , x >. )
209 1 3 4 2 8 206 208 btwnexchand 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> Q Btwn <. P , x >. )
210 76 adantr 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> ( Q Btwn <. P , x >. -> x Colinear <. P , Q >. ) )
211 209 210 mpd 
 |-  ( ( ( ( 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 >. /\ S Btwn <. x , P >. ) ) -> x Colinear <. P , Q >. )
212 211 expr 
 |-  ( ( ( ( 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 >. ) -> ( S Btwn <. x , P >. -> x Colinear <. P , Q >. ) )
213 198 204 212 3jaod 
 |-  ( ( ( ( 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 >. \/ P Btwn <. S , x >. \/ S Btwn <. x , P >. ) -> x Colinear <. P , Q >. ) )
214 188 213 sylbid 
 |-  ( ( ( ( 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 Colinear <. P , Q >. ) )
215 187 214 impbid 
 |-  ( ( ( ( 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 >. ) )
216 83 155 215 3jaodan 
 |-  ( ( ( ( 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 , S >. \/ Q Btwn <. S , P >. ) ) -> ( x Colinear <. P , Q >. <-> x Colinear <. P , S >. ) )
217 7 216 syldan 
 |-  ( ( ( ( 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 >. ) -> ( x Colinear <. P , Q >. <-> x Colinear <. P , S >. ) )
218 217 adantrl 
 |-  ( ( ( ( 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 ) /\ S Colinear <. P , Q >. ) ) -> ( x Colinear <. P , Q >. <-> x Colinear <. P , S >. ) )
219 218 an32s 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) /\ ( S e. ( EE ` N ) /\ S Colinear <. P , Q >. ) ) /\ x e. ( EE ` N ) ) -> ( x Colinear <. P , Q >. <-> x Colinear <. P , S >. ) )
220 219 rabbidva 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) /\ ( S e. ( EE ` N ) /\ S Colinear <. P , Q >. ) ) -> { x e. ( EE ` N ) | x Colinear <. P , Q >. } = { x e. ( EE ` N ) | x Colinear <. P , S >. } )
221 220 ex 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( ( S e. ( EE ` N ) /\ S Colinear <. P , Q >. ) -> { x e. ( EE ` N ) | x Colinear <. P , Q >. } = { x e. ( EE ` N ) | x Colinear <. P , S >. } ) )
222 fvline2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
223 222 3adant3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
224 223 eleq2d 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( S e. ( P Line Q ) <-> S e. { x e. ( EE ` N ) | x Colinear <. P , Q >. } ) )
225 breq1 
 |-  ( x = S -> ( x Colinear <. P , Q >. <-> S Colinear <. P , Q >. ) )
226 225 elrab 
 |-  ( S e. { x e. ( EE ` N ) | x Colinear <. P , Q >. } <-> ( S e. ( EE ` N ) /\ S Colinear <. P , Q >. ) )
227 224 226 bitrdi 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( S e. ( P Line Q ) <-> ( S e. ( EE ` N ) /\ S Colinear <. P , Q >. ) ) )
228 simp1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> N e. NN )
229 simp21 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> P e. ( EE ` N ) )
230 simp3l 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> S e. ( EE ` N ) )
231 simp3r 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> P =/= S )
232 fvline2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ S e. ( EE ` N ) /\ P =/= S ) ) -> ( P Line S ) = { x e. ( EE ` N ) | x Colinear <. P , S >. } )
233 228 229 230 231 232 syl13anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( P Line S ) = { x e. ( EE ` N ) | x Colinear <. P , S >. } )
234 223 233 eqeq12d 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( ( P Line Q ) = ( P Line S ) <-> { x e. ( EE ` N ) | x Colinear <. P , Q >. } = { x e. ( EE ` N ) | x Colinear <. P , S >. } ) )
235 221 227 234 3imtr4d 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) -> ( S e. ( P Line Q ) -> ( P Line Q ) = ( P Line S ) ) )