Metamath Proof Explorer

Theorem btwnconn1

Description: Connectitivy law for betweenness. Theorem 5.1 of Schwabhauser p. 39-41. (Contributed by Scott Fenton, 9-Oct-2013)

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

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ B = C \to (B Btwn ⟨A, D⟩ \leftrightarrow C Btwn ⟨A, D⟩)$
2	1	3anbi3d	$⊢ B = C \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \leftrightarrow (A \neq B \land B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩))$
3		orc	$⊢ C Btwn ⟨A, D⟩ \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩)$
4	3	3ad2ant3	$⊢ (A \neq B \land B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩)$
5	2 4	syl6bi	$⊢ B = C \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩))$
6	5	adantld	$⊢ B = C \to (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩))$
7		simpr1	$⊢ (B \neq C \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to A \neq B$
8		simpl	$⊢ (B \neq C \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to B \neq C$
9		3simpc	$⊢ (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)$
10	9	adantl	$⊢ (B \neq C \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)$
11	7 8 10	jca31	$⊢ (B \neq C \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to ((A \neq B \land B \neq C) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩))$
12		btwnconn1lem14	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land ((A \neq B \land B \neq C) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩))) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩)$
13	11 12	sylan2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩))) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩)$
14	13	an12s	$⊢ (B \neq C \land ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩))) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩)$
15	14	ex	$⊢ B \neq C \to (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩))$
16	6 15	pm2.61ine	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩)$
17	16	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩))$