btwnconn1lem8

Description: Lemma for btwnconn1 . Now, we introduce the last three points used in the construction: P , Q , and R will turn out to be equal further down, and will provide us with the key to the final statement. We begin by establishing congruence of R P and E d . (Contributed by Scott Fenton, 8-Oct-2013)

		Ref	Expression
	Assertion	btwnconn1lem8	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨R, P⟩ Cgr ⟨E, d⟩$

Proof

Step	Hyp	Ref	Expression
1		simpr2l	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to C Btwn ⟨d, R⟩$
2	1	ad2antll	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to C Btwn ⟨d, R⟩$
3		simpr1r	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to ⟨C, P⟩ Cgr ⟨C, d⟩$
4	3	ad2antll	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨C, P⟩ Cgr ⟨C, 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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to N \in ℕ$
6		simp2l1	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to C \in 𝔼 (N)$
7		simp31	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to P \in 𝔼 (N)$
8		simp2r1	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to d \in 𝔼 (N)$
9		cgrcomlr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨P, C⟩ Cgr ⟨d, C⟩)$
10	5 6 7 6 8 9	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨P, C⟩ Cgr ⟨d, C⟩)$
11		cgrcom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land C \in 𝔼 (N)) \land (d \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨P, C⟩ Cgr ⟨d, C⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
12	5 7 6 8 6 11	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨P, C⟩ Cgr ⟨d, C⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
13	10 12	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
14	13	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
15	4 14	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, C⟩ Cgr ⟨P, C⟩$
16		simp33	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to R \in 𝔼 (N)$
17		simp2r3	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to E \in 𝔼 (N)$
18		simp2l3	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to c \in 𝔼 (N)$
19		simpr1l	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to C Btwn ⟨c, P⟩$
20	19	ad2antll	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to C Btwn ⟨c, P⟩$
21	5 6 18 7 20	btwncomand	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to C Btwn ⟨P, c⟩$
22		simprll	$⊢ ((((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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to E Btwn ⟨C, c⟩$
23	22	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to E Btwn ⟨C, c⟩$
24		btwnintr	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land c \in 𝔼 (N))) \to ((C Btwn ⟨P, c⟩ \land E Btwn ⟨C, c⟩) \to C Btwn ⟨P, E⟩)$
25	5 7 6 17 18 24	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to ((C Btwn ⟨P, c⟩ \land E Btwn ⟨C, c⟩) \to C Btwn ⟨P, E⟩)$
26	25	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ((C Btwn ⟨P, c⟩ \land E Btwn ⟨C, c⟩) \to C Btwn ⟨P, E⟩)$
27	21 23 26	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to C Btwn ⟨P, E⟩$
28		simpr2r	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to ⟨C, R⟩ Cgr ⟨C, E⟩$
29	28	ad2antll	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨C, R⟩ Cgr ⟨C, E⟩$
30	5 8 6 16 7 6 17 2 27 15 29	cgrextendand	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, R⟩ Cgr ⟨P, E⟩$
31		brcgr3	$⊢ (N \in ℕ \land (d \in 𝔼 (N) \land C \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \in 𝔼 (N) \land C \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \leftrightarrow (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨d, R⟩ Cgr ⟨P, E⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩))$
32	5 8 6 16 7 6 17 31	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \leftrightarrow (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨d, R⟩ Cgr ⟨P, E⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩))$
33	32	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \leftrightarrow (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨d, R⟩ Cgr ⟨P, E⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩))$
34	15 30 29 33	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩$
35	5 8 7	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to ⟨d, P⟩ Cgr ⟨P, d⟩$
36	35	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, P⟩ Cgr ⟨P, d⟩$
37	36 4	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩)$
38	2 34 37	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (C Btwn ⟨d, R⟩ \land ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \land (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩))$
39		simp1	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N))$
40		simp2l	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N))$
41		simp2r	$⊢ ((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))$
42	39 40 41	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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 E \in 𝔼 (N)))$
43		simpl	$⊢ ((((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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to (((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⟩)))$
44		simprl	$⊢ ((((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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to (E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩)$
45	43 44	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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to ((((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⟩))) \land (E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩))$
46		btwnconn1lem7	$⊢ (((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 E \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⟩))) \land (E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩))) \to C \neq d$
47	42 45 46	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to C \neq d$
48	47	necomd	$⊢ (((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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to d \neq C$
49		brofs2	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land C \in 𝔼 (N)) \land (R \in 𝔼 (N) \land P \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land E \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨⟨d, C⟩, ⟨R, P⟩⟩ OuterFiveSeg ⟨⟨P, C⟩, ⟨E, d⟩⟩ \leftrightarrow (C Btwn ⟨d, R⟩ \land ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \land (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩)))$
50	49	anbi1d	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land C \in 𝔼 (N)) \land (R \in 𝔼 (N) \land P \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land E \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((⟨⟨d, C⟩, ⟨R, P⟩⟩ OuterFiveSeg ⟨⟨P, C⟩, ⟨E, d⟩⟩ \land d \neq C) \leftrightarrow ((C Btwn ⟨d, R⟩ \land ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \land (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩)) \land d \neq C))$
51		5segofs	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land C \in 𝔼 (N)) \land (R \in 𝔼 (N) \land P \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land E \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((⟨⟨d, C⟩, ⟨R, P⟩⟩ OuterFiveSeg ⟨⟨P, C⟩, ⟨E, d⟩⟩ \land d \neq C) \to ⟨R, P⟩ Cgr ⟨E, d⟩)$
52	50 51	sylbird	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land C \in 𝔼 (N)) \land (R \in 𝔼 (N) \land P \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land E \in 𝔼 (N) \land d \in 𝔼 (N))) \to (((C Btwn ⟨d, R⟩ \land ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \land (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩)) \land d \neq C) \to ⟨R, P⟩ Cgr ⟨E, d⟩)$
53	5 8 6 16 7 7 6 17 8 52	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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((C Btwn ⟨d, R⟩ \land ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \land (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩)) \land d \neq C) \to ⟨R, P⟩ Cgr ⟨E, d⟩)$
54	53	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (((C Btwn ⟨d, R⟩ \land ⟨d, ⟨C, R⟩⟩ Cgr3 ⟨P, ⟨C, E⟩⟩ \land (⟨d, P⟩ Cgr ⟨P, d⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩)) \land d \neq C) \to ⟨R, P⟩ Cgr ⟨E, d⟩)$
55	38 48 54	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \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⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨R, P⟩ Cgr ⟨E, d⟩$

Metamath Proof Explorer

Theorem btwnconn1lem8

Proof