Theorem cgrxfr 36198

Description: A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.)

Assertion

Ref	Expression
cgrxfr	⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))

Distinct variable groups:   𝐴,𝑒   𝐵,𝑒   𝐶,𝑒   𝐷,𝑒   𝑒,𝐹   𝑒,𝑁

Proof of Theorem cgrxfr

Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1192	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → 𝑁 ∈ ℕ)
2		simpl3r 1230	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → 𝐹 ∈ (𝔼‘𝑁))
3		simpl3l 1229	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → 𝐷 ∈ (𝔼‘𝑁))
4		btwndiff 36170	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → ∃𝑔 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))
5	1, 2, 3, 4	syl3anc 1373	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → ∃𝑔 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))
6		simpl1 1192	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
7		simpr 484	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝑔 ∈ (𝔼‘𝑁))
8		simpl3l 1229	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
9		simpl21 1252	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
10		simpl22 1253	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
11		axsegcon 28949	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))
12	6, 7, 8, 9, 10, 11	syl122anc 1381	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))
13	12	adantr 480	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))
14		anass 468	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ 𝑒 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))))
15		simpl1 1192	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
16		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝑔 ∈ (𝔼‘𝑁))
17		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁))
18		simpl22 1253	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
19		simpl23 1254	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
20		axsegcon 28949	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))
21	15, 16, 17, 18, 19, 20	syl122anc 1381	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))
22	21	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))
23		anass 468	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ 𝑓 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁))))
24		df-3an 1088	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ↔ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁)))
25	24	anbi2i 623	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁))))
26	23, 25	bitr4i 278	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ 𝑓 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))))
27		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) → 𝐷 ≠ 𝑔)
28	27	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝐷 ≠ 𝑔)
29	28	necomd 2985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝑔 ≠ 𝐷)
30		simpl1 1192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
31		simpr1 1195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑔 ∈ (𝔼‘𝑁))
32		simpl3l 1229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
33		simpr2 1196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁))
34		simpr3 1197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑓 ∈ (𝔼‘𝑁))
35		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) → 𝐷 Btwn ⟨𝑔, 𝑒⟩)
36	35	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝐷 Btwn ⟨𝑔, 𝑒⟩)
37		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝑒 Btwn ⟨𝑔, 𝑓⟩)
38	30, 31, 32, 33, 34, 36, 37	btwnexchand 36169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝐷 Btwn ⟨𝑔, 𝑓⟩)
39		simpl21 1252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
40		simpl22 1253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
41		simpl23 1254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
42	30, 31, 32, 33, 34, 36, 37	btwnexch3and 36164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝑒 Btwn ⟨𝐷, 𝑓⟩)
43		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
44	43	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
45		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) → ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)
46	45	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)
47		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩)
48	30, 32, 33, 34, 39, 40, 41, 42, 44, 46, 47	cgrextendand 36152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐷, 𝑓⟩Cgr⟨𝐴, 𝐶⟩)
49	38, 48	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → (𝐷 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝐷, 𝑓⟩Cgr⟨𝐴, 𝐶⟩))
50		simpl3r 1230	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
51		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) → 𝐷 Btwn ⟨𝐹, 𝑔⟩)
52	51	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝐷 Btwn ⟨𝐹, 𝑔⟩)
53	30, 32, 50, 31, 52	btwncomand 36158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝐷 Btwn ⟨𝑔, 𝐹⟩)
54		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)
55	54	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)
56	30, 39, 41, 32, 50, 55	cgrcomand 36134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐷, 𝐹⟩Cgr⟨𝐴, 𝐶⟩)
57	53, 56	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → (𝐷 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝐷, 𝐹⟩Cgr⟨𝐴, 𝐶⟩))
58	29, 49, 57	3jca 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → (𝑔 ≠ 𝐷 ∧ (𝐷 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝐷, 𝑓⟩Cgr⟨𝐴, 𝐶⟩) ∧ (𝐷 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝐷, 𝐹⟩Cgr⟨𝐴, 𝐶⟩)))
59	58	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩)) → (𝑔 ≠ 𝐷 ∧ (𝐷 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝐷, 𝑓⟩Cgr⟨𝐴, 𝐶⟩) ∧ (𝐷 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝐷, 𝐹⟩Cgr⟨𝐴, 𝐶⟩))))
60		segconeq 36153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝑔 ≠ 𝐷 ∧ (𝐷 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝐷, 𝑓⟩Cgr⟨𝐴, 𝐶⟩) ∧ (𝐷 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝐷, 𝐹⟩Cgr⟨𝐴, 𝐶⟩)) → 𝑓 = 𝐹))
61	30, 32, 39, 41, 31, 34, 50, 60	syl133anc 1395	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝑔 ≠ 𝐷 ∧ (𝐷 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝐷, 𝑓⟩Cgr⟨𝐴, 𝐶⟩) ∧ (𝐷 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝐷, 𝐹⟩Cgr⟨𝐴, 𝐶⟩)) → 𝑓 = 𝐹))
62	59, 61	syld 47	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩)) → 𝑓 = 𝐹))
63	62	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → 𝑓 = 𝐹)
64		opeq2 4828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝐹 → ⟨𝑔, 𝑓⟩ = ⟨𝑔, 𝐹⟩)
65	64	breq2d 5108	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝐹 → (𝑒 Btwn ⟨𝑔, 𝑓⟩ ↔ 𝑒 Btwn ⟨𝑔, 𝐹⟩))
66		opeq2 4828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝐹 → ⟨𝑒, 𝑓⟩ = ⟨𝑒, 𝐹⟩)
67	66	breq1d 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝐹 → (⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩ ↔ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))
68	65, 67	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → ((𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩) ↔ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩)))
69	68	biimpa 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = 𝐹 ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩)) → (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))
70		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩) → 𝑒 Btwn ⟨𝑔, 𝐹⟩)
71		btwnexch3 36163	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℕ ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ 𝑒 Btwn ⟨𝑔, 𝐹⟩) → 𝑒 Btwn ⟨𝐷, 𝐹⟩))
72	30, 31, 32, 33, 50, 71	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ 𝑒 Btwn ⟨𝑔, 𝐹⟩) → 𝑒 Btwn ⟨𝐷, 𝐹⟩))
73	35, 70, 72	syl2ani 607	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩)) → 𝑒 Btwn ⟨𝐷, 𝐹⟩))
74	73	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → 𝑒 Btwn ⟨𝐷, 𝐹⟩)
75		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩)) → ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)
76	75	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)
77	30, 32, 33, 39, 40, 76	cgrcomand 36134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩)
78	54	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)
79		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩)
80	30, 33, 50, 40, 41, 79	cgrcomand 36134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝐹⟩)
81		brcgr3 36189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝐹⟩)))
82	30, 39, 40, 41, 32, 33, 50, 81	syl133anc 1395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝐹⟩)))
83	82	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝐹⟩)))
84	77, 78, 80, 83	mpbir3and 1343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)
85	74, 84	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩))
86	85	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → ((𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
87	69, 86	syl5 34	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → ((𝑓 = 𝐹 ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩)) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
88	87	expcomd 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → ((𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩) → (𝑓 = 𝐹 → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩))))
89	88	impr 454	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → (𝑓 = 𝐹 → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
90	63, 89	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩))) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩))
91	90	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → ((𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
92	26, 91	sylanb 581	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → ((𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
93	92	an32s 652	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) ∧ 𝑓 ∈ (𝔼‘𝑁)) → ((𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
94	93	rexlimdva 3135	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → (∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝑔, 𝑓⟩ ∧ ⟨𝑒, 𝑓⟩Cgr⟨𝐵, 𝐶⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
95	22, 94	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩))) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩))
96	95	expr 456	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))) → ((𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
97	14, 96	sylanb 581	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))) → ((𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
98	97	an32s 652	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ((𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩) → (𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
99	98	reximdva 3147	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))) → (∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
100	13, 99	mpd 15	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩))
101	100	expr 456	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → ((𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
102	101	an32s 652	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) ∧ 𝑔 ∈ (𝔼‘𝑁)) → ((𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
103	102	rexlimdva 3135	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → (∃𝑔 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))
104	5, 103	mpd 15	. 2 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩))
105	104	ex 412	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn ⟨𝐷, 𝐹⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝑒, 𝐹⟩⟩)))

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

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

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

This theorem is referenced by:  btwnxfr  36199  lineext  36219  seglecgr12im  36253  segletr  36257