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

Proof

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