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 P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B A P B P c 𝔼 N c P P Btwn A c P Btwn B c

Proof

Step Hyp Ref Expression
1 broutsideof2 N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B A P B P A Btwn P B B Btwn P A
2 simpl N P 𝔼 N A 𝔼 N B 𝔼 N N
3 simpr3 N P 𝔼 N A 𝔼 N B 𝔼 N B 𝔼 N
4 simpr1 N P 𝔼 N A 𝔼 N B 𝔼 N P 𝔼 N
5 btwndiff N B 𝔼 N P 𝔼 N c 𝔼 N P Btwn B c P c
6 2 3 4 5 syl3anc N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N P Btwn B c P c
7 6 adantr N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B c 𝔼 N P Btwn B c P c
8 df-3an N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P A Btwn P B P Btwn B c P c P c
11 10 necomd N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P A Btwn P B P Btwn B c P c c P
12 simp1 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N N
13 simp23 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N B 𝔼 N
14 simp22 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A 𝔼 N
15 simp21 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N P 𝔼 N
16 simp3 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N c 𝔼 N
17 simpr1r N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P A Btwn P B P Btwn B c P c A Btwn B P
19 simpr2 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B c 𝔼 N P Btwn B c P c c P P Btwn A c P Btwn B c
25 24 reximdva N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B c 𝔼 N P Btwn B c P c c 𝔼 N c P P Btwn A c P Btwn B c
26 7 25 mpd N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B c 𝔼 N c P P Btwn A c P Btwn B c
27 26 expr N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B c 𝔼 N c P P Btwn A c P Btwn B c
28 simpr2 N P 𝔼 N A 𝔼 N B 𝔼 N A 𝔼 N
29 btwndiff N A 𝔼 N P 𝔼 N c 𝔼 N P Btwn A c P c
30 2 28 4 29 syl3anc N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N P Btwn A c P c
31 30 adantr N P 𝔼 N A 𝔼 N B 𝔼 N A P B P B Btwn P A c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P B Btwn P A P Btwn A c P c P c
34 33 necomd N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P B Btwn P A P Btwn A c P c c P
35 simpr2 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P B Btwn P A P Btwn A c P c P Btwn A c
36 simpr1r N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N A P B P B Btwn P A c 𝔼 N P Btwn A c P c c P P Btwn A c P Btwn B c
43 42 reximdva N P 𝔼 N A 𝔼 N B 𝔼 N A P B P B Btwn P A c 𝔼 N P Btwn A c P c c 𝔼 N c P P Btwn A c P Btwn B c
44 31 43 mpd N P 𝔼 N A 𝔼 N B 𝔼 N A P B P B Btwn P A c 𝔼 N c P P Btwn A c P Btwn B c
45 44 expr N P 𝔼 N A 𝔼 N B 𝔼 N A P B P B Btwn P A c 𝔼 N c P P Btwn A c P Btwn B c
46 27 45 jaod N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B B Btwn P A c 𝔼 N c P P Btwn A c P Btwn B c
47 simprr1 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P c P P Btwn A c P Btwn B c c P
48 simpll N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N N
49 simplr1 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N P 𝔼 N
50 simplr2 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A 𝔼 N
51 simpr N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N c 𝔼 N
52 simprr2 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P c P P Btwn A c P Btwn B c P Btwn c A
54 simplr3 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N B 𝔼 N
55 simprr3 N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N A P B P c P P Btwn A c P Btwn B c P Btwn c B
57 btwnconn2 N c 𝔼 N P 𝔼 N A 𝔼 N B 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 N c P P Btwn c A P Btwn c B A Btwn P B B Btwn P A
59 58 adantr N P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N c 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 N A P B P c 𝔼 N c P P Btwn A c P Btwn B c A Btwn P B B Btwn P A
63 62 rexlimdva N P 𝔼 N A 𝔼 N B 𝔼 N A P B P c 𝔼 N c P P Btwn A c P Btwn B c A Btwn P B B Btwn P A
64 46 63 impbid N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B B Btwn P A c 𝔼 N c P P Btwn A c P Btwn B c
65 64 pm5.32da N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B B Btwn P A A P B P c 𝔼 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 c 𝔼 N c P P Btwn A c P Btwn B c A P B P c 𝔼 N c P P Btwn A c P Btwn B c
68 65 66 67 3bitr4g N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B B Btwn P A A P B P c 𝔼 N c P P Btwn A c P Btwn B c
69 1 68 bitrd N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B A P B P c 𝔼 N c P P Btwn A c P Btwn B c