Metamath Proof Explorer


Theorem outsidene2

Description: Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 broutsideof2 ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
2 simp2 ( ( 𝐴𝑃𝐵𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → 𝐵𝑃 )
3 1 2 syl6bi ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ → 𝐵𝑃 ) )