btwnconn1lem7

Description: Lemma for btwnconn1 . Under our assumptions, C and d are distinct. (Contributed by Scott Fenton, 8-Oct-2013)

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		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$
2	1	adantr	$⊢ ((((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 c$
3		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⟩$
4	3	adantr	$⊢ ((((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, d⟩ Cgr ⟨C, D⟩$
5		simp2lr	$⊢ (((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \to ⟨D, c⟩ Cgr ⟨C, D⟩$
6	5	adantr	$⊢ ((((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 ⟨D, c⟩ Cgr ⟨C, D⟩$
7	2 4 6	3jca	$⊢ ((((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 c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)$
8		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))) \to N \in ℕ$
9		simp21	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \to C \in 𝔼 (N)$
10		simp22	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \to D \in 𝔼 (N)$
11		simp23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \to c \in 𝔼 (N)$
12		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))) \to d \in 𝔼 (N)$
13		simpr1	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to C \neq c$
14		opeq2	$⊢ C = d \to ⟨C, C⟩ = ⟨C, d⟩$
15	14	breq1d	$⊢ C = d \to (⟨C, C⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨C, d⟩ Cgr ⟨C, D⟩)$
16	15	3anbi2d	$⊢ C = d \to ((C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \leftrightarrow (C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩))$
17	16	biimparc	$⊢ ((C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land C = d) \to (C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)$
18		simp2	$⊢ (C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \to ⟨C, C⟩ Cgr ⟨C, D⟩$
19		simp1	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to N \in ℕ$
20		simp2l	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to C \in 𝔼 (N)$
21		simp2r	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to D \in 𝔼 (N)$
22		cgrid2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D)$
23	19 20 20 21 22	syl13anc	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D)$
24	18 23	syl5	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \to C = D)$
25	24	imp	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to C = D$
26		opeq1	$⊢ C = D \to ⟨C, c⟩ = ⟨D, c⟩$
27		opeq2	$⊢ C = D \to ⟨C, C⟩ = ⟨C, D⟩$
28	26 27	breq12d	$⊢ C = D \to (⟨C, c⟩ Cgr ⟨C, C⟩ \leftrightarrow ⟨D, c⟩ Cgr ⟨C, D⟩)$
29	28	biimparc	$⊢ (⟨D, c⟩ Cgr ⟨C, D⟩ \land C = D) \to ⟨C, c⟩ Cgr ⟨C, C⟩$
30		simp3l	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to c \in 𝔼 (N)$
31		axcgrid	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land c \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨C, c⟩ Cgr ⟨C, C⟩ \to C = c)$
32	19 20 30 20 31	syl13anc	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨C, c⟩ Cgr ⟨C, C⟩ \to C = c)$
33	29 32	syl5	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((⟨D, c⟩ Cgr ⟨C, D⟩ \land C = D) \to C = c)$
34	33	expdimp	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land ⟨D, c⟩ Cgr ⟨C, D⟩) \to (C = D \to C = c)$
35	34	3ad2antr3	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to (C = D \to C = c)$
36	25 35	mpd	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to C = c$
37	36	ex	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((C \neq c \land ⟨C, C⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \to C = c)$
38	17 37	syl5	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to (((C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land C = d) \to C = c)$
39	38	expdimp	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to (C = d \to C = c)$
40	39	necon3d	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to (C \neq c \to C \neq d)$
41	13 40	mpd	$⊢ ((N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \land (C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩)) \to C \neq d$
42	41	ex	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (c \in 𝔼 (N) \land d \in 𝔼 (N))) \to ((C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \to C \neq d)$
43	8 9 10 11 12 42	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))) \to ((C \neq c \land ⟨C, d⟩ Cgr ⟨C, D⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \to C \neq d)$
44	7 43	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))) \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⟩)) \to C \neq d)$
45	44	imp	$⊢ (((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$

Metamath Proof Explorer

Theorem btwnconn1lem7

Proof