btwnconn1lem4

Description: Lemma for btwnconn1 . Assuming C =/= c , we now attempt to force D = d from here out via a series of congruences. (Contributed by Scott Fenton, 8-Oct-2013)

		Ref	Expression
	Assertion	btwnconn1lem4	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨d, c⟩ Cgr ⟨D, C⟩$

Proof

Step	Hyp	Ref	Expression
1		simp1rl	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to B Btwn ⟨A, C⟩$
2		simp2rl	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to C Btwn ⟨A, d⟩$
3	1 2	jca	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to (B Btwn ⟨A, C⟩ \land C Btwn ⟨A, d⟩)$
4	3	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to (B Btwn ⟨A, C⟩ \land C Btwn ⟨A, d⟩)$
5		simp11	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to N \in ℕ$
6		simp12	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to A \in 𝔼 (N)$
7		simp13	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to B \in 𝔼 (N)$
8		simp21	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to C \in 𝔼 (N)$
9		simp3l	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to d \in 𝔼 (N)$
10		btwnexch3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, d⟩) \to C Btwn ⟨B, d⟩)$
11	5 6 7 8 9 10	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, d⟩) \to C Btwn ⟨B, d⟩)$
12	11	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, d⟩) \to C Btwn ⟨B, d⟩)$
13	4 12	mpd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to C Btwn ⟨B, d⟩$
14		simp3lr	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to ⟨c, b⟩ Cgr ⟨C, B⟩$
15	14	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨c, b⟩ Cgr ⟨C, B⟩$
16		simp23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to c \in 𝔼 (N)$
17		simp3r	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to b \in 𝔼 (N)$
18		cgrcomlr	$⊢ (N \in ℕ \land (c \in 𝔼 (N) \land b \in 𝔼 (N)) \land (C \in 𝔼 (N) \land B \in 𝔼 (N))) \to (⟨c, b⟩ Cgr ⟨C, B⟩ \leftrightarrow ⟨b, c⟩ Cgr ⟨B, C⟩)$
19	5 16 17 8 7 18	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to (⟨c, b⟩ Cgr ⟨C, B⟩ \leftrightarrow ⟨b, c⟩ Cgr ⟨B, C⟩)$
20		cgrcom	$⊢ (N \in ℕ \land (b \in 𝔼 (N) \land c \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨b, c⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨b, c⟩)$
21	5 17 16 7 8 20	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to (⟨b, c⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨b, c⟩)$
22	19 21	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to (⟨c, b⟩ Cgr ⟨C, B⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨b, c⟩)$
23	22	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to (⟨c, b⟩ Cgr ⟨C, B⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨b, c⟩)$
24	15 23	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨B, C⟩ Cgr ⟨b, c⟩$
25		3simpa	$⊢ (A \neq B \land B \neq C \land C \neq c) \to (A \neq B \land B \neq C)$
26	25	anim1i	$⊢ ((A \neq B \land B \neq C \land C \neq c) \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⟩))$
27		btwnconn1lem3	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨B, d⟩ Cgr ⟨b, D⟩$
28	26 27	syl3anr1	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨B, d⟩ Cgr ⟨b, D⟩$
29		simp22	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to D \in 𝔼 (N)$
30		simp2rr	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to ⟨C, d⟩ Cgr ⟨C, D⟩$
31	30	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨C, d⟩ Cgr ⟨C, D⟩$
32		simp2lr	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to ⟨D, c⟩ Cgr ⟨C, D⟩$
33	32	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨D, c⟩ Cgr ⟨C, D⟩$
34	5 29 16 8 29 33	cgrcomland	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨c, D⟩ Cgr ⟨C, D⟩$
35	5 8 9 16 29 8 29 31 34	cgrtr3and	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨C, d⟩ Cgr ⟨c, D⟩$
36		brcgr3	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land d \in 𝔼 (N)) \land (b \in 𝔼 (N) \land c \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \leftrightarrow (⟨B, C⟩ Cgr ⟨b, c⟩ \land ⟨B, d⟩ Cgr ⟨b, D⟩ \land ⟨C, d⟩ Cgr ⟨c, D⟩))$
37	5 7 8 9 17 16 29 36	syl133anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to (⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \leftrightarrow (⟨B, C⟩ Cgr ⟨b, c⟩ \land ⟨B, d⟩ Cgr ⟨b, D⟩ \land ⟨C, d⟩ Cgr ⟨c, D⟩))$
38	37	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to (⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \leftrightarrow (⟨B, C⟩ Cgr ⟨b, c⟩ \land ⟨B, d⟩ Cgr ⟨b, D⟩ \land ⟨C, d⟩ Cgr ⟨c, D⟩))$
39	24 28 35 38	mpbir3and	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩$
40		simpl	$⊢ (d \in 𝔼 (N) \land b \in 𝔼 (N)) \to d \in 𝔼 (N)$
41		simpr	$⊢ (d \in 𝔼 (N) \land b \in 𝔼 (N)) \to b \in 𝔼 (N)$
42	40 41 41	3jca	$⊢ (d \in 𝔼 (N) \land b \in 𝔼 (N)) \to (d \in 𝔼 (N) \land b \in 𝔼 (N) \land b \in 𝔼 (N))$
43	42	3anim3i	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land b \in 𝔼 (N)))$
44	26	3anim1i	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to (((A \neq B \land B \neq C) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))$
45		btwnconn1lem1	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨B, c⟩ Cgr ⟨b, C⟩$
46	43 44 45	syl2an	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨B, c⟩ Cgr ⟨b, C⟩$
47	5 8 16	cgrrflx2d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to ⟨C, c⟩ Cgr ⟨c, C⟩$
48	47	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨C, c⟩ Cgr ⟨c, C⟩$
49	46 48	jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩)$
50	13 39 49	3jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to (C Btwn ⟨B, d⟩ \land ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \land (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩))$
51		simp1l2	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to B \neq C$
52	51	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to B \neq C$
53		brofs2	$⊢ ((N \in ℕ \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (d \in 𝔼 (N) \land c \in 𝔼 (N) \land b \in 𝔼 (N)) \land (c \in 𝔼 (N) \land D \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨⟨B, C⟩, ⟨d, c⟩⟩ OuterFiveSeg ⟨⟨b, c⟩, ⟨D, C⟩⟩ \leftrightarrow (C Btwn ⟨B, d⟩ \land ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \land (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩)))$
54	53	anbi1d	$⊢ ((N \in ℕ \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (d \in 𝔼 (N) \land c \in 𝔼 (N) \land b \in 𝔼 (N)) \land (c \in 𝔼 (N) \land D \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((⟨⟨B, C⟩, ⟨d, c⟩⟩ OuterFiveSeg ⟨⟨b, c⟩, ⟨D, C⟩⟩ \land B \neq C) \leftrightarrow ((C Btwn ⟨B, d⟩ \land ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \land (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩)) \land B \neq C))$
55		5segofs	$⊢ ((N \in ℕ \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (d \in 𝔼 (N) \land c \in 𝔼 (N) \land b \in 𝔼 (N)) \land (c \in 𝔼 (N) \land D \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((⟨⟨B, C⟩, ⟨d, c⟩⟩ OuterFiveSeg ⟨⟨b, c⟩, ⟨D, C⟩⟩ \land B \neq C) \to ⟨d, c⟩ Cgr ⟨D, C⟩)$
56	54 55	sylbird	$⊢ ((N \in ℕ \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (d \in 𝔼 (N) \land c \in 𝔼 (N) \land b \in 𝔼 (N)) \land (c \in 𝔼 (N) \land D \in 𝔼 (N) \land C \in 𝔼 (N))) \to (((C Btwn ⟨B, d⟩ \land ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \land (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩)) \land B \neq C) \to ⟨d, c⟩ Cgr ⟨D, C⟩)$
57	5 7 8 9 16 17 16 29 8 56	syl333anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \to (((C Btwn ⟨B, d⟩ \land ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \land (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩)) \land B \neq C) \to ⟨d, c⟩ Cgr ⟨D, C⟩)$
58	57	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to (((C Btwn ⟨B, d⟩ \land ⟨B, ⟨C, d⟩⟩ Cgr3 ⟨b, ⟨c, D⟩⟩ \land (⟨B, c⟩ Cgr ⟨b, C⟩ \land ⟨C, c⟩ Cgr ⟨c, C⟩)) \land B \neq C) \to ⟨d, c⟩ Cgr ⟨D, C⟩)$
59	50 52 58	mp2and	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N))) \land (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩)))) \to ⟨d, c⟩ Cgr ⟨D, C⟩$

Metamath Proof Explorer

Theorem btwnconn1lem4

Proof