Metamath Proof Explorer

Theorem broutsideof3

Description: Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of Schwabhauser p. 43. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion broutsideof3 
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) )

Proof

Step Hyp Ref Expression
1 broutsideof2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
2 simpl 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> N e. NN )
3 simpr3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
4 simpr1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
5 btwndiff 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ P e. ( EE ` N ) ) -> E. c e. ( EE ` N ) ( P Btwn <. B , c >. /\ P =/= c ) )
6 2 3 4 5 syl3anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. c e. ( EE ` N ) ( P Btwn <. B , c >. /\ P =/= c ) )
7 6 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) ) -> E. c e. ( EE ` N ) ( P Btwn <. B , c >. /\ P =/= c ) )
8 df-3an 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) )
9 3anass 
 |-  ( ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) <-> ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ ( P Btwn <. B , c >. /\ P =/= c ) ) )
10 simpr3 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> P =/= c )
11 10 necomd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> c =/= P )
12 simp1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) -> N e. NN )
13 simp23 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) -> B e. ( EE ` N ) )
14 simp22 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) -> A e. ( EE ` N ) )
15 simp21 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) -> P e. ( EE ` N ) )
16 simp3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) -> c e. ( EE ` N ) )
17 simpr1r 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> A Btwn <. P , B >. )
18 12 14 15 13 17 btwncomand 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> A Btwn <. B , P >. )
19 simpr2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> P Btwn <. B , c >. )
20 12 13 14 15 16 18 19 btwnexch3and 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> P Btwn <. A , c >. )
21 11 20 19 3jca 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ P Btwn <. B , c >. /\ P =/= c ) ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) )
22 8 9 21 syl2anbr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) /\ ( P Btwn <. B , c >. /\ P =/= c ) ) ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) )
23 22 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) ) -> ( ( P Btwn <. B , c >. /\ P =/= c ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
24 23 an32s 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) ) /\ c e. ( EE ` N ) ) -> ( ( P Btwn <. B , c >. /\ P =/= c ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
25 24 reximdva 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) ) -> ( E. c e. ( EE ` N ) ( P Btwn <. B , c >. /\ P =/= c ) -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
26 7 25 mpd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ A Btwn <. P , B >. ) ) -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) )
27 26 expr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P ) ) -> ( A Btwn <. P , B >. -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
28 simpr2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
29 btwndiff 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ P e. ( EE ` N ) ) -> E. c e. ( EE ` N ) ( P Btwn <. A , c >. /\ P =/= c ) )
30 2 28 4 29 syl3anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. c e. ( EE ` N ) ( P Btwn <. A , c >. /\ P =/= c ) )
31 30 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) ) -> E. c e. ( EE ` N ) ( P Btwn <. A , c >. /\ P =/= c ) )
32 3anass 
 |-  ( ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) <-> ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ ( P Btwn <. A , c >. /\ P =/= c ) ) )
33 simpr3 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> P =/= c )
34 33 necomd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> c =/= P )
35 simpr2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> P Btwn <. A , c >. )
36 simpr1r 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> B Btwn <. P , A >. )
37 12 13 15 14 36 btwncomand 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> B Btwn <. A , P >. )
38 12 14 13 15 16 37 35 btwnexch3and 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> P Btwn <. B , c >. )
39 34 35 38 3jca 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ P Btwn <. A , c >. /\ P =/= c ) ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) )
40 8 32 39 syl2anbr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) /\ ( P Btwn <. A , c >. /\ P =/= c ) ) ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) )
41 40 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) ) -> ( ( P Btwn <. A , c >. /\ P =/= c ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
42 41 an32s 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) ) /\ c e. ( EE ` N ) ) -> ( ( P Btwn <. A , c >. /\ P =/= c ) -> ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
43 42 reximdva 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) ) -> ( E. c e. ( EE ` N ) ( P Btwn <. A , c >. /\ P =/= c ) -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
44 31 43 mpd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P ) /\ B Btwn <. P , A >. ) ) -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) )
45 44 expr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P ) ) -> ( B Btwn <. P , A >. -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
46 27 45 jaod 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P ) ) -> ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) -> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
47 simprr1 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> c =/= P )
48 simpll 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) -> N e. NN )
49 simplr1 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) -> P e. ( EE ` N ) )
50 simplr2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) -> A e. ( EE ` N ) )
51 simpr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) -> c e. ( EE ` N ) )
52 simprr2 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> P Btwn <. A , c >. )
53 48 49 50 51 52 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> P Btwn <. c , A >. )
54 simplr3 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) -> B e. ( EE ` N ) )
55 simprr3 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> P Btwn <. B , c >. )
56 48 49 54 51 55 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> P Btwn <. c , B >. )
57 btwnconn2 
 |-  ( ( N e. NN /\ ( c e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( c =/= P /\ P Btwn <. c , A >. /\ P Btwn <. c , B >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
58 48 51 49 50 54 57 syl122anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) -> ( ( c =/= P /\ P Btwn <. c , A >. /\ P Btwn <. c , B >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
59 58 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> ( ( c =/= P /\ P Btwn <. c , A >. /\ P Btwn <. c , B >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
60 47 53 56 59 mp3and 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( ( A =/= P /\ B =/= P ) /\ ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) )
61 60 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ c e. ( EE ` N ) ) /\ ( A =/= P /\ B =/= P ) ) -> ( ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
62 61 an32s 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P ) ) /\ c e. ( EE ` N ) ) -> ( ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
63 62 rexlimdva 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P ) ) -> ( E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
64 46 63 impbid 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P ) ) -> ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) <-> E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
65 64 pm5.32da 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( ( A =/= P /\ B =/= P ) /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( ( A =/= P /\ B =/= P ) /\ E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) )
66 df-3an 
 |-  ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( ( A =/= P /\ B =/= P ) /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
67 df-3an 
 |-  ( ( A =/= P /\ B =/= P /\ E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) <-> ( ( A =/= P /\ B =/= P ) /\ E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) )
68 65 66 67 3bitr4g 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( A =/= P /\ B =/= P /\ E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) )
69 1 68 bitrd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ E. c e. ( EE ` N ) ( c =/= P /\ P Btwn <. A , c >. /\ P Btwn <. B , c >. ) ) ) )