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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ( 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 df-3an ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
2 simpr11 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝐴𝑃 )
3 simpr12 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝐵𝑃 )
4 simpr13 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝐶𝑃 )
5 simp1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
6 simp3r ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simp2l ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simp3l ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simpr2 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
10 5 6 7 8 9 btwncomand ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐶 , 𝐴 ⟩ )
11 simp2r ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simpr3 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ )
13 5 6 11 8 12 btwncomand ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐶 , 𝐵 ⟩ )
14 btwnconn2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶𝑃𝑃 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∧ 𝑃 Btwn ⟨ 𝐶 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
15 14 3com23 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶𝑃𝑃 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∧ 𝑃 Btwn ⟨ 𝐶 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
16 15 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( ( 𝐶𝑃𝑃 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∧ 𝑃 Btwn ⟨ 𝐶 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
17 4 10 13 16 mp3and ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
18 2 3 17 3jca ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
19 1 18 sylan2br ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
20 19 expr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
21 simp3 ( ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
22 df-3an ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ↔ ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
23 simpr11 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐴𝑃 )
24 simpr3 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
25 5 7 6 11 24 btwncomand ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐴 Btwn ⟨ 𝐵 , 𝑃 ⟩ )
26 simpr2 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
27 btwnouttr2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴𝑃𝐴 Btwn ⟨ 𝐵 , 𝑃 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
28 5 11 7 6 8 27 syl122anc ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴𝑃𝐴 Btwn ⟨ 𝐵 , 𝑃 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
29 28 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( ( 𝐴𝑃𝐴 Btwn ⟨ 𝐵 , 𝑃 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
30 23 25 26 29 mp3and ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ )
31 22 30 sylan2br ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ )
32 31 expr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
33 df-3an ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ↔ ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
34 simpr3 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ )
35 5 11 6 7 34 btwncomand ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝑃 ⟩ )
36 simpr2 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
37 5 7 11 6 8 35 36 btwnexch3and ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ )
38 33 37 sylan2br ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ )
39 38 expr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
40 32 39 jaod ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
41 21 40 syl5 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
42 20 41 impbid ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
43 broutsideof2 ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
44 5 6 7 11 43 syl13anc ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
45 44 adantr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
46 42 45 bitr4d ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) → ( 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) )
47 46 ex ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴𝑃𝐵𝑃𝐶𝑃 ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ( 𝑃 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) ) )