ifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H G , with B between A and C and F between E and G . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Scott Fenton, 27-Sep-2013)

		Ref	Expression
	Assertion	ifscgr	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ InnerFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to ⟨B, D⟩ Cgr ⟨F, H⟩)$

Proof

Step	Hyp	Ref	Expression
1		brifs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ InnerFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
2		simp1l	$⊢ ((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to B Btwn ⟨C, C⟩$
3		simp11	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to N \in ℕ$
4		simp13	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to B \in 𝔼 (N)$
5		simp21	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to C \in 𝔼 (N)$
6		axbtwnid	$⊢ (N \in ℕ \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B Btwn ⟨C, C⟩ \to B = C)$
7	3 4 5 6	syl3anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (B Btwn ⟨C, C⟩ \to B = C)$
8	2 7	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to B = C)$
9		simp2r	$⊢ ((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, C⟩ Cgr ⟨F, G⟩$
10		simp3r	$⊢ ((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨C, D⟩ Cgr ⟨G, H⟩$
11	9 10	jca	$⊢ ((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (⟨B, C⟩ Cgr ⟨F, G⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)$
12		opeq2	$⊢ B = C \to ⟨B, B⟩ = ⟨B, C⟩$
13	12	breq1d	$⊢ B = C \to (⟨B, B⟩ Cgr ⟨F, G⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨F, G⟩)$
14		opeq1	$⊢ B = C \to ⟨B, D⟩ = ⟨C, D⟩$
15	14	breq1d	$⊢ B = C \to (⟨B, D⟩ Cgr ⟨G, H⟩ \leftrightarrow ⟨C, D⟩ Cgr ⟨G, H⟩)$
16	13 15	anbi12d	$⊢ B = C \to ((⟨B, B⟩ Cgr ⟨F, G⟩ \land ⟨B, D⟩ Cgr ⟨G, H⟩) \leftrightarrow (⟨B, C⟩ Cgr ⟨F, G⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))$
17	16	biimprd	$⊢ B = C \to ((⟨B, C⟩ Cgr ⟨F, G⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \to (⟨B, B⟩ Cgr ⟨F, G⟩ \land ⟨B, D⟩ Cgr ⟨G, H⟩))$
18	11 17	mpan9	$⊢ (((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land B = C) \to (⟨B, B⟩ Cgr ⟨F, G⟩ \land ⟨B, D⟩ Cgr ⟨G, H⟩)$
19		simp31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to F \in 𝔼 (N)$
20		simp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to G \in 𝔼 (N)$
21		cgrid2	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \to (⟨B, B⟩ Cgr ⟨F, G⟩ \to F = G)$
22	3 4 19 20 21	syl13anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨B, B⟩ Cgr ⟨F, G⟩ \to F = G)$
23		opeq1	$⊢ F = G \to ⟨F, H⟩ = ⟨G, H⟩$
24	23	breq2d	$⊢ F = G \to (⟨B, D⟩ Cgr ⟨F, H⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨G, H⟩)$
25	24	biimprd	$⊢ F = G \to (⟨B, D⟩ Cgr ⟨G, H⟩ \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
26	22 25	syl6	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨B, B⟩ Cgr ⟨F, G⟩ \to (⟨B, D⟩ Cgr ⟨G, H⟩ \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
27	26	impd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨B, B⟩ Cgr ⟨F, G⟩ \land ⟨B, D⟩ Cgr ⟨G, H⟩) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
28	18 27	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land B = C) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
29	28	expd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (B = C \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
30	8 29	mpdd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
31		opeq1	$⊢ A = C \to ⟨A, C⟩ = ⟨C, C⟩$
32	31	breq2d	$⊢ A = C \to (B Btwn ⟨A, C⟩ \leftrightarrow B Btwn ⟨C, C⟩)$
33	32	anbi1d	$⊢ A = C \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \leftrightarrow (B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩))$
34	31	breq1d	$⊢ A = C \to (⟨A, C⟩ Cgr ⟨E, G⟩ \leftrightarrow ⟨C, C⟩ Cgr ⟨E, G⟩)$
35	34	anbi1d	$⊢ A = C \to ((⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \leftrightarrow (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
36	33 35	3anbi12d	$⊢ A = C \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \leftrightarrow ((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
37	36	imbi1d	$⊢ A = C \to ((((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, D⟩ Cgr ⟨F, H⟩) \leftrightarrow (((B Btwn ⟨C, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨C, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
38	30 37	imbitrrid	$⊢ A = C \to (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
39		simp12	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to A \in 𝔼 (N)$
40		btwndiff	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land C \in 𝔼 (N)) \to \exists e \in 𝔼 (N) (C Btwn ⟨A, e⟩ \land C \neq e)$
41	3 39 5 40	syl3anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to \exists e \in 𝔼 (N) (C Btwn ⟨A, e⟩ \land C \neq e)$
42		simpl11	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to N \in ℕ$
43		simpl23	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to E \in 𝔼 (N)$
44		simpl32	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to G \in 𝔼 (N)$
45		simpl21	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to C \in 𝔼 (N)$
46		simpr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to e \in 𝔼 (N)$
47		axsegcon	$⊢ (N \in ℕ \land (E \in 𝔼 (N) \land G \in 𝔼 (N)) \land (C \in 𝔼 (N) \land e \in 𝔼 (N))) \to \exists f \in 𝔼 (N) (G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩)$
48	42 43 44 45 46 47	syl122anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to \exists f \in 𝔼 (N) (G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩)$
49		anass	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)) \leftrightarrow ((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land ((C Btwn ⟨A, e⟩ \land C \neq e) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)))$
50		anass	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land A \neq C) \leftrightarrow (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C))$
51		simplrl	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to C Btwn ⟨A, e⟩$
52	51	adantl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to C Btwn ⟨A, e⟩$
53		simplll	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to G Btwn ⟨E, f⟩$
54	53	adantl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to G Btwn ⟨E, f⟩$
55	52 54	jca	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to (C Btwn ⟨A, e⟩ \land G Btwn ⟨E, f⟩)$
56		simpr2l	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨A, C⟩ Cgr ⟨E, G⟩$
57	56	adantl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to ⟨A, C⟩ Cgr ⟨E, G⟩$
58		simpllr	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨G, f⟩ Cgr ⟨C, e⟩$
59	58	adantl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to ⟨G, f⟩ Cgr ⟨C, e⟩$
60	3	ad2antrr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to N \in ℕ$
61	20	ad2antrr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to G \in 𝔼 (N)$
62		simplrr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to f \in 𝔼 (N)$
63	5	ad2antrr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to C \in 𝔼 (N)$
64		simplrl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to e \in 𝔼 (N)$
65		cgrcom	$⊢ (N \in ℕ \land (G \in 𝔼 (N) \land f \in 𝔼 (N)) \land (C \in 𝔼 (N) \land e \in 𝔼 (N))) \to (⟨G, f⟩ Cgr ⟨C, e⟩ \leftrightarrow ⟨C, e⟩ Cgr ⟨G, f⟩)$
66	60 61 62 63 64 65	syl122anc	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to (⟨G, f⟩ Cgr ⟨C, e⟩ \leftrightarrow ⟨C, e⟩ Cgr ⟨G, f⟩)$
67	59 66	mpbid	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to ⟨C, e⟩ Cgr ⟨G, f⟩$
68	57 67	jca	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨C, e⟩ Cgr ⟨G, f⟩)$
69		simprr3	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)$
70	55 68 69	3jca	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))) \to ((C Btwn ⟨A, e⟩ \land G Btwn ⟨E, f⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨C, e⟩ Cgr ⟨G, f⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))$
71	70	ex	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ((C Btwn ⟨A, e⟩ \land G Btwn ⟨E, f⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨C, e⟩ Cgr ⟨G, f⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
72		simpl11	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to N \in ℕ$
73		simpl12	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to A \in 𝔼 (N)$
74		simpl21	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to C \in 𝔼 (N)$
75		simprl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to e \in 𝔼 (N)$
76		simpl22	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to D \in 𝔼 (N)$
77		simpl23	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to E \in 𝔼 (N)$
78		simpl32	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to G \in 𝔼 (N)$
79		simprr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to f \in 𝔼 (N)$
80		simpl33	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to H \in 𝔼 (N)$
81		brofs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (e \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (G \in 𝔼 (N) \land f \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, C⟩, ⟨e, D⟩⟩ OuterFiveSeg ⟨⟨E, G⟩, ⟨f, H⟩⟩ \leftrightarrow ((C Btwn ⟨A, e⟩ \land G Btwn ⟨E, f⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨C, e⟩ Cgr ⟨G, f⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
82	72 73 74 75 76 77 78 79 80 81	syl333anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (⟨⟨A, C⟩, ⟨e, D⟩⟩ OuterFiveSeg ⟨⟨E, G⟩, ⟨f, H⟩⟩ \leftrightarrow ((C Btwn ⟨A, e⟩ \land G Btwn ⟨E, f⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨C, e⟩ Cgr ⟨G, f⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
83	71 82	sylibrd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨⟨A, C⟩, ⟨e, D⟩⟩ OuterFiveSeg ⟨⟨E, G⟩, ⟨f, H⟩⟩)$
84		5segofs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (e \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (G \in 𝔼 (N) \land f \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨⟨A, C⟩, ⟨e, D⟩⟩ OuterFiveSeg ⟨⟨E, G⟩, ⟨f, H⟩⟩ \land A \neq C) \to ⟨e, D⟩ Cgr ⟨f, H⟩)$
85	72 73 74 75 76 77 78 79 80 84	syl333anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((⟨⟨A, C⟩, ⟨e, D⟩⟩ OuterFiveSeg ⟨⟨E, G⟩, ⟨f, H⟩⟩ \land A \neq C) \to ⟨e, D⟩ Cgr ⟨f, H⟩)$
86	83 85	syland	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land A \neq C) \to ⟨e, D⟩ Cgr ⟨f, H⟩)$
87		simpr1l	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to B Btwn ⟨A, C⟩$
88	87	adantr	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to B Btwn ⟨A, C⟩$
89	51	adantr	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to C Btwn ⟨A, e⟩$
90	88 89	jca	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to (B Btwn ⟨A, C⟩ \land C Btwn ⟨A, e⟩)$
91		simpr1r	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to F Btwn ⟨E, G⟩$
92	91	adantr	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to F Btwn ⟨E, G⟩$
93	53	adantr	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to G Btwn ⟨E, f⟩$
94	90 92 93	jca32	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, e⟩) \land (F Btwn ⟨E, G⟩ \land G Btwn ⟨E, f⟩))$
95		simpl13	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to B \in 𝔼 (N)$
96		btwnexch3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land e \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, e⟩) \to C Btwn ⟨B, e⟩)$
97	72 73 95 74 75 96	syl122anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, e⟩) \to C Btwn ⟨B, e⟩)$
98		simpl31	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to F \in 𝔼 (N)$
99		btwnexch3	$⊢ (N \in ℕ \land (E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((F Btwn ⟨E, G⟩ \land G Btwn ⟨E, f⟩) \to G Btwn ⟨F, f⟩)$
100	72 77 98 78 79 99	syl122anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((F Btwn ⟨E, G⟩ \land G Btwn ⟨E, f⟩) \to G Btwn ⟨F, f⟩)$
101	97 100	anim12d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, e⟩) \land (F Btwn ⟨E, G⟩ \land G Btwn ⟨E, f⟩)) \to (C Btwn ⟨B, e⟩ \land G Btwn ⟨F, f⟩))$
102	94 101	syl5	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to (C Btwn ⟨B, e⟩ \land G Btwn ⟨F, f⟩))$
103	102	imp	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to (C Btwn ⟨B, e⟩ \land G Btwn ⟨F, f⟩)$
104		btwncom	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land B \in 𝔼 (N) \land e \in 𝔼 (N))) \to (C Btwn ⟨B, e⟩ \leftrightarrow C Btwn ⟨e, B⟩)$
105	72 74 95 75 104	syl13anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (C Btwn ⟨B, e⟩ \leftrightarrow C Btwn ⟨e, B⟩)$
106		btwncom	$⊢ (N \in ℕ \land (G \in 𝔼 (N) \land F \in 𝔼 (N) \land f \in 𝔼 (N))) \to (G Btwn ⟨F, f⟩ \leftrightarrow G Btwn ⟨f, F⟩)$
107	72 78 98 79 106	syl13anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (G Btwn ⟨F, f⟩ \leftrightarrow G Btwn ⟨f, F⟩)$
108	105 107	anbi12d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((C Btwn ⟨B, e⟩ \land G Btwn ⟨F, f⟩) \leftrightarrow (C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩))$
109	108	adantr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ((C Btwn ⟨B, e⟩ \land G Btwn ⟨F, f⟩) \leftrightarrow (C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩))$
110	103 109	mpbid	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to (C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩)$
111	58	ad2antrl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ⟨G, f⟩ Cgr ⟨C, e⟩$
112	72 78 79 74 75 65	syl122anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (⟨G, f⟩ Cgr ⟨C, e⟩ \leftrightarrow ⟨C, e⟩ Cgr ⟨G, f⟩)$
113		cgrcomlr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land e \in 𝔼 (N)) \land (G \in 𝔼 (N) \land f \in 𝔼 (N))) \to (⟨C, e⟩ Cgr ⟨G, f⟩ \leftrightarrow ⟨e, C⟩ Cgr ⟨f, G⟩)$
114	72 74 75 78 79 113	syl122anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (⟨C, e⟩ Cgr ⟨G, f⟩ \leftrightarrow ⟨e, C⟩ Cgr ⟨f, G⟩)$
115	112 114	bitrd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (⟨G, f⟩ Cgr ⟨C, e⟩ \leftrightarrow ⟨e, C⟩ Cgr ⟨f, G⟩)$
116	115	adantr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to (⟨G, f⟩ Cgr ⟨C, e⟩ \leftrightarrow ⟨e, C⟩ Cgr ⟨f, G⟩)$
117	111 116	mpbid	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ⟨e, C⟩ Cgr ⟨f, G⟩$
118		simpr2r	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨B, C⟩ Cgr ⟨F, G⟩$
119	118	ad2antrl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ⟨B, C⟩ Cgr ⟨F, G⟩$
120	72 95 74 98 78 119	cgrcomlrand	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ⟨C, B⟩ Cgr ⟨G, F⟩$
121	117 120	jca	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to (⟨e, C⟩ Cgr ⟨f, G⟩ \land ⟨C, B⟩ Cgr ⟨G, F⟩)$
122		simprr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ⟨e, D⟩ Cgr ⟨f, H⟩$
123		simpr3r	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨C, D⟩ Cgr ⟨G, H⟩$
124	123	ad2antrl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ⟨C, D⟩ Cgr ⟨G, H⟩$
125	122 124	jca	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to (⟨e, D⟩ Cgr ⟨f, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)$
126	110 121 125	3jca	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \land ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩)) \to ((C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩) \land (⟨e, C⟩ Cgr ⟨f, G⟩ \land ⟨C, B⟩ Cgr ⟨G, F⟩) \land (⟨e, D⟩ Cgr ⟨f, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))$
127	126	ex	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to ((C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩) \land (⟨e, C⟩ Cgr ⟨f, G⟩ \land ⟨C, B⟩ Cgr ⟨G, F⟩) \land (⟨e, D⟩ Cgr ⟨f, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
128		brofs	$⊢ ((N \in ℕ \land e \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B \in 𝔼 (N) \land D \in 𝔼 (N) \land f \in 𝔼 (N)) \land (G \in 𝔼 (N) \land F \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨e, C⟩, ⟨B, D⟩⟩ OuterFiveSeg ⟨⟨f, G⟩, ⟨F, H⟩⟩ \leftrightarrow ((C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩) \land (⟨e, C⟩ Cgr ⟨f, G⟩ \land ⟨C, B⟩ Cgr ⟨G, F⟩) \land (⟨e, D⟩ Cgr ⟨f, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
129	72 75 74 95 76 79 78 98 80 128	syl333anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (⟨⟨e, C⟩, ⟨B, D⟩⟩ OuterFiveSeg ⟨⟨f, G⟩, ⟨F, H⟩⟩ \leftrightarrow ((C Btwn ⟨e, B⟩ \land G Btwn ⟨f, F⟩) \land (⟨e, C⟩ Cgr ⟨f, G⟩ \land ⟨C, B⟩ Cgr ⟨G, F⟩) \land (⟨e, D⟩ Cgr ⟨f, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
130	127 129	sylibrd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to ⟨⟨e, C⟩, ⟨B, D⟩⟩ OuterFiveSeg ⟨⟨f, G⟩, ⟨F, H⟩⟩)$
131		simplrr	$⊢ (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to C \neq e$
132	131	adantr	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to C \neq e$
133	132	necomd	$⊢ ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to e \neq C$
134	133	a1i	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to e \neq C)$
135	130 134	jcad	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to (⟨⟨e, C⟩, ⟨B, D⟩⟩ OuterFiveSeg ⟨⟨f, G⟩, ⟨F, H⟩⟩ \land e \neq C))$
136		5segofs	$⊢ ((N \in ℕ \land e \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B \in 𝔼 (N) \land D \in 𝔼 (N) \land f \in 𝔼 (N)) \land (G \in 𝔼 (N) \land F \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨⟨e, C⟩, ⟨B, D⟩⟩ OuterFiveSeg ⟨⟨f, G⟩, ⟨F, H⟩⟩ \land e \neq C) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
137	72 75 74 95 76 79 78 98 80 136	syl333anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((⟨⟨e, C⟩, ⟨B, D⟩⟩ OuterFiveSeg ⟨⟨f, G⟩, ⟨F, H⟩⟩ \land e \neq C) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
138	135 137	syld	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land ⟨e, D⟩ Cgr ⟨f, H⟩) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
139	138	expd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (⟨e, D⟩ Cgr ⟨f, H⟩ \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
140	139	adantrd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land A \neq C) \to (⟨e, D⟩ Cgr ⟨f, H⟩ \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
141	86 140	mpdd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \land A \neq C) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
142	50 141	biimtrrid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land (C Btwn ⟨A, e⟩ \land C \neq e)) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
143	49 142	biimtrrid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to (((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \land ((C Btwn ⟨A, e⟩ \land C \neq e) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C))) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
144	143	expd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (e \in 𝔼 (N) \land f \in 𝔼 (N))) \to ((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \to (((C Btwn ⟨A, e⟩ \land C \neq e) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
145	144	anassrs	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \land f \in 𝔼 (N)) \to ((G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \to (((C Btwn ⟨A, e⟩ \land C \neq e) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
146	145	rexlimdva	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to (\exists f \in 𝔼 (N) (G Btwn ⟨E, f⟩ \land ⟨G, f⟩ Cgr ⟨C, e⟩) \to (((C Btwn ⟨A, e⟩ \land C \neq e) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
147	48 146	mpd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to (((C Btwn ⟨A, e⟩ \land C \neq e) \land (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C)) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
148	147	expd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land e \in 𝔼 (N)) \to ((C Btwn ⟨A, e⟩ \land C \neq e) \to ((((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
149	148	rexlimdva	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (\exists e \in 𝔼 (N) (C Btwn ⟨A, e⟩ \land C \neq e) \to ((((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
150	41 149	mpd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land A \neq C) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
151	150	expd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (A \neq C \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
152	151	com3r	$⊢ A \neq C \to (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, D⟩ Cgr ⟨F, H⟩))$
153	38 152	pm2.61ine	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨B, D⟩ Cgr ⟨F, H⟩)$
154	1 153	sylbid	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ InnerFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to ⟨B, D⟩ Cgr ⟨F, H⟩)$

Metamath Proof Explorer

Theorem ifscgr

Proof