Theorem cgrxfr 36036

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 36008	. . . 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 28907	. . . . . . . . 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 28907	. . . . . . . . . . . . . 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 2980	. . . . . . . . . . . . . . . . . . . . 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 36007	. . . . . . . . . . . . . . . . . . . . . 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 36002	. . . . . . . . . . . . . . . . . . . . . . 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 35990	. . . . . . . . . . . . . . . . . . . . . 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 35996	. . . . . . . . . . . . . . . . . . . . . 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 35972	. . . . . . . . . . . . . . . . . . . . . 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 35991	. . . . . . . . . . . . . . . . . . . 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 4834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝐹 → ⟨𝑔, 𝑓⟩ = ⟨𝑔, 𝐹⟩)
65	64	breq2d 5114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝐹 → (𝑒 Btwn ⟨𝑔, 𝑓⟩ ↔ 𝑒 Btwn ⟨𝑔, 𝐹⟩))
66		opeq2 4834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝐹 → ⟨𝑒, 𝑓⟩ = ⟨𝑒, 𝐹⟩)
67	66	breq1d 5112	. . . . . . . . . . . . . . . . . . . . . 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 36001	. . . . . . . . . . . . . . . . . . . . . . . . 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 35972	. . . . . . . . . . . . . . . . . . . . . . 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 35972	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩) ∧ (𝐷 Btwn ⟨𝐹, 𝑔⟩ ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn ⟨𝑔, 𝑒⟩ ∧ ⟨𝐷, 𝑒⟩Cgr⟨𝐴, 𝐵⟩)) ∧ (𝑒 Btwn ⟨𝑔, 𝐹⟩ ∧ ⟨𝑒, 𝐹⟩Cgr⟨𝐵, 𝐶⟩))) → ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝐹⟩)
81		brcgr3 36027	. . . . . . . . . . . . . . . . . . . . . . . . 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 3134	. . . . . . . . . . . 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 3146	. . . . . . 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 3134	. . 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 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  ⟨cop 4591   class class class wbr 5102  ‘cfv 6499  ℕcn 12162  𝔼cee 28868   Btwn cbtwn 28869  Cgrccgr 28870  Cgr3ccgr3 36017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-er 8648  df-map 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-sup 9369  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-z 12506  df-uz 12770  df-rp 12928  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-seq 13943  df-exp 14003  df-hash 14272  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-clim 15430  df-sum 15629  df-ee 28871  df-btwn 28872  df-cgr 28873  df-ofs 35964  df-cgr3 36022

This theorem is referenced by:  btwnxfr  36037  lineext  36057  seglecgr12im  36091  segletr  36095