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 36272

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 36271	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
2		simp1l 1204	. . . . . 6 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → 𝐵 Btwn ⟨𝐶, 𝐶⟩)
3		simp11 1210	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
4		simp13 1212	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
5		simp21 1213	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
6		axbtwnid 29026	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐶⟩ → 𝐵 = 𝐶))
7	3, 4, 5, 6	syl3anc 1379	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐶, 𝐶⟩ → 𝐵 = 𝐶))
8	2, 7	syl5 34	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → 𝐵 = 𝐶))
9		simp2r 1207	. . . . . . . . 9 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
10		simp3r 1209	. . . . . . . . 9 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
11	9, 10	jca 516	. . . . . . . 8 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
12		opeq2 4805	. . . . . . . . . . 11 ⊢ (𝐵 = 𝐶 → ⟨𝐵, 𝐵⟩ = ⟨𝐵, 𝐶⟩)
13	12	breq1d 5082	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
14		opeq1 4804	. . . . . . . . . . 11 ⊢ (𝐵 = 𝐶 → ⟨𝐵, 𝐷⟩ = ⟨𝐶, 𝐷⟩)
15	14	breq1d 5082	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
16	13, 15	anbi12d 638	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) ↔ (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
17	16	biimprd 249	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → ((⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
18	11, 17	mpan9 511	. . . . . . 7 ⊢ ((((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐵 = 𝐶) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
19		simp31 1216	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
20		simp32 1217	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁))
21		cgrid2 36231	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → 𝐹 = 𝐺))
22	3, 4, 19, 20, 21	syl13anc 1380	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → 𝐹 = 𝐺))
23		opeq1 4804	. . . . . . . . . . 11 ⊢ (𝐹 = 𝐺 → ⟨𝐹, 𝐻⟩ = ⟨𝐺, 𝐻⟩)
24	23	breq2d 5084	. . . . . . . . . 10 ⊢ (𝐹 = 𝐺 → (⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
25	24	biimprd 249	. . . . . . . . 9 ⊢ (𝐹 = 𝐺 → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
26	22, 25	syl6 35	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
27	26	impd 411	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
28	18, 27	syl5 34	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐵 = 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
29	28	expd 416	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (𝐵 = 𝐶 → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
30	8, 29	mpdd 43	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
31		opeq1 4804	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐶⟩ = ⟨𝐶, 𝐶⟩)
32	31	breq2d 5084	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ↔ 𝐵 Btwn ⟨𝐶, 𝐶⟩))
33	32	anbi1d 637	. . . . . 6 ⊢ (𝐴 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ↔ (𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
34	31	breq1d 5082	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ↔ ⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
35	34	anbi1d 637	. . . . . 6 ⊢ (𝐴 = 𝐶 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ↔ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
36	33, 35	3anbi12d 1445	. . . . 5 ⊢ (𝐴 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ↔ ((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
37	36	imbi1d 342	. . . 4 ⊢ (𝐴 = 𝐶 → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩) ↔ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
38	30, 37	imbitrrid 247	. . 3 ⊢ (𝐴 = 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
39		simp12 1211	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
40		btwndiff 36255	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒))
41	3, 39, 5, 40	syl3anc 1379	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒))
42		simpl11 1255	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
43		simpl23 1260	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
44		simpl32 1262	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐺 ∈ (𝔼‘𝑁))
45		simpl21 1258	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
46		simpr 485	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁))
47		axsegcon 29014	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩))
48	42, 43, 44, 45, 46, 47	syl122anc 1387	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩))
49		anass 469	. . . . . . . . . . . . 13 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) ↔ ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶))))
50		anass 469	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) ↔ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)))
51		simplrl 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
52	51	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
53		simplll 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
54	53	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
55	52, 54	jca 516	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩))
56		simpr2l 1239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩)
57	56	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩)
58		simpllr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
59	58	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
60	3	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑁 ∈ ℕ)
61	20	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐺 ∈ (𝔼‘𝑁))
62		simplrr 783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑓 ∈ (𝔼‘𝑁))
63	5	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐶 ∈ (𝔼‘𝑁))
64		simplrl 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑒 ∈ (𝔼‘𝑁))
65		cgrcom 36218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
66	60, 61, 62, 63, 64, 65	syl122anc 1387	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
67	59, 66	mpbid 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩)
68	57, 67	jca 516	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
69		simprr3 1230	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
70	55, 68, 69	3jca 1134	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
71	70	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
72		simpl11 1255	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73		simpl12 1256	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
74		simpl21 1258	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
75		simprl 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁))
76		simpl22 1259	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
77		simpl23 1260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
78		simpl32 1262	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁))
79		simprr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑓 ∈ (𝔼‘𝑁))
80		simpl33 1263	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐻 ∈ (𝔼‘𝑁))
81		brofs 36233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
82	72, 73, 74, 75, 76, 77, 78, 79, 80, 81	syl333anc 1410	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
83	71, 82	sylibrd 260	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩))
84		5segofs 36234	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
85	72, 73, 74, 75, 76, 77, 78, 79, 80, 84	syl333anc 1410	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
86	83, 85	syland 609	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
87		simpr1l 1237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
88	87	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
89	51	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
90	88, 89	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩))
91		simpr1r 1238	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐹 Btwn ⟨𝐸, 𝐺⟩)
92	91	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐹 Btwn ⟨𝐸, 𝐺⟩)
93	53	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
94	90, 92, 93	jca32 520	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) ∧ (𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩)))
95		simpl13 1257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
96		btwnexch3 36248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) → 𝐶 Btwn ⟨𝐵, 𝑒⟩))
97	72, 73, 95, 74, 75, 96	syl122anc 1387	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) → 𝐶 Btwn ⟨𝐵, 𝑒⟩))
98		simpl31 1261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
99		btwnexch3 36248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) → 𝐺 Btwn ⟨𝐹, 𝑓⟩))
100	72, 77, 98, 78, 79, 99	syl122anc 1387	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) → 𝐺 Btwn ⟨𝐹, 𝑓⟩))
101	97, 100	anim12d 615	. . . . . . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩))
104		btwncom 36242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ↔ 𝐶 Btwn ⟨𝑒, 𝐵⟩))
105	72, 74, 95, 75, 104	syl13anc 1380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ↔ 𝐶 Btwn ⟨𝑒, 𝐵⟩))
106		btwncom 36242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn ⟨𝐹, 𝑓⟩ ↔ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
107	72, 78, 98, 79, 106	syl13anc 1380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn ⟨𝐹, 𝑓⟩ ↔ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
108	105, 107	anbi12d 638	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩) ↔ (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩)))
109	108	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ((𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩) ↔ (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩)))
110	103, 109	mpbid 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
111	58	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
112	72, 78, 79, 74, 75, 65	syl122anc 1387	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
113		cgrcomlr 36226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
114	72, 74, 75, 78, 79, 113	syl122anc 1387	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
115	112, 114	bitrd 280	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
116	115	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
117	111, 116	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩)
118		simpr2r 1240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
119	118	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
120	72, 95, 74, 98, 78, 119	cgrcomlrand 36229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩)
121	117, 120	jca 516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩))
122		simprr 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)
123		simpr3r 1242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
124	123	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
125	122, 124	jca 516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
126	110, 121, 125	3jca 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
127	126	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
128		brofs 36233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
129	72, 75, 74, 95, 76, 79, 78, 98, 80, 128	syl333anc 1410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
130	127, 129	sylibrd 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩))
131		simplrr 783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐶 ≠ 𝑒)
132	131	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐶 ≠ 𝑒)
133	132	necomd 2989	. . . . . . . . . . . . . . . . . . . 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 517	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶)))
136		5segofs 36234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
137	72, 75, 74, 95, 76, 79, 78, 98, 80, 136	syl333anc 1410	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
138	135, 137	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
139	138	expd 416	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
140	139	adantrd 492	. . . . . . . . . . . . . . 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 244	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
143	49, 142	biimtrrid 244	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶))) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
144	143	expd 416	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
145	144	anassrs 468	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁)) → ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
146	145	rexlimdva 3140	. . . . . . . . 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 416	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
149	148	rexlimdva 3140	. . . . . 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 416	. . . 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 3017	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
154	1, 153	sylbid 241	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∃wrex 3063 ⟨cop 4561 class class class wbr 5072 ‘cfv 6485 ℕcn 12165 𝔼cee 28974 Btwn cbtwn 28975 Cgrccgr 28976 OuterFiveSeg cofs 36210 InnerFiveSeg cifs 36263

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 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 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-oi 9415 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-ee 28977 df-btwn 28978 df-cgr 28979 df-ofs 36211 df-ifs 36268

This theorem is referenced by: cgrsub 36273 btwnxfr 36284 fscgr 36308 btwnconn1lem5 36319 btwnconn1lem6 36320

W3C validator