btwnconn1lem9

Description: Lemma for btwnconn1 . Now, a quick use of transitivity to establish congruence on R Q and E D . (Contributed by Scott Fenton, 8-Oct-2013)

		Ref	Expression
	Assertion	btwnconn1lem9	$⊢ (((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 ⟨E, 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		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)$
3		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)$
4		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)$
5		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)$
6		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)$
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		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⟩$
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 ⟨R, Q⟩ Cgr ⟨R, P⟩$
10		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⟩$
11	1 2 3 2 7 4 6 9 10	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 ⟨R, Q⟩ Cgr ⟨E, d⟩$
12		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))$
13		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))$
14		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))$
15	12 13 14	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)))$
16		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⟩)))$
17		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⟩)$
18	16 17	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⟩))$
19		btwnconn1lem6	$⊢ (((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, D⟩ Cgr ⟨E, d⟩$
20	15 18 19	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, D⟩ Cgr ⟨E, d⟩$
21	1 2 3 4 5 4 6 11 20	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 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 ⟨E, D⟩$

Metamath Proof Explorer

Theorem btwnconn1lem9

Proof