Theorem outsidene1

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

	Ref	Expression
Assertion	outsidene1	$$⊢\left(N\in \mathbb{N}\wedge \left(P\in 𝔼\left(N\right)\wedge A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\right)\to \left(P\mathrm{OutsideOf}⟨A,B⟩\to A\ne P\right)$$

Proof

Step	Hyp	Ref	Expression
1		broutsideof2	$$⊢\left(N\in \mathbb{N}\wedge \left(P\in 𝔼\left(N\right)\wedge A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\right)\to \left(P\mathrm{OutsideOf}⟨A,B⟩\leftrightarrow \left(A\ne P\wedge B\ne P\wedge \left(A\mathrm{Btwn}⟨P,B⟩\vee B\mathrm{Btwn}⟨P,A⟩\right)\right)\right)$$
2		simp1	$$⊢\left(A\ne P\wedge B\ne P\wedge \left(A\mathrm{Btwn}⟨P,B⟩\vee B\mathrm{Btwn}⟨P,A⟩\right)\right)\to A\ne P$$
3	1 2	syl6bi	$$⊢\left(N\in \mathbb{N}\wedge \left(P\in 𝔼\left(N\right)\wedge A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\right)\to \left(P\mathrm{OutsideOf}⟨A,B⟩\to A\ne P\right)$$