Description: Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | outsidene2 | ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 → 𝐵 ≠ 𝑃 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | broutsideof2 | ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) ) | |
2 | simp2 | ⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝐵 ≠ 𝑃 ) | |
3 | 1 2 | syl6bi | ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 → 𝐵 ≠ 𝑃 ) ) |