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 36789

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 36788	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
2		simp1l 1216	. . . . . 6 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → 𝐵 Btwn ⟨𝐶, 𝐶⟩)
3		simp11 1222	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
4		simp13 1224	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
5		simp21 1225	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
6		axbtwnid 29510	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐶⟩ → 𝐵 = 𝐶))
7	3, 4, 5, 6	syl3anc 1398	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐶, 𝐶⟩ → 𝐵 = 𝐶))
8	2, 7	syl5 35	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → 𝐵 = 𝐶))
9		simp2r 1219	. . . . . . . . 9 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
10		simp3r 1221	. . . . . . . . 9 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
11	9, 10	jca 521	. . . . . . . 8 ⊢ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
12		opeq2 4834	. . . . . . . . . . 11 ⊢ (𝐵 = 𝐶 → ⟨𝐵, 𝐵⟩ = ⟨𝐵, 𝐶⟩)
13	12	breq1d 5113	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
14		opeq1 4833	. . . . . . . . . . 11 ⊢ (𝐵 = 𝐶 → ⟨𝐵, 𝐷⟩ = ⟨𝐶, 𝐷⟩)
15	14	breq1d 5113	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
16	13, 15	anbi12d 644	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) ↔ (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
17	16	biimprd 251	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → ((⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
18	11, 17	mpan9 516	. . . . . . 7 ⊢ ((((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐵 = 𝐶) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
19		simp31 1228	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
20		simp32 1229	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁))
21		cgrid2 36748	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → 𝐹 = 𝐺))
22	3, 4, 19, 20, 21	syl13anc 1399	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → 𝐹 = 𝐺))
23		opeq1 4833	. . . . . . . . . . 11 ⊢ (𝐹 = 𝐺 → ⟨𝐹, 𝐻⟩ = ⟨𝐺, 𝐻⟩)
24	23	breq2d 5115	. . . . . . . . . 10 ⊢ (𝐹 = 𝐺 → (⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
25	24	biimprd 251	. . . . . . . . 9 ⊢ (𝐹 = 𝐺 → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
26	22, 25	syl6 36	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ → (⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
27	26	impd 416	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨𝐵, 𝐵⟩Cgr⟨𝐹, 𝐺⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
28	18, 27	syl5 35	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐵 = 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
29	28	expd 421	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (𝐵 = 𝐶 → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
30	8, 29	mpdd 44	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
31		opeq1 4833	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐶⟩ = ⟨𝐶, 𝐶⟩)
32	31	breq2d 5115	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ↔ 𝐵 Btwn ⟨𝐶, 𝐶⟩))
33	32	anbi1d 643	. . . . . 6 ⊢ (𝐴 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ↔ (𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
34	31	breq1d 5113	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ↔ ⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
35	34	anbi1d 643	. . . . . 6 ⊢ (𝐴 = 𝐶 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ↔ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
36	33, 35	3anbi12d 1465	. . . . 5 ⊢ (𝐴 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ↔ ((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
37	36	imbi1d 344	. . . 4 ⊢ (𝐴 = 𝐶 → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩) ↔ (((𝐵 Btwn ⟨𝐶, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐶, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
38	30, 37	imbitrrid 249	. . 3 ⊢ (𝐴 = 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
39		simp12 1223	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
40		btwndiff 36772	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒))
41	3, 39, 5, 40	syl3anc 1398	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒))
42		simpl11 1267	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
43		simpl23 1272	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
44		simpl32 1274	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐺 ∈ (𝔼‘𝑁))
45		simpl21 1270	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
46		simpr 490	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁))
47		axsegcon 29498	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩))
48	42, 43, 44, 45, 46, 47	syl122anc 1406	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩))
49		anass 474	. . . . . . . . . . . . 13 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) ↔ ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶))))
50		anass 474	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) ↔ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)))
51		simplrl 789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
52	51	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
53		simplll 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
54	53	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
55	52, 54	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩))
56		simpr2l 1251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩)
57	56	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩)
58		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
59	58	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
60	3	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑁 ∈ ℕ)
61	20	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐺 ∈ (𝔼‘𝑁))
62		simplrr 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑓 ∈ (𝔼‘𝑁))
63	5	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝐶 ∈ (𝔼‘𝑁))
64		simplrl 789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → 𝑒 ∈ (𝔼‘𝑁))
65		cgrcom 36735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
66	60, 61, 62, 63, 64, 65	syl122anc 1406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
67	59, 66	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩)
68	57, 67	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
69		simprr3 1242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
70	55, 68, 69	3jca 1146	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
71	70	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
72		simpl11 1267	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73		simpl12 1268	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
74		simpl21 1270	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
75		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁))
76		simpl22 1271	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
77		simpl23 1272	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
78		simpl32 1274	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁))
79		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑓 ∈ (𝔼‘𝑁))
80		simpl33 1275	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐻 ∈ (𝔼‘𝑁))
81		brofs 36750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
82	72, 73, 74, 75, 76, 77, 78, 79, 80, 81	syl333anc 1429	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
83	71, 82	sylibrd 262	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩))
84		5segofs 36751	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
85	72, 73, 74, 75, 76, 77, 78, 79, 80, 84	syl333anc 1429	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐶⟩, ⟨𝑒, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐺⟩, ⟨𝑓, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
86	83, 85	syland 615	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩))
87		simpr1l 1249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
88	87	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
89	51	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐶 Btwn ⟨𝐴, 𝑒⟩)
90	88, 89	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩))
91		simpr1r 1250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐹 Btwn ⟨𝐸, 𝐺⟩)
92	91	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐹 Btwn ⟨𝐸, 𝐺⟩)
93	53	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐺 Btwn ⟨𝐸, 𝑓⟩)
94	90, 92, 93	jca32 525	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) ∧ (𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩)))
95		simpl13 1269	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
96		btwnexch3 36765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) → 𝐶 Btwn ⟨𝐵, 𝑒⟩))
97	72, 73, 95, 74, 75, 96	syl122anc 1406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) → 𝐶 Btwn ⟨𝐵, 𝑒⟩))
98		simpl31 1273	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
99		btwnexch3 36765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) → 𝐺 Btwn ⟨𝐹, 𝑓⟩))
100	72, 77, 98, 78, 79, 99	syl122anc 1406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩) → 𝐺 Btwn ⟨𝐹, 𝑓⟩))
101	97, 100	anim12d 621	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑒⟩) ∧ (𝐹 Btwn ⟨𝐸, 𝐺⟩ ∧ 𝐺 Btwn ⟨𝐸, 𝑓⟩)) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩)))
102	94, 101	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩)))
103	102	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩))
104		btwncom 36759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ↔ 𝐶 Btwn ⟨𝑒, 𝐵⟩))
105	72, 74, 95, 75, 104	syl13anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑒⟩ ↔ 𝐶 Btwn ⟨𝑒, 𝐵⟩))
106		btwncom 36759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn ⟨𝐹, 𝑓⟩ ↔ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
107	72, 78, 98, 79, 106	syl13anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn ⟨𝐹, 𝑓⟩ ↔ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
108	105, 107	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩) ↔ (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩)))
109	108	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ((𝐶 Btwn ⟨𝐵, 𝑒⟩ ∧ 𝐺 Btwn ⟨𝐹, 𝑓⟩) ↔ (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩)))
110	103, 109	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩))
111	58	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩)
112	72, 78, 79, 74, 75, 65	syl122anc 1406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩))
113		cgrcomlr 36743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
114	72, 74, 75, 78, 79, 113	syl122anc 1406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝑒⟩Cgr⟨𝐺, 𝑓⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
115	112, 114	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
116	115	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩ ↔ ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩))
117	111, 116	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩)
118		simpr2r 1252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
119	118	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)
120	72, 95, 74, 98, 78, 119	cgrcomlrand 36746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩)
121	117, 120	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩))
122		simprr 785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)
123		simpr3r 1254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
124	123	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)
125	122, 124	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
126	110, 121, 125	3jca 1146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩)) → ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
127	126	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
128		brofs 36750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
129	72, 75, 74, 95, 76, 79, 78, 98, 80, 128	syl333anc 1429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ↔ ((𝐶 Btwn ⟨𝑒, 𝐵⟩ ∧ 𝐺 Btwn ⟨𝑓, 𝐹⟩) ∧ (⟨𝑒, 𝐶⟩Cgr⟨𝑓, 𝐺⟩ ∧ ⟨𝐶, 𝐵⟩Cgr⟨𝐺, 𝐹⟩) ∧ (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
130	127, 129	sylibrd 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩))
131		simplrr 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → 𝐶 ≠ 𝑒)
132	131	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → 𝐶 ≠ 𝑒)
133	132	necomd 3011	. . . . . . . . . . . . . . . . . . . 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 522	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → (⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶)))
136		5segofs 36751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
137	72, 75, 74, 95, 76, 79, 78, 98, 80, 136	syl333anc 1429	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((⟨⟨𝑒, 𝐶⟩, ⟨𝐵, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝑓, 𝐺⟩, ⟨𝐹, 𝐻⟩⟩ ∧ 𝑒 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
138	135, 137	syld 48	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ ⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
139	138	expd 421	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
140	139	adantrd 497	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → (⟨𝑒, 𝐷⟩Cgr⟨𝑓, 𝐻⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
141	86, 140	mpdd 44	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
142	50, 141	biimtrrid 246	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
143	49, 142	biimtrrid 246	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) ∧ ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶))) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
144	143	expd 421	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
145	144	anassrs 473	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁)) → ((𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
146	145	rexlimdva 3164	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn ⟨𝐸, 𝑓⟩ ∧ ⟨𝐺, 𝑓⟩Cgr⟨𝐶, 𝑒⟩) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
147	48, 146	mpd 16	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
148	147	expd 421	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ((𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
149	148	rexlimdva 3164	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn ⟨𝐴, 𝑒⟩ ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
150	41, 149	mpd 16	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) ∧ 𝐴 ≠ 𝐶) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
151	150	expd 421	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → (𝐴 ≠ 𝐶 → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
152	151	com3r 88	. . 3 ⊢ (𝐴 ≠ 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
153	38, 152	pm2.61ine 3039	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)) → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
154	1, 153	sylbid 243	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∃wrex 3087 ⟨cop 4590 class class class wbr 5103 ‘cfv 6537 ℕcn 12328 𝔼cee 29458 Btwn cbtwn 29459 Cgrccgr 29460 OuterFiveSeg cofs 36727 InnerFiveSeg cifs 36780

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-er 8710 df-map 8842 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-z 12687 df-uz 12959 df-rp 13114 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-sum 15847 df-ee 29461 df-btwn 29462 df-cgr 29463 df-ofs 36728 df-ifs 36785

This theorem is used by: cgrsub 36790 btwnxfr 36801 fscgr 36825 btwnconn1lem5 36836 btwnconn1lem6 36837

W3C validator