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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C A P
3 simpr12 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C B P
4 simpr13 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C C P
5 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N N
6 simp3r N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P 𝔼 N
7 simp2l N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A 𝔼 N
8 simp3l N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N C 𝔼 N
9 simpr2 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C P Btwn C A
11 simp2r N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N B 𝔼 N
12 simpr3 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C P Btwn C B
14 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
15 14 3com23 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N C P P Btwn C A P Btwn C B A Btwn P B B Btwn P A
16 15 adantr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C A Btwn P B A P
24 simpr3 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C A Btwn P B A Btwn B P
26 simpr2 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C A Btwn P B P Btwn A C
27 btwnouttr2 N B 𝔼 N A 𝔼 N P 𝔼 N C 𝔼 N A P A Btwn B P P Btwn A C P Btwn B C
28 5 11 7 6 8 27 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P A Btwn B P P Btwn A C P Btwn B C
29 28 adantr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C A Btwn P B P Btwn B C
31 22 30 sylan2br N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C A Btwn P B P Btwn B C
32 31 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C B Btwn P A B Btwn A P
36 simpr2 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C B Btwn P A P Btwn B C
38 33 37 sylan2br N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C B Btwn P A P Btwn B C
39 38 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C B Btwn P A P Btwn B C
40 32 39 jaod N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 P 𝔼 N A 𝔼 N B 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A B A P B P A Btwn P B B Btwn P A
45 44 adantr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C P OutsideOf A B
47 46 ex N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P P Btwn A C P Btwn B C P OutsideOf A B