btwnconn3

Description: Inner connectivity law for betweenness. Theorem 5.3 of Schwabhauser p. 41. (Contributed by Scott Fenton, 9-Oct-2013)

		Ref	Expression
	Assertion	btwnconn3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to N \in ℕ$
2		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to D \in 𝔼 (N)$
3		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to A \in 𝔼 (N)$
4		btwndiff	$⊢ (N \in ℕ \land D \in 𝔼 (N) \land A \in 𝔼 (N)) \to \exists p \in 𝔼 (N) (A Btwn ⟨D, p⟩ \land A \neq p)$
5	1 2 3 4	syl3anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists p \in 𝔼 (N) (A Btwn ⟨D, p⟩ \land A \neq p)$
6		simprlr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to A \neq p$
7	6	necomd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to p \neq A$
8		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to N \in ℕ$
9		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to A \in 𝔼 (N)$
10		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to B \in 𝔼 (N)$
11		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to p \in 𝔼 (N)$
12		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to D \in 𝔼 (N)$
13		simprrl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to B Btwn ⟨A, D⟩$
14	8 10 9 12 13	btwncomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to B Btwn ⟨D, A⟩$
15		simprll	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to A Btwn ⟨D, p⟩$
16	8 12 10 9 11 14 15	btwnexch3and	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to A Btwn ⟨B, p⟩$
17	8 9 10 11 16	btwncomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to A Btwn ⟨p, B⟩$
18		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to C \in 𝔼 (N)$
19		simprrr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to C Btwn ⟨A, D⟩$
20	8 18 9 12 19	btwncomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to C Btwn ⟨D, A⟩$
21	8 12 18 9 11 20 15	btwnexch3and	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to A Btwn ⟨C, p⟩$
22	8 9 18 11 21	btwncomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to A Btwn ⟨p, C⟩$
23	7 17 22	3jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \land ((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩))) \to (p \neq A \land A Btwn ⟨p, B⟩ \land A Btwn ⟨p, C⟩)$
24	23	ex	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to (((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩)) \to (p \neq A \land A Btwn ⟨p, B⟩ \land A Btwn ⟨p, C⟩))$
25		btwnconn2	$⊢ (N \in ℕ \land (p \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((p \neq A \land A Btwn ⟨p, B⟩ \land A Btwn ⟨p, C⟩) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩))$
26	8 11 9 10 18 25	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to ((p \neq A \land A Btwn ⟨p, B⟩ \land A Btwn ⟨p, C⟩) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩))$
27	24 26	syld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to (((A Btwn ⟨D, p⟩ \land A \neq p) \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩)) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩))$
28	27	expd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land p \in 𝔼 (N)) \to ((A Btwn ⟨D, p⟩ \land A \neq p) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩)))$
29	28	rexlimdva	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists p \in 𝔼 (N) (A Btwn ⟨D, p⟩ \land A \neq p) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩)))$
30	5 29	mpd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨A, D⟩) \to (B Btwn ⟨A, C⟩ \lor C Btwn ⟨A, B⟩))$

Metamath Proof Explorer

Theorem btwnconn3

Proof