ifscgr - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ifscgr		Structured version Visualization version GIF version

Theorem ifscgr 36187

Description: Inner five segment congruence. Take two triangles, 𝐴𝐷𝐶 and 𝐸𝐻𝐺, with 𝐵 between 𝐴 and 𝐶 and 𝐹 between 𝐸 and 𝐺. If the other components of the triangles are congruent, then so are 𝐵𝐷 and 𝐹𝐻. Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 27-Sep-2013.)

**Assertion**
Ref	Expression
ifscgr	⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))

Proof of Theorem ifscgr Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brifs 36186	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
2		simp1l 1198	. . . . . 6 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → 𝐵 Btwn ⟨𝐶, 𝐶⟩)
3		simp11 1204	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
4		simp13 1206	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
5		simp21 1207	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
6		axbtwnid 28961	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐶⟩ → 𝐵 = 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐶, 𝐶⟩ → 𝐵 = 𝐶))
8	2, 7	syl5 34	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → 𝐵 = 𝐶))
9		simp2r 1201	. . . . . . . . 9 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
10		simp3r 1203	. . . . . . . . 9 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
11	9, 10	jca 511	. . . . . . . 8 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
12		opeq2 4828	. . . . . . . . . . 11 ⊢ (𝐵 = 𝐶 → ⟨𝐵, 𝐵⟩ = ⟨𝐵, 𝐶⟩)
13	12	breq1d 5106	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
14		opeq1 4827	. . . . . . . . . . 11 ⊢ (𝐵 = 𝐶 → ⟨𝐵, 𝐷⟩ = ⟨𝐶, 𝐷⟩)
15	14	breq1d 5106	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
16	13, 15	anbi12d 632	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) ↔ (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
17	16	biimprd 248	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → ((⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
18	11, 17	mpan9 506	. . . . . . 7 ⊢ ((((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐵 = 𝐶) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
19		simp31 1210	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
20		simp32 1211	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁))
21		cgrid2 36146	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → 𝐹 = 𝐺))
22	3, 4, 19, 20, 21	syl13anc 1374	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → 𝐹 = 𝐺))
23		opeq1 4827	. . . . . . . . . . 11 ⊢ (𝐹 = 𝐺 → ⟨𝐹, 𝐻⟩ = ⟨𝐺, 𝐻⟩)
24	23	breq2d 5108	. . . . . . . . . 10 ⊢ (𝐹 = 𝐺 → (⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
25	24	biimprd 248	. . . . . . . . 9 ⊢ (𝐹 = 𝐺 → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
26	22, 25	syl6 35	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
27	26	impd 410	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
28	18, 27	syl5 34	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐵 = 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
29	28	expd 415	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (𝐵 = 𝐶 → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
30	8, 29	mpdd 43	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
31		opeq1 4827	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐶⟩ = ⟨𝐶, 𝐶⟩)
32	31	breq2d 5108	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ↔ 𝐵 Btwn ⟨𝐶, 𝐶⟩))
33	32	anbi1d 631	. . . . . 6 ⊢ (𝐴 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ↔ (𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
34	31	breq1d 5106	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ↔ ⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
35	34	anbi1d 631	. . . . . 6 ⊢ (𝐴 = 𝐶 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ↔ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
36	33, 35	3anbi12d 1439	. . . . 5 ⊢ (𝐴 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ↔ ((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
37	36	imbi1d 341	. . . 4 ⊢ (𝐴 = 𝐶 → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩) ↔ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
38	30, 37	imbitrrid 246	. . 3 ⊢ (𝐴 = 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
39		simp12 1205	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
40		btwndiff 36170	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒))
41	3, 39, 5, 40	syl3anc 1373	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒))
42		simpl11 1249	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
43		simpl23 1254	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
44		simpl32 1256	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐺 ∈ (𝔼‘𝑁))
45		simpl21 1252	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
46		simpr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁))
47		axsegcon 28949	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩))
48	42, 43, 44, 45, 46, 47	syl122anc 1381	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩))
49		anass 468	. . . . . . . . . . . . 13 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) ↔ ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶))))
50		anass 468	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) ↔ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)))
51		simplrl 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
52	51	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
53		simplll 774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
54	53	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
55	52, 54	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩))
56		simpr2l 1233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩)
57	56	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩)
58		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
59	58	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
60	3	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑁 ∈ ℕ)
61	20	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐺 ∈ (𝔼‘𝑁))
62		simplrr 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑓 ∈ (𝔼‘𝑁))
63	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐶 ∈ (𝔼‘𝑁))
64		simplrl 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑒 ∈ (𝔼‘𝑁))
65		cgrcom 36133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
66	60, 61, 62, 63, 64, 65	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
67	59, 66	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩)
68	57, 67	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
69		simprr3 1224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
70	55, 68, 69	3jca 1128	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
71	70	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
72		simpl11 1249	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73		simpl12 1250	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
74		simpl21 1252	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
75		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁))
76		simpl22 1253	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
77		simpl23 1254	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
78		simpl32 1256	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁))
79		simprr 772	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑓 ∈ (𝔼‘𝑁))
80		simpl33 1257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐻 ∈ (𝔼‘𝑁))
81		brofs 36148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
82	72, 73, 74, 75, 76, 77, 78, 79, 80, 81	syl333anc 1404	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
83	71, 82	sylibrd 259	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩))
84		5segofs 36149	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
85	72, 73, 74, 75, 76, 77, 78, 79, 80, 84	syl333anc 1404	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
86	83, 85	syland 603	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
87		simpr1l 1231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
88	87	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
89	51	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
90	88, 89	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩))
91		simpr1r 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐹 Btwn ⟨𝐸, 𝐺⟩)
92	91	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐹 Btwn ⟨𝐸, 𝐺⟩)
93	53	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
94	90, 92, 93	jca32 515	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) ∧ (𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩)))
95		simpl13 1251	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
96		btwnexch3 36163	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) → 𝐶 Btwn ⟨𝐵, 𝑒⟩))
97	72, 73, 95, 74, 75, 96	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) → 𝐶 Btwn ⟨𝐵, 𝑒⟩))
98		simpl31 1255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
99		btwnexch3 36163	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) → 𝐺 Btwn ⟨𝐹, 𝑓⟩))
100	72, 77, 98, 78, 79, 99	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) → 𝐺 Btwn ⟨𝐹, 𝑓⟩))
101	97, 100	anim12d 609	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) ∧ (𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩)) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩)))
102	94, 101	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩)))
103	102	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩))
104		btwncom 36157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ↔ 𝐶 Btwn ⟨𝑒, 𝐵⟩))
105	72, 74, 95, 75, 104	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ↔ 𝐶 Btwn ⟨𝑒, 𝐵⟩))
106		btwncom 36157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn ⟨𝐹, 𝑓⟩ ↔ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
107	72, 78, 98, 79, 106	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn ⟨𝐹, 𝑓⟩ ↔ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
108	105, 107	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩) ↔ (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩)))
109	108	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ((𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩) ↔ (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩)))
110	103, 109	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
111	58	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
112	72, 78, 79, 74, 75, 65	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
113		cgrcomlr 36141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
114	72, 74, 75, 78, 79, 113	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
115	112, 114	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
116	115	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
117	111, 116	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩)
118		simpr2r 1234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
119	118	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
120	72, 95, 74, 98, 78, 119	cgrcomlrand 36144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩)
121	117, 120	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩))
122		simprr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)
123		simpr3r 1236	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
124	123	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
125	122, 124	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
126	110, 121, 125	3jca 1128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
127	126	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
128		brofs 36148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
129	72, 75, 74, 95, 76, 79, 78, 98, 80, 128	syl333anc 1404	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
130	127, 129	sylibrd 259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩))
131		simplrr 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐶 ≠ 𝑒)
132	131	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐶 ≠ 𝑒)
133	132	necomd 2985	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝑒 ≠ 𝐶)
134	133	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝑒 ≠ 𝐶))
135	130, 134	jcad 512	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶)))
136		5segofs 36149	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
137	72, 75, 74, 95, 76, 79, 78, 98, 80, 136	syl333anc 1404	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
138	135, 137	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
139	138	expd 415	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
140	139	adantrd 491	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
141	86, 140	mpdd 43	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
142	50, 141	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
143	49, 142	biimtrrid 243	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶))) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
144	143	expd 415	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
145	144	anassrs 467	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁)) → ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
146	145	rexlimdva 3135	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
147	48, 146	mpd 15	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
148	147	expd 415	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
149	148	rexlimdva 3135	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
150	41, 149	mpd 15	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
151	150	expd 415	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (𝐴 ≠ 𝐶 → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
152	151	com3r 87	. . 3 ⊢ (𝐴 ≠ 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
153	38, 152	pm2.61ine 3013	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
154	1, 153	sylbid 240	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2930 ∃wrex 3058 ⟨cop 4584 class class class wbr 5096 ‘cfv 6490 ℕcn 12143 𝔼cee 28909 Btwn cbtwn 28910 Cgrccgr 28911 OuterFiveSeg cofs 36125 InnerFiveSeg cifs 36178

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-inf2 9548 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-map 8763 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-sup 9343 df-oi 9413 df-card 9849 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-n0 12400 df-z 12487 df-uz 12750 df-rp 12904 df-ico 13265 df-icc 13266 df-fz 13422 df-fzo 13569 df-seq 13923 df-exp 13983 df-hash 14252 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157 df-clim 15409 df-sum 15608 df-ee 28912 df-btwn 28913 df-cgr 28914 df-ofs 36126 df-ifs 36183

This theorem is referenced by: cgrsub 36188 btwnxfr 36199 fscgr 36223 btwnconn1lem5 36234 btwnconn1lem6 36235

W3C validator