Metamath Proof Explorer

Theorem outsidele

Description: Relate OutsideOf to Seg<_ . Theorem 6.13 of Schwabhauser p. 45. (Contributed by Scott Fenton, 24-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsidele ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ↔ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
5 brsegle2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) )
6 1 2 3 2 4 5 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) )
8 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ )
9 outsideofcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ) )
10 9 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ) )
11 8 10 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ )
12 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
13 simplr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simplr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
15 12 13 14 cgrrflxd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝑃 , 𝐵 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ )
16 15 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ⟨ 𝑃 , 𝐵 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ )
17 11 16 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝐵 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) )
18 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ )
19 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
20 simplr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
21 btwncolinear1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ → 𝑃 Colinear ⟨ 𝑦 , 𝐴 ⟩ ) )
22 12 13 19 20 21 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ → 𝑃 Colinear ⟨ 𝑦 , 𝐴 ⟩ ) )
23 22 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ → 𝑃 Colinear ⟨ 𝑦 , 𝐴 ⟩ ) )
24 18 23 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝑃 Colinear ⟨ 𝑦 , 𝐴 ⟩ )
25 outsidene1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 ≠ 𝑃 ) )
26 25 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 ≠ 𝑃 ) )
27 8 26 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐴 ≠ 𝑃 )
28 27 neneqd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ¬ 𝐴 = 𝑃 )
29 df-3an ⊢ ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ↔ ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) )
30 simpr2l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ )
31 12 20 13 19 30 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ) → 𝐴 Btwn ⟨ 𝑦 , 𝑃 ⟩ )
32 simpr3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ) → 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ )
33 btwnswapid2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝑦 , 𝑃 ⟩ ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) → 𝐴 = 𝑃 ) )
34 12 20 19 13 33 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Btwn ⟨ 𝑦 , 𝑃 ⟩ ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) → 𝐴 = 𝑃 ) )
35 34 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ) → ( ( 𝐴 Btwn ⟨ 𝑦 , 𝑃 ⟩ ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) → 𝐴 = 𝑃 ) )
36 31 32 35 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ) → 𝐴 = 𝑃 )
37 29 36 sylan2br ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ∧ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) ) → 𝐴 = 𝑃 )
38 37 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ → 𝐴 = 𝑃 ) )
39 28 38 mtod ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ¬ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ )
40 broutsideof ⊢ ( 𝑃 OutsideOf ⟨ 𝑦 , 𝐴 ⟩ ↔ ( 𝑃 Colinear ⟨ 𝑦 , 𝐴 ⟩ ∧ ¬ 𝑃 Btwn ⟨ 𝑦 , 𝐴 ⟩ ) )
41 24 39 40 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝑃 OutsideOf ⟨ 𝑦 , 𝐴 ⟩ )
42 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ )
43 41 42 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝑃 OutsideOf ⟨ 𝑦 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) )
44 outsideofeq ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝐵 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ ( 𝑃 OutsideOf ⟨ 𝑦 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐵 = 𝑦 ) )
45 12 13 20 13 14 14 19 44 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝐵 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ ( 𝑃 OutsideOf ⟨ 𝑦 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐵 = 𝑦 ) )
46 45 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( ( ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝐵 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ∧ ( 𝑃 OutsideOf ⟨ 𝑦 , 𝐴 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐵 = 𝑦 ) )
47 17 43 46 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐵 = 𝑦 )
48 opeq2 ⊢ ( 𝐵 = 𝑦 → ⟨ 𝑃 , 𝐵 ⟩ = ⟨ 𝑃 , 𝑦 ⟩ )
49 48 breq2d ⊢ ( 𝐵 = 𝑦 → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ↔ 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ) )
50 18 49 syl5ibrcom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝐵 = 𝑦 → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
51 47 50 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
52 51 an4s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
53 52 rexlimdvaa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝑃 , 𝑦 ⟩ ∧ ⟨ 𝑃 , 𝑦 ⟩ Cgr ⟨ 𝑃 , 𝐵 ⟩ ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
54 7 53 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
55 btwnsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ → ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ) )
56 55 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ → ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ) )
57 54 56 impbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ) → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ↔ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
58 57 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ → ( ⟨ 𝑃 , 𝐴 ⟩ Seg≤ ⟨ 𝑃 , 𝐵 ⟩ ↔ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) )