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

Theorem btwnconn1lem12 35630
Description: Lemma for btwnconn1 35633. Using a long string of invocations of linecgr 35613, we show that 𝐷 = 𝑑. (Contributed by Scott Fenton, 9-Oct-2013.)
Assertion
Ref Expression
btwnconn1lem12 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐷 = 𝑑)

Proof of Theorem btwnconn1lem12
StepHypRef Expression
1 simp11 1201 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
2 simp2l1 1270 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
3 simp2l3 1272 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑐 ∈ (𝔼‘𝑁))
4 simp31 1207 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑃 ∈ (𝔼‘𝑁))
5 simp32 1208 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑄 ∈ (𝔼‘𝑁))
6 simp1l3 1266 . . . . . 6 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐶𝑐)
76ad2antrl 727 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶𝑐)
8 simpr1l 1228 . . . . . . 7 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → 𝐶 Btwn ⟨𝑐, 𝑃⟩)
98ad2antll 728 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝑐, 𝑃⟩)
10 btwncolinear5 35605 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑐, 𝑃⟩ → 𝐶 Colinear ⟨𝑐, 𝑃⟩))
111, 3, 4, 2, 10syl13anc 1370 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑐, 𝑃⟩ → 𝐶 Colinear ⟨𝑐, 𝑃⟩))
1211adantr 480 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝐶 Btwn ⟨𝑐, 𝑃⟩ → 𝐶 Colinear ⟨𝑐, 𝑃⟩))
139, 12mpd 15 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Colinear ⟨𝑐, 𝑃⟩)
14 simp2l2 1271 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
15 simp2r1 1273 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑑 ∈ (𝔼‘𝑁))
16 simpr1r 1229 . . . . . . . 8 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩)
1716ad2antll 728 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩)
18 simp2rr 1241 . . . . . . . 8 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)
1918ad2antrl 727 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)
201, 2, 4, 2, 15, 2, 14, 17, 19cgrtrand 35525 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝐷⟩)
21 btwnconn1lem11 35629 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐷, 𝐶⟩Cgr⟨𝑄, 𝐶⟩)
221, 14, 2, 5, 2, 21cgrcomlrand 35533 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝐷⟩Cgr⟨𝐶, 𝑄⟩)
231, 2, 4, 2, 14, 2, 5, 20, 22cgrtrand 35525 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑄⟩)
24 simp12 1202 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
25 simp13 1203 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
26 simp2r2 1274 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
27 simp1rr 1237 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐵 Btwn ⟨𝐴, 𝐷⟩)
2827ad2antrl 727 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐵 Btwn ⟨𝐴, 𝐷⟩)
29 simp2ll 1238 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐷 Btwn ⟨𝐴, 𝑐⟩)
3029ad2antrl 727 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐷 Btwn ⟨𝐴, 𝑐⟩)
311, 24, 25, 14, 3, 28, 30btwnexchand 35558 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐵 Btwn ⟨𝐴, 𝑐⟩)
32 simp3ll 1242 . . . . . . . . . . 11 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝑐 Btwn ⟨𝐴, 𝑏⟩)
3332ad2antrl 727 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑐 Btwn ⟨𝐴, 𝑏⟩)
341, 24, 25, 3, 26, 31, 33btwnexch3and 35553 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑐 Btwn ⟨𝐵, 𝑏⟩)
35 opeq1 4869 . . . . . . . . . . . . . 14 (𝐵 = 𝑏 → ⟨𝐵, 𝑏⟩ = ⟨𝑏, 𝑏⟩)
3635breq2d 5154 . . . . . . . . . . . . 13 (𝐵 = 𝑏 → (𝑐 Btwn ⟨𝐵, 𝑏⟩ ↔ 𝑐 Btwn ⟨𝑏, 𝑏⟩))
3736biimpac 478 . . . . . . . . . . . 12 ((𝑐 Btwn ⟨𝐵, 𝑏⟩ ∧ 𝐵 = 𝑏) → 𝑐 Btwn ⟨𝑏, 𝑏⟩)
38 axbtwnid 28737 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑐 Btwn ⟨𝑏, 𝑏⟩ → 𝑐 = 𝑏))
391, 3, 26, 38syl3anc 1369 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝑏, 𝑏⟩ → 𝑐 = 𝑏))
4037, 39syl5 34 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝑐 Btwn ⟨𝐵, 𝑏⟩ ∧ 𝐵 = 𝑏) → 𝑐 = 𝑏))
4140expd 415 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → (𝐵 = 𝑏𝑐 = 𝑏)))
4241adantr 480 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → (𝐵 = 𝑏𝑐 = 𝑏)))
4334, 42mpd 15 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝐵 = 𝑏𝑐 = 𝑏))
44 simp1 1134 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
45 simp2l 1197 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)))
46 simp2r 1198 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)))
4744, 45, 463jca 1126 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))))
48 simpl 482 . . . . . . . . . . 11 (((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))) → (((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))))
49 simprl 770 . . . . . . . . . . 11 (((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))) → (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩))
5048, 49jca 511 . . . . . . . . . 10 (((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))) → ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩)))
51 btwnconn1lem7 35625 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩))) → 𝐶𝑑)
5247, 50, 51syl2an 595 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶𝑑)
53 simp2rl 1240 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐶 Btwn ⟨𝐴, 𝑑⟩)
5453ad2antrl 727 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝐴, 𝑑⟩)
55 simp3rl 1244 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝑑 Btwn ⟨𝐴, 𝑏⟩)
5655ad2antrl 727 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑑 Btwn ⟨𝐴, 𝑏⟩)
571, 24, 2, 15, 26, 54, 56btwnexch3and 35553 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑑 Btwn ⟨𝐶, 𝑏⟩)
58 btwncolinear2 35602 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (𝑑 Btwn ⟨𝐶, 𝑏⟩ → 𝐶 Colinear ⟨𝑑, 𝑏⟩))
591, 2, 26, 15, 58syl13anc 1370 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑑 Btwn ⟨𝐶, 𝑏⟩ → 𝐶 Colinear ⟨𝑑, 𝑏⟩))
6059adantr 480 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝑑 Btwn ⟨𝐶, 𝑏⟩ → 𝐶 Colinear ⟨𝑑, 𝑏⟩))
6157, 60mpd 15 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Colinear ⟨𝑑, 𝑏⟩)
62 simp33 1209 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑅 ∈ (𝔼‘𝑁))
63 simpr2r 1231 . . . . . . . . . . . . . 14 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩)
6463ad2antll 728 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩)
65 btwnconn1lem5 35623 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩))) → ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩)
6647, 50, 65syl2an 595 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩)
67 opeq2 4870 . . . . . . . . . . . . . . . . . . 19 (𝑅 = 𝐶 → ⟨𝐶, 𝑅⟩ = ⟨𝐶, 𝐶⟩)
6867breq1d 5152 . . . . . . . . . . . . . . . . . 18 (𝑅 = 𝐶 → (⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ↔ ⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩))
6968anbi1d 629 . . . . . . . . . . . . . . . . 17 (𝑅 = 𝐶 → ((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) ↔ (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩)))
7069biimpac 478 . . . . . . . . . . . . . . . 16 (((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) ∧ 𝑅 = 𝐶) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩))
71 simp2r3 1275 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
72 cgrid2 35535 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ → 𝐶 = 𝐸))
731, 2, 2, 71, 72syl13anc 1370 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ → 𝐶 = 𝐸))
74 opeq1 4869 . . . . . . . . . . . . . . . . . . . 20 (𝐶 = 𝐸 → ⟨𝐶, 𝐶⟩ = ⟨𝐸, 𝐶⟩)
75 opeq1 4869 . . . . . . . . . . . . . . . . . . . 20 (𝐶 = 𝐸 → ⟨𝐶, 𝑐⟩ = ⟨𝐸, 𝑐⟩)
7674, 75breq12d 5155 . . . . . . . . . . . . . . . . . . 19 (𝐶 = 𝐸 → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩ ↔ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩))
7776biimpar 477 . . . . . . . . . . . . . . . . . 18 ((𝐶 = 𝐸 ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → ⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩)
78 cgrid2 35535 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩ → 𝐶 = 𝑐))
791, 2, 2, 3, 78syl13anc 1370 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩ → 𝐶 = 𝑐))
8077, 79syl5 34 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝐶 = 𝐸 ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → 𝐶 = 𝑐))
8173, 80syland 602 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → 𝐶 = 𝑐))
8270, 81syl5 34 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) ∧ 𝑅 = 𝐶) → 𝐶 = 𝑐))
8382expd 415 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → (𝑅 = 𝐶𝐶 = 𝑐)))
8483adantr 480 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → (𝑅 = 𝐶𝐶 = 𝑐)))
8564, 66, 84mp2and 698 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝑅 = 𝐶𝐶 = 𝑐))
8685necon3d 2956 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝐶𝑐𝑅𝐶))
877, 86mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑅𝐶)
88 simpr2l 1230 . . . . . . . . . . . 12 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → 𝐶 Btwn ⟨𝑑, 𝑅⟩)
8988ad2antll 728 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝑑, 𝑅⟩)
90 btwncolinear4 35604 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑑, 𝑅⟩ → 𝑅 Colinear ⟨𝐶, 𝑑⟩))
911, 15, 62, 2, 90syl13anc 1370 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑑, 𝑅⟩ → 𝑅 Colinear ⟨𝐶, 𝑑⟩))
9291adantr 480 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝐶 Btwn ⟨𝑑, 𝑅⟩ → 𝑅 Colinear ⟨𝐶, 𝑑⟩))
9389, 92mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑅 Colinear ⟨𝐶, 𝑑⟩)
94 simpr3r 1233 . . . . . . . . . . . 12 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)
9594ad2antll 728 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)
961, 62, 5, 62, 4, 95cgrcomand 35523 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑅, 𝑃⟩Cgr⟨𝑅, 𝑄⟩)
971, 62, 2, 15, 4, 5, 87, 93, 96, 23linecgrand 35614 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑑, 𝑃⟩Cgr⟨𝑑, 𝑄⟩)
981, 2, 15, 26, 4, 5, 52, 61, 23, 97linecgrand 35614 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑏, 𝑃⟩Cgr⟨𝑏, 𝑄⟩)
99 opeq1 4869 . . . . . . . . . 10 (𝑐 = 𝑏 → ⟨𝑐, 𝑃⟩ = ⟨𝑏, 𝑃⟩)
100 opeq1 4869 . . . . . . . . . 10 (𝑐 = 𝑏 → ⟨𝑐, 𝑄⟩ = ⟨𝑏, 𝑄⟩)
10199, 100breq12d 5155 . . . . . . . . 9 (𝑐 = 𝑏 → (⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩ ↔ ⟨𝑏, 𝑃⟩Cgr⟨𝑏, 𝑄⟩))
102101biimprd 247 . . . . . . . 8 (𝑐 = 𝑏 → (⟨𝑏, 𝑃⟩Cgr⟨𝑏, 𝑄⟩ → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩))
10343, 98, 102syl6ci 71 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝐵 = 𝑏 → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩))
104103com12 32 . . . . . 6 (𝐵 = 𝑏 → ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩))
105 simprl 770 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → 𝐵𝑏)
10634adantrl 715 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → 𝑐 Btwn ⟨𝐵, 𝑏⟩)
107 btwncolinear1 35601 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → 𝐵 Colinear ⟨𝑏, 𝑐⟩))
1081, 25, 26, 3, 107syl13anc 1370 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → 𝐵 Colinear ⟨𝑏, 𝑐⟩))
109108adantr 480 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → 𝐵 Colinear ⟨𝑏, 𝑐⟩))
110106, 109mpd 15 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → 𝐵 Colinear ⟨𝑏, 𝑐⟩)
111 simp1rl 1236 . . . . . . . . . . . . . 14 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
112111ad2antrl 727 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
1131, 24, 25, 2, 15, 112, 54btwnexch3and 35553 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝐵, 𝑑⟩)
114 btwncolinear6 35606 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑑⟩ → 𝐶 Colinear ⟨𝑑, 𝐵⟩))
1151, 25, 15, 2, 114syl13anc 1370 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑑⟩ → 𝐶 Colinear ⟨𝑑, 𝐵⟩))
116115adantr 480 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝐶 Btwn ⟨𝐵, 𝑑⟩ → 𝐶 Colinear ⟨𝑑, 𝐵⟩))
117113, 116mpd 15 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Colinear ⟨𝑑, 𝐵⟩)
1181, 2, 15, 25, 4, 5, 52, 117, 23, 97linecgrand 35614 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐵, 𝑃⟩Cgr⟨𝐵, 𝑄⟩)
119118adantrl 715 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝐵, 𝑃⟩Cgr⟨𝐵, 𝑄⟩)
12098adantrl 715 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝑏, 𝑃⟩Cgr⟨𝑏, 𝑄⟩)
1211, 25, 26, 3, 4, 5, 105, 110, 119, 120linecgrand 35614 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩)
122121an12s 648 . . . . . . 7 ((𝐵𝑏 ∧ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩)
123122ex 412 . . . . . 6 (𝐵𝑏 → ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩))
124104, 123pm2.61ine 3020 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩)
1251, 2, 3, 4, 4, 5, 7, 13, 23, 124linecgrand 35614 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩)
126 cgrid2 35535 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩ → 𝑃 = 𝑄))
1271, 4, 4, 5, 126syl13anc 1370 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩ → 𝑃 = 𝑄))
128127adantr 480 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩ → 𝑃 = 𝑄))
129125, 128mpd 15 . . 3 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑃 = 𝑄)
130 btwnconn1lem10 35628 . . 3 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩)
131 opeq1 4869 . . . . . . 7 (𝑃 = 𝑄 → ⟨𝑃, 𝑄⟩ = ⟨𝑄, 𝑄⟩)
132131breq2d 5154 . . . . . 6 (𝑃 = 𝑄 → (⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩ ↔ ⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩))
133132biimpa 476 . . . . 5 ((𝑃 = 𝑄 ∧ ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩) → ⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩)
134 axcgrid 28714 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩ → 𝑑 = 𝐷))
1351, 15, 14, 5, 134syl13anc 1370 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩ → 𝑑 = 𝐷))
136133, 135syl5 34 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝑃 = 𝑄 ∧ ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩) → 𝑑 = 𝐷))
137136adantr 480 . . 3 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ((𝑃 = 𝑄 ∧ ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩) → 𝑑 = 𝐷))
138129, 130, 137mp2and 698 . 2 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑑 = 𝐷)
139138eqcomd 2733 1 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐷 = 𝑑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2935  cop 4630   class class class wbr 5142  cfv 6542  cn 12234  𝔼cee 28686   Btwn cbtwn 28687  Cgrccgr 28688   Colinear ccolin 35569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657  df-ee 28689  df-btwn 28690  df-cgr 28691  df-ofs 35515  df-colinear 35571  df-ifs 35572  df-cgr3 35573  df-fs 35574
This theorem is referenced by:  btwnconn1lem13  35631
  Copyright terms: Public domain W3C validator