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