btwnconn1lem12

Description: Lemma for btwnconn1 . Using a long string of invocations of linecgr , we show that D = d . (Contributed by Scott Fenton, 9-Oct-2013)

		Ref	Expression
	Assertion	btwnconn1lem12	$⊢ (((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 = d$

Proof

Step	Hyp	Ref	Expression
1		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 ℕ$
2		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)$
3		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)$
4		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)$
5		simp32	$⊢ ((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 Q \in 𝔼 (N)$
6		simp1l3	$⊢ (((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 \neq c$
7	6	ad2antrl	$⊢ (((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 c$
8		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⟩$
9	8	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⟩$
10		btwncolinear5	$⊢ (N \in ℕ \land (c \in 𝔼 (N) \land P \in 𝔼 (N) \land C \in 𝔼 (N))) \to (C Btwn ⟨c, P⟩ \to C Colinear ⟨c, P⟩)$
11	1 3 4 2 10	syl13anc	$⊢ ((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 ⟨c, P⟩ \to C Colinear ⟨c, P⟩)$
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 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⟩ \to C Colinear ⟨c, P⟩)$
13	9 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 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 Colinear ⟨c, P⟩$
14		simp2l2	$⊢ ((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)$
15		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)$
16		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⟩$
17	16	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⟩$
18		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⟩$
19	18	ad2antrl	$⊢ (((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, d⟩ Cgr ⟨C, D⟩$
20	1 2 4 2 15 2 14 17 19	cgrtrand	$⊢ (((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⟩$
21		btwnconn1lem11	$⊢ (((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 ⟨Q, C⟩$
22	1 14 2 5 2 21	cgrcomlrand	$⊢ (((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, D⟩ Cgr ⟨C, Q⟩$
23	1 2 4 2 14 2 5 20 22	cgrtrand	$⊢ (((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, Q⟩$
24		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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to A \in 𝔼 (N)$
25		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) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to B \in 𝔼 (N)$
26		simp2r2	$⊢ ((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 b \in 𝔼 (N)$
27		simp1rr	$⊢ (((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, D⟩$
28	27	ad2antrl	$⊢ (((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 B Btwn ⟨A, D⟩$
29		simp2ll	$⊢ (((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 Btwn ⟨A, c⟩$
30	29	ad2antrl	$⊢ (((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 Btwn ⟨A, c⟩$
31	1 24 25 14 3 28 30	btwnexchand	$⊢ (((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 B Btwn ⟨A, c⟩$
32		simp3ll	$⊢ (((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, b⟩$
33	32	ad2antrl	$⊢ (((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 ⟨A, b⟩$
34	1 24 25 3 26 31 33	btwnexch3and	$⊢ (((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 ⟨B, b⟩$
35		opeq1	$⊢ B = b \to ⟨B, b⟩ = ⟨b, b⟩$
36	35	breq2d	$⊢ B = b \to (c Btwn ⟨B, b⟩ \leftrightarrow c Btwn ⟨b, b⟩)$
37	36	biimpac	$⊢ (c Btwn ⟨B, b⟩ \land B = b) \to c Btwn ⟨b, b⟩$
38		axbtwnid	$⊢ (N \in ℕ \land c \in 𝔼 (N) \land b \in 𝔼 (N)) \to (c Btwn ⟨b, b⟩ \to c = b)$
39	1 3 26 38	syl3anc	$⊢ ((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 ⟨b, b⟩ \to c = b)$
40	37 39	syl5	$⊢ ((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 ⟨B, b⟩ \land B = b) \to c = b)$
41	40	expd	$⊢ ((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 ⟨B, b⟩ \to (B = b \to c = b))$
42	41	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 ⟨B, b⟩ \to (B = b \to c = b))$
43	34 42	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 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 (B = b \to c = b)$
44		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))$
45		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))$
46		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))$
47	44 45 46	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)))$
48		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⟩)))$
49		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⟩)$
50	48 49	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⟩))$
51		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$
52	47 50 51	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$
53		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⟩$
54	53	ad2antrl	$⊢ (((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 ⟨A, d⟩$
55		simp3rl	$⊢ (((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 Btwn ⟨A, b⟩$
56	55	ad2antrl	$⊢ (((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 Btwn ⟨A, b⟩$
57	1 24 2 15 26 54 56	btwnexch3and	$⊢ (((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 Btwn ⟨C, b⟩$
58		btwncolinear2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land b \in 𝔼 (N) \land d \in 𝔼 (N))) \to (d Btwn ⟨C, b⟩ \to C Colinear ⟨d, b⟩)$
59	1 2 26 15 58	syl13anc	$⊢ ((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 Btwn ⟨C, b⟩ \to C Colinear ⟨d, b⟩)$
60	59	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 Btwn ⟨C, b⟩ \to C Colinear ⟨d, b⟩)$
61	57 60	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 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 Colinear ⟨d, b⟩$
62		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)$
63		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⟩$
64	63	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⟩$
65		btwnconn1lem5	$⊢ (((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 ⟨E, C⟩ Cgr ⟨E, c⟩$
66	47 50 65	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 ⟨E, C⟩ Cgr ⟨E, c⟩$
67		opeq2	$⊢ R = C \to ⟨C, R⟩ = ⟨C, C⟩$
68	67	breq1d	$⊢ R = C \to (⟨C, R⟩ Cgr ⟨C, E⟩ \leftrightarrow ⟨C, C⟩ Cgr ⟨C, E⟩)$
69	68	anbi1d	$⊢ R = C \to ((⟨C, R⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩) \leftrightarrow (⟨C, C⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩))$
70	69	biimpac	$⊢ ((⟨C, R⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩) \land R = C) \to (⟨C, C⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩)$
71		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)$
72		cgrid2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land C \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨C, C⟩ Cgr ⟨C, E⟩ \to C = E)$
73	1 2 2 71 72	syl13anc	$⊢ ((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, C⟩ Cgr ⟨C, E⟩ \to C = E)$
74		opeq1	$⊢ C = E \to ⟨C, C⟩ = ⟨E, C⟩$
75		opeq1	$⊢ C = E \to ⟨C, c⟩ = ⟨E, c⟩$
76	74 75	breq12d	$⊢ C = E \to (⟨C, C⟩ Cgr ⟨C, c⟩ \leftrightarrow ⟨E, C⟩ Cgr ⟨E, c⟩)$
77	76	biimpar	$⊢ (C = E \land ⟨E, C⟩ Cgr ⟨E, c⟩) \to ⟨C, C⟩ Cgr ⟨C, c⟩$
78		cgrid2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land C \in 𝔼 (N) \land c \in 𝔼 (N))) \to (⟨C, C⟩ Cgr ⟨C, c⟩ \to C = c)$
79	1 2 2 3 78	syl13anc	$⊢ ((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, C⟩ Cgr ⟨C, c⟩ \to C = c)$
80	77 79	syl5	$⊢ ((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 = E \land ⟨E, C⟩ Cgr ⟨E, c⟩) \to C = c)$
81	73 80	syland	$⊢ ((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, C⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩) \to C = c)$
82	70 81	syl5	$⊢ ((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, R⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩) \land R = C) \to C = c)$
83	82	expd	$⊢ ((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, R⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩) \to (R = C \to C = c))$
84	83	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, R⟩ Cgr ⟨C, E⟩ \land ⟨E, C⟩ Cgr ⟨E, c⟩) \to (R = C \to C = c))$
85	64 66 84	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 = C \to C = c)$
86	85	necon3d	$⊢ (((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 c \to R \neq C)$
87	7 86	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 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 \neq C$
88		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⟩$
89	88	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⟩$
90		btwncolinear4	$⊢ (N \in ℕ \land (d \in 𝔼 (N) \land R \in 𝔼 (N) \land C \in 𝔼 (N))) \to (C Btwn ⟨d, R⟩ \to R Colinear ⟨C, d⟩)$
91	1 15 62 2 90	syl13anc	$⊢ ((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⟩ \to R Colinear ⟨C, d⟩)$
92	91	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⟩ \to R Colinear ⟨C, d⟩)$
93	89 92	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 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 Colinear ⟨C, d⟩$
94		simpr3r	$⊢ ((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, Q⟩ Cgr ⟨R, P⟩$
95	94	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 ⟨R, Q⟩ Cgr ⟨R, P⟩$
96	1 62 5 62 4 95	cgrcomand	$⊢ (((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 ⟨R, Q⟩$
97	1 62 2 15 4 5 87 93 96 23	linecgrand	$⊢ (((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 ⟨d, Q⟩$
98	1 2 15 26 4 5 52 61 23 97	linecgrand	$⊢ (((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 ⟨b, P⟩ Cgr ⟨b, Q⟩$
99		opeq1	$⊢ c = b \to ⟨c, P⟩ = ⟨b, P⟩$
100		opeq1	$⊢ c = b \to ⟨c, Q⟩ = ⟨b, Q⟩$
101	99 100	breq12d	$⊢ c = b \to (⟨c, P⟩ Cgr ⟨c, Q⟩ \leftrightarrow ⟨b, P⟩ Cgr ⟨b, Q⟩)$
102	101	biimprd	$⊢ c = b \to (⟨b, P⟩ Cgr ⟨b, Q⟩ \to ⟨c, P⟩ Cgr ⟨c, Q⟩)$
103	43 98 102	syl6ci	$⊢ (((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 (B = b \to ⟨c, P⟩ Cgr ⟨c, Q⟩)$
104	103	com12	$⊢ B = b \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))) \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, Q⟩)$
105		simprl	$⊢ (((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 (B \neq b \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 B \neq b$
106	34	adantrl	$⊢ (((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 (B \neq b \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 ⟨B, b⟩$
107		btwncolinear1	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land b \in 𝔼 (N) \land c \in 𝔼 (N))) \to (c Btwn ⟨B, b⟩ \to B Colinear ⟨b, c⟩)$
108	1 25 26 3 107	syl13anc	$⊢ ((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 ⟨B, b⟩ \to B Colinear ⟨b, c⟩)$
109	108	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 (B \neq b \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 ⟨B, b⟩ \to B Colinear ⟨b, c⟩)$
110	106 109	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 E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land (B \neq b \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 B Colinear ⟨b, c⟩$
111		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⟩$
112	111	ad2antrl	$⊢ (((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 B Btwn ⟨A, C⟩$
113	1 24 25 2 15 112 54	btwnexch3and	$⊢ (((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 ⟨B, d⟩$
114		btwncolinear6	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land d \in 𝔼 (N) \land C \in 𝔼 (N))) \to (C Btwn ⟨B, d⟩ \to C Colinear ⟨d, B⟩)$
115	1 25 15 2 114	syl13anc	$⊢ ((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 ⟨B, d⟩ \to C Colinear ⟨d, B⟩)$
116	115	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 ⟨B, d⟩ \to C Colinear ⟨d, B⟩)$
117	113 116	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 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 Colinear ⟨d, B⟩$
118	1 2 15 25 4 5 52 117 23 97	linecgrand	$⊢ (((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 ⟨B, P⟩ Cgr ⟨B, Q⟩$
119	118	adantrl	$⊢ (((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 (B \neq b \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 ⟨B, P⟩ Cgr ⟨B, Q⟩$
120	98	adantrl	$⊢ (((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 (B \neq b \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 ⟨b, P⟩ Cgr ⟨b, Q⟩$
121	1 25 26 3 4 5 105 110 119 120	linecgrand	$⊢ (((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 (B \neq b \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, Q⟩$
122	121	an12s	$⊢ (B \neq b \land (((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, Q⟩$
123	122	ex	$⊢ B \neq b \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))) \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, Q⟩)$
124	104 123	pm2.61ine	$⊢ (((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, Q⟩$
125	1 2 3 4 4 5 7 13 23 124	linecgrand	$⊢ (((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 ⟨P, P⟩ Cgr ⟨P, Q⟩$
126		cgrid2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (⟨P, P⟩ Cgr ⟨P, Q⟩ \to P = Q)$
127	1 4 4 5 126	syl13anc	$⊢ ((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, P⟩ Cgr ⟨P, Q⟩ \to P = Q)$
128	127	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 (⟨P, P⟩ Cgr ⟨P, Q⟩ \to P = Q)$
129	125 128	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 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 P = Q$
130		btwnconn1lem10	$⊢ (((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, D⟩ Cgr ⟨P, Q⟩$
131		opeq1	$⊢ P = Q \to ⟨P, Q⟩ = ⟨Q, Q⟩$
132	131	breq2d	$⊢ P = Q \to (⟨d, D⟩ Cgr ⟨P, Q⟩ \leftrightarrow ⟨d, D⟩ Cgr ⟨Q, Q⟩)$
133	132	biimpa	$⊢ (P = Q \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to ⟨d, D⟩ Cgr ⟨Q, Q⟩$
134		axcgrid	$⊢ (N \in ℕ \land (d \in 𝔼 (N) \land D \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (⟨d, D⟩ Cgr ⟨Q, Q⟩ \to d = D)$
135	1 15 14 5 134	syl13anc	$⊢ ((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, D⟩ Cgr ⟨Q, Q⟩ \to d = D)$
136	133 135	syl5	$⊢ ((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 = Q \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to d = D)$
137	136	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 ((P = Q \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to d = D)$
138	129 130 137	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 d = D$
139	138	eqcomd	$⊢ (((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 = d$

Metamath Proof Explorer

Theorem btwnconn1lem12

Proof