Metamath Proof Explorer

Theorem broutsideof2

Description: Alternate form of OutsideOf . Definition 6.1 of Schwabhauser p. 43. (Contributed by Scott Fenton, 17-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion 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 >. ) ) ) )

Proof

Step Hyp Ref Expression
1 broutsideof 
 |-  ( P OutsideOf <. A , B >. <-> ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) )
2 btwntriv1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Btwn <. A , B >. )
3 2 3adant3r1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> A Btwn <. A , B >. )
4 breq1 
 |-  ( A = P -> ( A Btwn <. A , B >. <-> P Btwn <. A , B >. ) )
5 3 4 syl5ibcom 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A = P -> P Btwn <. A , B >. ) )
6 5 necon3bd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( -. P Btwn <. A , B >. -> A =/= P ) )
7 6 imp 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ -. P Btwn <. A , B >. ) -> A =/= P )
8 7 adantrl 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) ) -> A =/= P )
9 btwntriv2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B Btwn <. A , B >. )
10 9 3adant3r1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> B Btwn <. A , B >. )
11 breq1 
 |-  ( B = P -> ( B Btwn <. A , B >. <-> P Btwn <. A , B >. ) )
12 10 11 syl5ibcom 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( B = P -> P Btwn <. A , B >. ) )
13 12 necon3bd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( -. P Btwn <. A , B >. -> B =/= P ) )
14 13 imp 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ -. P Btwn <. A , B >. ) -> B =/= P )
15 14 adantrl 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) ) -> B =/= P )
16 brcolinear 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P Colinear <. A , B >. <-> ( P Btwn <. A , B >. \/ A Btwn <. B , P >. \/ B Btwn <. P , A >. ) ) )
17 pm2.24 
 |-  ( P Btwn <. A , B >. -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
18 17 a1i 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P Btwn <. A , B >. -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
19 3anrot 
 |-  ( ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ P e. ( EE ` N ) ) )
20 btwncom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( A Btwn <. B , P >. <-> A Btwn <. P , B >. ) )
21 19 20 sylan2b 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. B , P >. <-> A Btwn <. P , B >. ) )
22 orc 
 |-  ( A Btwn <. P , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) )
23 21 22 syl6bi 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. B , P >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
24 23 a1dd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. B , P >. -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
25 olc 
 |-  ( B Btwn <. P , A >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) )
26 25 a1d 
 |-  ( B Btwn <. P , A >. -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
27 26 a1i 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( B Btwn <. P , A >. -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
28 18 24 27 3jaod 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( P Btwn <. A , B >. \/ A Btwn <. B , P >. \/ B Btwn <. P , A >. ) -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
29 16 28 sylbid 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P Colinear <. A , B >. -> ( -. P Btwn <. A , B >. -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
30 29 imp32 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) )
31 8 15 30 3jca 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) ) -> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
32 simp3 
 |-  ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) -> ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) )
33 3ancomb 
 |-  ( ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( P e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
34 btwncolinear2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( A Btwn <. P , B >. -> P Colinear <. A , B >. ) )
35 33 34 sylan2b 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. P , B >. -> P Colinear <. A , B >. ) )
36 btwncolinear1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( B Btwn <. P , A >. -> P Colinear <. A , B >. ) )
37 35 36 jaod 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) -> P Colinear <. A , B >. ) )
38 32 37 syl5 
 |-  ( ( 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 >. ) ) -> P Colinear <. A , B >. ) )
39 38 imp 
 |-  ( ( ( 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 >. ) ) ) -> P Colinear <. A , B >. )
40 simpr2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) ) -> A =/= P )
41 40 neneqd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) ) -> -. A = P )
42 simprl1 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> A Btwn <. P , B >. )
43 simprr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> P Btwn <. A , B >. )
44 simpl 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> N e. NN )
45 simpr2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
46 simpr1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
47 simpr3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
48 btwnswapid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ P e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A Btwn <. P , B >. /\ P Btwn <. A , B >. ) -> A = P ) )
49 44 45 46 47 48 syl13anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A Btwn <. P , B >. /\ P Btwn <. A , B >. ) -> A = P ) )
50 49 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> ( ( A Btwn <. P , B >. /\ P Btwn <. A , B >. ) -> A = P ) )
51 42 43 50 mp2and 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> A = P )
52 51 expr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) ) -> ( P Btwn <. A , B >. -> A = P ) )
53 41 52 mtod 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( A Btwn <. P , B >. /\ A =/= P /\ B =/= P ) ) -> -. P Btwn <. A , B >. )
54 53 3exp2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. P , B >. -> ( A =/= P -> ( B =/= P -> -. P Btwn <. A , B >. ) ) ) )
55 simpr3 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) ) -> B =/= P )
56 55 neneqd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) ) -> -. B = P )
57 simprl1 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> B Btwn <. P , A >. )
58 simprr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> P Btwn <. A , B >. )
59 44 46 45 47 58 btwncomand 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> P Btwn <. B , A >. )
60 3anrot 
 |-  ( ( B e. ( EE ` N ) /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) <-> ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
61 btwnswapid 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( ( B Btwn <. P , A >. /\ P Btwn <. B , A >. ) -> B = P ) )
62 60 61 sylan2br 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( B Btwn <. P , A >. /\ P Btwn <. B , A >. ) -> B = P ) )
63 62 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> ( ( B Btwn <. P , A >. /\ P Btwn <. B , A >. ) -> B = P ) )
64 57 59 63 mp2and 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) /\ P Btwn <. A , B >. ) ) -> B = P )
65 64 expr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) ) -> ( P Btwn <. A , B >. -> B = P ) )
66 56 65 mtod 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ ( B Btwn <. P , A >. /\ A =/= P /\ B =/= P ) ) -> -. P Btwn <. A , B >. )
67 66 3exp2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( B Btwn <. P , A >. -> ( A =/= P -> ( B =/= P -> -. P Btwn <. A , B >. ) ) ) )
68 54 67 jaod 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) -> ( A =/= P -> ( B =/= P -> -. P Btwn <. A , B >. ) ) ) )
69 68 com12 
 |-  ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) -> ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A =/= P -> ( B =/= P -> -. P Btwn <. A , B >. ) ) ) )
70 69 com4l 
 |-  ( ( 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 >. ) -> -. P Btwn <. A , B >. ) ) ) )
71 70 3imp2 
 |-  ( ( ( 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 >. ) ) ) -> -. P Btwn <. A , B >. )
72 39 71 jca 
 |-  ( ( ( 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 >. ) ) ) -> ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) )
73 31 72 impbida 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( P Colinear <. A , B >. /\ -. P Btwn <. A , B >. ) <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
74 1 73 syl5bb 
 |-  ( ( 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 >. ) ) ) )