Metamath Proof Explorer

Theorem btwnoutside

Description: A principle linking outsideness to betweenness. Theorem 6.2 of Schwabhauser p. 43. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) <-> ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) /\ P Btwn <. B , C >. ) )
2 simpr11 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> A =/= P )
3 simpr12 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> B =/= P )
4 simpr13 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> C =/= P )
5 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> N e. NN )
6 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
7 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
8 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
9 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> P Btwn <. A , C >. )
10 5 6 7 8 9 btwncomand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> P Btwn <. C , A >. )
11 simp2r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
12 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> P Btwn <. B , C >. )
13 5 6 11 8 12 btwncomand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> P Btwn <. C , B >. )
14 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 >. ) ) )
15 14 3com23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( C =/= P /\ P Btwn <. C , A >. /\ P Btwn <. C , B >. ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
16 15 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P 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 >. ) ) )
17 4 10 13 16 mp3and 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P 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 >. ) )
18 2 3 17 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ P Btwn <. B , C >. ) ) -> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
19 1 18 sylan2br 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) /\ P Btwn <. B , C >. ) ) -> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
20 19 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( P Btwn <. B , C >. -> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
21 simp3 
 |-  ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) )
22 df-3an 
 |-  ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) <-> ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) /\ A Btwn <. P , B >. ) )
23 simpr11 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) ) -> A =/= P )
24 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) ) -> A Btwn <. P , B >. )
25 5 7 6 11 24 btwncomand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) ) -> A Btwn <. B , P >. )
26 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) ) -> P Btwn <. A , C >. )
27 btwnouttr2 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A =/= P /\ A Btwn <. B , P >. /\ P Btwn <. A , C >. ) -> P Btwn <. B , C >. ) )
28 5 11 7 6 8 27 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( A =/= P /\ A Btwn <. B , P >. /\ P Btwn <. A , C >. ) -> P Btwn <. B , C >. ) )
29 28 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) ) -> ( ( A =/= P /\ A Btwn <. B , P >. /\ P Btwn <. A , C >. ) -> P Btwn <. B , C >. ) )
30 23 25 26 29 mp3and 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ A Btwn <. P , B >. ) ) -> P Btwn <. B , C >. )
31 22 30 sylan2br 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) /\ A Btwn <. P , B >. ) ) -> P Btwn <. B , C >. )
32 31 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( A Btwn <. P , B >. -> P Btwn <. B , C >. ) )
33 df-3an 
 |-  ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ B Btwn <. P , A >. ) <-> ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) /\ B Btwn <. P , A >. ) )
34 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ B Btwn <. P , A >. ) ) -> B Btwn <. P , A >. )
35 5 11 6 7 34 btwncomand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ B Btwn <. P , A >. ) ) -> B Btwn <. A , P >. )
36 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ B Btwn <. P , A >. ) ) -> P Btwn <. A , C >. )
37 5 7 11 6 8 35 36 btwnexch3and 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. /\ B Btwn <. P , A >. ) ) -> P Btwn <. B , C >. )
38 33 37 sylan2br 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) /\ B Btwn <. P , A >. ) ) -> P Btwn <. B , C >. )
39 38 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( B Btwn <. P , A >. -> P Btwn <. B , C >. ) )
40 32 39 jaod 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) -> P Btwn <. B , C >. ) )
41 21 40 syl5 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) -> P Btwn <. B , C >. ) )
42 20 41 impbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( P Btwn <. B , C >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
43 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 >. ) ) ) )
44 5 6 7 11 43 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
45 44 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
46 42 45 bitr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) ) -> ( P Btwn <. B , C >. <-> P OutsideOf <. A , B >. ) )
47 46 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ P Btwn <. A , C >. ) -> ( P Btwn <. B , C >. <-> P OutsideOf <. A , B >. ) ) )