fscgr

Description: Congruence law for the general five segment configuration. Theorem 4.16 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

		Ref	Expression
	Assertion	fscgr	$⊢ ((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⟩⟩ FiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$

Proof

Step	Hyp	Ref	Expression
1		brfs	$⊢ ((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⟩⟩ FiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
2	1	anbi1d	$⊢ ((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⟩⟩ FiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \leftrightarrow ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \land A \neq B))$
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		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)$
5		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)$
6		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)$
7		brcolinear	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (A Colinear ⟨B, C⟩ \leftrightarrow (A Btwn ⟨B, C⟩ \lor B Btwn ⟨C, A⟩ \lor C Btwn ⟨A, B⟩))$
8	3 4 5 6 7	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 (A Colinear ⟨B, C⟩ \leftrightarrow (A Btwn ⟨B, C⟩ \lor B Btwn ⟨C, A⟩ \lor C Btwn ⟨A, B⟩))$
9		simp23	$⊢ ((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 E \in 𝔼 (N)$
10		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)$
11		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)$
12		cgr3permute2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \leftrightarrow ⟨B, ⟨A, C⟩⟩ Cgr3 ⟨F, ⟨E, G⟩⟩)$
13	3 4 5 6 9 10 11 12	syl133anc	$⊢ ((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⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \leftrightarrow ⟨B, ⟨A, C⟩⟩ Cgr3 ⟨F, ⟨E, G⟩⟩)$
14		ancom	$⊢ (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \leftrightarrow (⟨B, D⟩ Cgr ⟨F, H⟩ \land ⟨A, D⟩ Cgr ⟨E, H⟩)$
15	14	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))) \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \leftrightarrow (⟨B, D⟩ Cgr ⟨F, H⟩ \land ⟨A, D⟩ Cgr ⟨E, H⟩))$
16	13 15	3anbi23d	$⊢ ((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 Btwn ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow (A Btwn ⟨B, C⟩ \land ⟨B, ⟨A, C⟩⟩ Cgr3 ⟨F, ⟨E, G⟩⟩ \land (⟨B, D⟩ Cgr ⟨F, H⟩ \land ⟨A, D⟩ Cgr ⟨E, H⟩)))$
17		simp22	$⊢ ((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 D \in 𝔼 (N)$
18		simp33	$⊢ ((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 H \in 𝔼 (N)$
19		brofs2	$⊢ ((N \in ℕ \land B \in 𝔼 (N) \land A \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land F \in 𝔼 (N)) \land (E \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨B, A⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨F, E⟩, ⟨G, H⟩⟩ \leftrightarrow (A Btwn ⟨B, C⟩ \land ⟨B, ⟨A, C⟩⟩ Cgr3 ⟨F, ⟨E, G⟩⟩ \land (⟨B, D⟩ Cgr ⟨F, H⟩ \land ⟨A, D⟩ Cgr ⟨E, H⟩)))$
20	3 5 4 6 17 10 9 11 18 19	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))) \to (⟨⟨B, A⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨F, E⟩, ⟨G, H⟩⟩ \leftrightarrow (A Btwn ⟨B, C⟩ \land ⟨B, ⟨A, C⟩⟩ Cgr3 ⟨F, ⟨E, G⟩⟩ \land (⟨B, D⟩ Cgr ⟨F, H⟩ \land ⟨A, D⟩ Cgr ⟨E, H⟩)))$
21	16 20	bitr4d	$⊢ ((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 Btwn ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow ⟨⟨B, A⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨F, E⟩, ⟨G, H⟩⟩)$
22		necom	$⊢ A \neq B \leftrightarrow B \neq A$
23	22	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))) \to (A \neq B \leftrightarrow B \neq A)$
24	21 23	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))) \to (((A Btwn ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \land A \neq B) \leftrightarrow (⟨⟨B, A⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨F, E⟩, ⟨G, H⟩⟩ \land B \neq A))$
25		5segofs	$⊢ ((N \in ℕ \land B \in 𝔼 (N) \land A \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land F \in 𝔼 (N)) \land (E \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨⟨B, A⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨F, E⟩, ⟨G, H⟩⟩ \land B \neq A) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
26	3 5 4 6 17 10 9 11 18 25	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))) \to ((⟨⟨B, A⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨F, E⟩, ⟨G, H⟩⟩ \land B \neq A) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
27	24 26	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 Btwn ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
28	27	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 ((A Btwn ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))$
29	28	3expd	$⊢ ((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 Btwn ⟨B, C⟩ \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))))$
30		btwncom	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land A \in 𝔼 (N))) \to (B Btwn ⟨C, A⟩ \leftrightarrow B Btwn ⟨A, C⟩)$
31	3 5 6 4 30	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 Btwn ⟨C, A⟩ \leftrightarrow B Btwn ⟨A, C⟩)$
32	31	3anbi1d	$⊢ ((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, A⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
33		brofs2	$⊢ ((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⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
34	32 33	bitr4d	$⊢ ((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, A⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩)$
35	34	anbi1d	$⊢ ((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, A⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \land A \neq B) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B))$
36		5segofs	$⊢ ((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⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
37	35 36	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 (((B Btwn ⟨C, A⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
38	37	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, A⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))$
39	38	3expd	$⊢ ((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, A⟩ \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))))$
40		cgr3permute1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \leftrightarrow ⟨A, ⟨C, B⟩⟩ Cgr3 ⟨E, ⟨G, F⟩⟩)$
41	3 4 5 6 9 10 11 40	syl133anc	$⊢ ((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⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \leftrightarrow ⟨A, ⟨C, B⟩⟩ Cgr3 ⟨E, ⟨G, F⟩⟩)$
42	41	3anbi2d	$⊢ ((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 Btwn ⟨A, B⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow (C Btwn ⟨A, B⟩ \land ⟨A, ⟨C, B⟩⟩ Cgr3 ⟨E, ⟨G, F⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
43		brifs2	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B \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⟩, ⟨B, D⟩⟩ InnerFiveSeg ⟨⟨E, G⟩, ⟨F, H⟩⟩ \leftrightarrow (C Btwn ⟨A, B⟩ \land ⟨A, ⟨C, B⟩⟩ Cgr3 ⟨E, ⟨G, F⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
44	3 4 6 5 17 9 11 10 18 43	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))) \to (⟨⟨A, C⟩, ⟨B, D⟩⟩ InnerFiveSeg ⟨⟨E, G⟩, ⟨F, H⟩⟩ \leftrightarrow (C Btwn ⟨A, B⟩ \land ⟨A, ⟨C, B⟩⟩ Cgr3 ⟨E, ⟨G, F⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
45	42 44	bitr4d	$⊢ ((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 Btwn ⟨A, B⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow ⟨⟨A, C⟩, ⟨B, D⟩⟩ InnerFiveSeg ⟨⟨E, G⟩, ⟨F, H⟩⟩)$
46		ifscgr	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B \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⟩, ⟨B, D⟩⟩ InnerFiveSeg ⟨⟨E, G⟩, ⟨F, H⟩⟩ \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
47	3 4 6 5 17 9 11 10 18 46	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))) \to (⟨⟨A, C⟩, ⟨B, D⟩⟩ InnerFiveSeg ⟨⟨E, G⟩, ⟨F, H⟩⟩ \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
48	45 47	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 ((C Btwn ⟨A, B⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
49	48	a1dd	$⊢ ((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 Btwn ⟨A, B⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))$
50	49	3expd	$⊢ ((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 Btwn ⟨A, B⟩ \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))))$
51	29 39 50	3jaod	$⊢ ((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 Btwn ⟨B, C⟩ \lor B Btwn ⟨C, A⟩ \lor C Btwn ⟨A, B⟩) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))))$
52	8 51	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 Colinear ⟨B, C⟩ \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))))$
53	52	3impd	$⊢ ((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 Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to (A \neq B \to ⟨C, D⟩ Cgr ⟨G, H⟩))$
54	53	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 (((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$
55	2 54	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⟩⟩ FiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$

Metamath Proof Explorer

Theorem fscgr

Proof