btwnoutside

Description: A principle linking outsideness to betweenness. Theorem 6.2 of Schwabhauser p. 43. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		df-3an	$⊢ ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land P Btwn ⟨B, C⟩) \leftrightarrow (((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩) \land P Btwn ⟨B, C⟩)$
2		simpr11	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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 \neq P$
3		simpr12	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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 B \neq P$
4		simpr13	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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$
5		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to N \in ℕ$
6		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to P \in 𝔼 (N)$
7		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to A \in 𝔼 (N)$
8		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to C \in 𝔼 (N)$
9		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩$
10	5 6 7 8 9	btwncomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩$
11		simp2r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to B \in 𝔼 (N)$
12		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩$
13	5 6 11 8 12	btwncomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩$
14		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⟩))$
15	14	3com23	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩))$
16	15	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩))$
17	4 10 13 16	mp3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩)$
18	2 3 17	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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 \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
19	1 18	sylan2br	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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 \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
20	19	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to (P Btwn ⟨B, C⟩ \to (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)))$
21		simp3	$⊢ (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \to (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)$
22		df-3an	$⊢ ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩) \leftrightarrow (((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩) \land A Btwn ⟨P, B⟩)$
23		simpr11	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩)) \to A \neq P$
24		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩)) \to A Btwn ⟨P, B⟩$
25	5 7 6 11 24	btwncomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩)) \to A Btwn ⟨B, P⟩$
26		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩)) \to P Btwn ⟨A, C⟩$
27		btwnouttr2	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land A \in 𝔼 (N)) \land (P \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((A \neq P \land A Btwn ⟨B, P⟩ \land P Btwn ⟨A, C⟩) \to P Btwn ⟨B, C⟩)$
28	5 11 7 6 8 27	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((A \neq P \land A Btwn ⟨B, P⟩ \land P Btwn ⟨A, C⟩) \to P Btwn ⟨B, C⟩)$
29	28	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩)) \to ((A \neq P \land A Btwn ⟨B, P⟩ \land P Btwn ⟨A, C⟩) \to P Btwn ⟨B, C⟩)$
30	23 25 26 29	mp3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land A Btwn ⟨P, B⟩)) \to P Btwn ⟨B, C⟩$
31	22 30	sylan2br	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩) \land A Btwn ⟨P, B⟩)) \to P Btwn ⟨B, C⟩$
32	31	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to (A Btwn ⟨P, B⟩ \to P Btwn ⟨B, C⟩)$
33		df-3an	$⊢ ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land B Btwn ⟨P, A⟩) \leftrightarrow (((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩) \land B Btwn ⟨P, A⟩)$
34		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land B Btwn ⟨P, A⟩)) \to B Btwn ⟨P, A⟩$
35	5 11 6 7 34	btwncomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land B Btwn ⟨P, A⟩)) \to B Btwn ⟨A, P⟩$
36		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land B Btwn ⟨P, A⟩)) \to P Btwn ⟨A, C⟩$
37	5 7 11 6 8 35 36	btwnexch3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩ \land B Btwn ⟨P, A⟩)) \to P Btwn ⟨B, C⟩$
38	33 37	sylan2br	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩) \land B Btwn ⟨P, A⟩)) \to P Btwn ⟨B, C⟩$
39	38	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to (B Btwn ⟨P, A⟩ \to P Btwn ⟨B, C⟩)$
40	32 39	jaod	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \to P Btwn ⟨B, C⟩)$
41	21 40	syl5	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to ((A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \to P Btwn ⟨B, C⟩)$
42	20 41	impbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to (P Btwn ⟨B, C⟩ \leftrightarrow (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)))$
43		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⟩)))$
44	5 6 7 11 43	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \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⟩)))$
45	44	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)))$
46	42 45	bitr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩)) \to (P Btwn ⟨B, C⟩ \leftrightarrow P OutsideOf ⟨A, B⟩)$
47	46	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to (((A \neq P \land B \neq P \land C \neq P) \land P Btwn ⟨A, C⟩) \to (P Btwn ⟨B, C⟩ \leftrightarrow P OutsideOf ⟨A, B⟩))$

Metamath Proof Explorer

Theorem btwnoutside

Proof