broutsideof3

Description: Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of Schwabhauser p. 43. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	broutsideof3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow (A \neq P \land B \neq P \land \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)))$

Proof

Step	Hyp	Ref	Expression
1		broutsideof2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)))$
2		simpl	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to N \in ℕ$
3		simpr3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to B \in 𝔼 (N)$
4		simpr1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to P \in 𝔼 (N)$
5		btwndiff	$⊢ (N \in ℕ \land B \in 𝔼 (N) \land P \in 𝔼 (N)) \to \exists c \in 𝔼 (N) (P Btwn ⟨B, c⟩ \land P \neq c)$
6	2 3 4 5	syl3anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to \exists c \in 𝔼 (N) (P Btwn ⟨B, c⟩ \land P \neq c)$
7	6	adantr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩)) \to \exists c \in 𝔼 (N) (P Btwn ⟨B, c⟩ \land P \neq c)$
8		df-3an	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \leftrightarrow ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N))$
9		3anass	$⊢ (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c) \leftrightarrow (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land (P Btwn ⟨B, c⟩ \land P \neq c))$
10		simpr3	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to P \neq c$
11	10	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to c \neq P$
12		simp1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \to N \in ℕ$
13		simp23	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \to B \in 𝔼 (N)$
14		simp22	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \to A \in 𝔼 (N)$
15		simp21	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \to P \in 𝔼 (N)$
16		simp3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \to c \in 𝔼 (N)$
17		simpr1r	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to A Btwn ⟨P, B⟩$
18	12 14 15 13 17	btwncomand	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to A Btwn ⟨B, P⟩$
19		simpr2	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to P Btwn ⟨B, c⟩$
20	12 13 14 15 16 18 19	btwnexch3and	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to P Btwn ⟨A, c⟩$
21	11 20 19	3jca	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land P Btwn ⟨B, c⟩ \land P \neq c)) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)$
22	8 9 21	syl2anbr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩) \land (P Btwn ⟨B, c⟩ \land P \neq c))) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)$
23	22	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩)) \to ((P Btwn ⟨B, c⟩ \land P \neq c) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
24	23	an32s	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩)) \land c \in 𝔼 (N)) \to ((P Btwn ⟨B, c⟩ \land P \neq c) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
25	24	reximdva	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩)) \to (\exists c \in 𝔼 (N) (P Btwn ⟨B, c⟩ \land P \neq c) \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
26	7 25	mpd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land A Btwn ⟨P, B⟩)) \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)$
27	26	expr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land (A \neq P \land B \neq P)) \to (A Btwn ⟨P, B⟩ \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
28		simpr2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to A \in 𝔼 (N)$
29		btwndiff	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land P \in 𝔼 (N)) \to \exists c \in 𝔼 (N) (P Btwn ⟨A, c⟩ \land P \neq c)$
30	2 28 4 29	syl3anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to \exists c \in 𝔼 (N) (P Btwn ⟨A, c⟩ \land P \neq c)$
31	30	adantr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩)) \to \exists c \in 𝔼 (N) (P Btwn ⟨A, c⟩ \land P \neq c)$
32		3anass	$⊢ (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c) \leftrightarrow (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land (P Btwn ⟨A, c⟩ \land P \neq c))$
33		simpr3	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to P \neq c$
34	33	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to c \neq P$
35		simpr2	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to P Btwn ⟨A, c⟩$
36		simpr1r	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to B Btwn ⟨P, A⟩$
37	12 13 15 14 36	btwncomand	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to B Btwn ⟨A, P⟩$
38	12 14 13 15 16 37 35	btwnexch3and	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to P Btwn ⟨B, c⟩$
39	34 35 38	3jca	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land P Btwn ⟨A, c⟩ \land P \neq c)) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)$
40	8 32 39	syl2anbr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land (((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩) \land (P Btwn ⟨A, c⟩ \land P \neq c))) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)$
41	40	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩)) \to ((P Btwn ⟨A, c⟩ \land P \neq c) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
42	41	an32s	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩)) \land c \in 𝔼 (N)) \to ((P Btwn ⟨A, c⟩ \land P \neq c) \to (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
43	42	reximdva	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩)) \to (\exists c \in 𝔼 (N) (P Btwn ⟨A, c⟩ \land P \neq c) \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
44	31 43	mpd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land ((A \neq P \land B \neq P) \land B Btwn ⟨P, A⟩)) \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)$
45	44	expr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land (A \neq P \land B \neq P)) \to (B Btwn ⟨P, A⟩ \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
46	27 45	jaod	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land (A \neq P \land B \neq P)) \to ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \to \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
47		simprr1	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to c \neq P$
48		simpll	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \to N \in ℕ$
49		simplr1	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \to P \in 𝔼 (N)$
50		simplr2	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \to A \in 𝔼 (N)$
51		simpr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \to c \in 𝔼 (N)$
52		simprr2	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to P Btwn ⟨A, c⟩$
53	48 49 50 51 52	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to P Btwn ⟨c, A⟩$
54		simplr3	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \to B \in 𝔼 (N)$
55		simprr3	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to P Btwn ⟨B, c⟩$
56	48 49 54 51 55	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to P Btwn ⟨c, B⟩$
57		btwnconn2	$⊢ (N \in ℕ \land (c \in 𝔼 (N) \land P \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((c \neq P \land P Btwn ⟨c, A⟩ \land P Btwn ⟨c, B⟩) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
58	48 51 49 50 54 57	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \to ((c \neq P \land P Btwn ⟨c, A⟩ \land P Btwn ⟨c, B⟩) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
59	58	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to ((c \neq P \land P Btwn ⟨c, A⟩ \land P Btwn ⟨c, B⟩) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
60	47 53 56 59	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land ((A \neq P \land B \neq P) \land (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)$
61	60	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land c \in 𝔼 (N)) \land (A \neq P \land B \neq P)) \to ((c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
62	61	an32s	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land (A \neq P \land B \neq P)) \land c \in 𝔼 (N)) \to ((c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
63	62	rexlimdva	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land (A \neq P \land B \neq P)) \to (\exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
64	46 63	impbid	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land (A \neq P \land B \neq P)) \to ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \leftrightarrow \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
65	64	pm5.32da	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (((A \neq P \land B \neq P) \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \leftrightarrow ((A \neq P \land B \neq P) \land \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)))$
66		df-3an	$⊢ (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \leftrightarrow ((A \neq P \land B \neq P) \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
67		df-3an	$⊢ (A \neq P \land B \neq P \land \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)) \leftrightarrow ((A \neq P \land B \neq P) \land \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩))$
68	65 66 67	3bitr4g	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \leftrightarrow (A \neq P \land B \neq P \land \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)))$
69	1 68	bitrd	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow (A \neq P \land B \neq P \land \exists c \in 𝔼 (N) (c \neq P \land P Btwn ⟨A, c⟩ \land P Btwn ⟨B, c⟩)))$

Metamath Proof Explorer

Theorem broutsideof3

Proof