Theorem outsideofrflx

Description: Reflexivity 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 ⟨ 𝐴 , 𝐴 ⟩ ) )