Metamath Proof Explorer


Theorem outsideofrflx

Description: Reflexitivity of outsideness. Theorem 6.5 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofrflx ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴𝑃𝑃 OutsideOf ⟨ 𝐴 , 𝐴 ⟩ ) )

Proof

Step Hyp Ref Expression
1 axbtwnid ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑃 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝑃 = 𝐴 ) )
2 eqcom ( 𝑃 = 𝐴𝐴 = 𝑃 )
3 1 2 syl6ib ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑃 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝐴 = 𝑃 ) )
4 3 necon3ad ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴𝑃 → ¬ 𝑃 Btwn ⟨ 𝐴 , 𝐴 ⟩ ) )
5 colineartriv2 ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 Colinear ⟨ 𝐴 , 𝐴 ⟩ )
6 4 5 jctild ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴𝑃 → ( 𝑃 Colinear ⟨ 𝐴 , 𝐴 ⟩ ∧ ¬ 𝑃 Btwn ⟨ 𝐴 , 𝐴 ⟩ ) ) )
7 broutsideof ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐴 ⟩ ↔ ( 𝑃 Colinear ⟨ 𝐴 , 𝐴 ⟩ ∧ ¬ 𝑃 Btwn ⟨ 𝐴 , 𝐴 ⟩ ) )
8 6 7 syl6ibr ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴𝑃𝑃 OutsideOf ⟨ 𝐴 , 𝐴 ⟩ ) )