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 32542
Description: Lemma for btwnconn1 32545. Using a long string of invocations of linecgr 32525, 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 1245 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
2 simp2l1 1356 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
3 simp2l3 1358 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑐 ∈ (𝔼‘𝑁))
4 simp31 1251 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑃 ∈ (𝔼‘𝑁))
5 simp32 1252 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑄 ∈ (𝔼‘𝑁))
6 simp1l3 1352 . . . . . 6 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐶𝑐)
76ad2antrl 707 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶𝑐)
8 simpr1l 1290 . . . . . . 7 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → 𝐶 Btwn ⟨𝑐, 𝑃⟩)
98ad2antll 708 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝑐, 𝑃⟩)
10 btwncolinear5 32517 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑐, 𝑃⟩ → 𝐶 Colinear ⟨𝑐, 𝑃⟩))
111, 3, 4, 2, 10syl13anc 1478 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑐, 𝑃⟩ → 𝐶 Colinear ⟨𝑐, 𝑃⟩))
1211adantr 466 . . . . . 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 1357 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
15 simp2r1 1359 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑑 ∈ (𝔼‘𝑁))
16 simpr1r 1292 . . . . . . . 8 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩)
1716ad2antll 708 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩)
18 simp2rr 1309 . . . . . . . 8 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)
1918ad2antrl 707 . . . . . . 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 32437 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝐷⟩)
21 btwnconn1lem11 32541 . . . . . . 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 32445 . . . . . 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 32437 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑄⟩)
24 simp12 1246 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
25 simp13 1247 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
26 simp2r2 1360 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
27 simp1rr 1305 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐵 Btwn ⟨𝐴, 𝐷⟩)
2827ad2antrl 707 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐵 Btwn ⟨𝐴, 𝐷⟩)
29 simp2ll 1306 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐷 Btwn ⟨𝐴, 𝑐⟩)
3029ad2antrl 707 . . . . . . . . . . 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 32470 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐵 Btwn ⟨𝐴, 𝑐⟩)
32 simp3ll 1310 . . . . . . . . . . 11 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝑐 Btwn ⟨𝐴, 𝑏⟩)
3332ad2antrl 707 . . . . . . . . . 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 32465 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑐 Btwn ⟨𝐵, 𝑏⟩)
35 opeq1 4539 . . . . . . . . . . . . . 14 (𝐵 = 𝑏 → ⟨𝐵, 𝑏⟩ = ⟨𝑏, 𝑏⟩)
3635breq2d 4798 . . . . . . . . . . . . 13 (𝐵 = 𝑏 → (𝑐 Btwn ⟨𝐵, 𝑏⟩ ↔ 𝑐 Btwn ⟨𝑏, 𝑏⟩))
3736biimpac 464 . . . . . . . . . . . 12 ((𝑐 Btwn ⟨𝐵, 𝑏⟩ ∧ 𝐵 = 𝑏) → 𝑐 Btwn ⟨𝑏, 𝑏⟩)
38 axbtwnid 26040 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑐 Btwn ⟨𝑏, 𝑏⟩ → 𝑐 = 𝑏))
391, 3, 26, 38syl3anc 1476 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝑏, 𝑏⟩ → 𝑐 = 𝑏))
4037, 39syl5 34 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝑐 Btwn ⟨𝐵, 𝑏⟩ ∧ 𝐵 = 𝑏) → 𝑐 = 𝑏))
4140expd 400 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → (𝐵 = 𝑏𝑐 = 𝑏)))
4241adantr 466 . . . . . . . . 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 1130 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
45 simp2l 1241 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)))
46 simp2r 1242 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)))
4744, 45, 463jca 1122 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))))
48 simpl 468 . . . . . . . . . . 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 754 . . . . . . . . . . 11 (((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))) → (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩))
5048, 49jca 501 . . . . . . . . . 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 32537 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩))) → 𝐶𝑑)
5247, 50, 51syl2an 583 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶𝑑)
53 simp2rl 1308 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐶 Btwn ⟨𝐴, 𝑑⟩)
5453ad2antrl 707 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝐴, 𝑑⟩)
55 simp3rl 1312 . . . . . . . . . . . 12 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝑑 Btwn ⟨𝐴, 𝑏⟩)
5655ad2antrl 707 . . . . . . . . . . 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 32465 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑑 Btwn ⟨𝐶, 𝑏⟩)
58 btwncolinear2 32514 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (𝑑 Btwn ⟨𝐶, 𝑏⟩ → 𝐶 Colinear ⟨𝑑, 𝑏⟩))
591, 2, 26, 15, 58syl13anc 1478 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑑 Btwn ⟨𝐶, 𝑏⟩ → 𝐶 Colinear ⟨𝑑, 𝑏⟩))
6059adantr 466 . . . . . . . . . 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 1253 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝑅 ∈ (𝔼‘𝑁))
63 simpr2r 1296 . . . . . . . . . . . . . 14 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩)
6463ad2antll 708 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩)
65 btwnconn1lem5 32535 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ (𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩))) → ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩)
6647, 50, 65syl2an 583 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩)
67 opeq2 4540 . . . . . . . . . . . . . . . . . . 19 (𝑅 = 𝐶 → ⟨𝐶, 𝑅⟩ = ⟨𝐶, 𝐶⟩)
6867breq1d 4796 . . . . . . . . . . . . . . . . . 18 (𝑅 = 𝐶 → (⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ↔ ⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩))
6968anbi1d 615 . . . . . . . . . . . . . . . . 17 (𝑅 = 𝐶 → ((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) ↔ (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩)))
7069biimpac 464 . . . . . . . . . . . . . . . 16 (((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) ∧ 𝑅 = 𝐶) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩))
71 simp2r3 1361 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
72 cgrid2 32447 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ → 𝐶 = 𝐸))
731, 2, 2, 71, 72syl13anc 1478 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ → 𝐶 = 𝐸))
74 opeq1 4539 . . . . . . . . . . . . . . . . . . . 20 (𝐶 = 𝐸 → ⟨𝐶, 𝐶⟩ = ⟨𝐸, 𝐶⟩)
75 opeq1 4539 . . . . . . . . . . . . . . . . . . . 20 (𝐶 = 𝐸 → ⟨𝐶, 𝑐⟩ = ⟨𝐸, 𝑐⟩)
7674, 75breq12d 4799 . . . . . . . . . . . . . . . . . . 19 (𝐶 = 𝐸 → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩ ↔ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩))
7776biimpar 463 . . . . . . . . . . . . . . . . . 18 ((𝐶 = 𝐸 ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → ⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩)
78 cgrid2 32447 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩ → 𝐶 = 𝑐))
791, 2, 2, 3, 78syl13anc 1478 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝑐⟩ → 𝐶 = 𝑐))
8077, 79syl5 34 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝐶 = 𝐸 ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → 𝐶 = 𝑐))
8173, 80syland 590 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((⟨𝐶, 𝐶⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → 𝐶 = 𝑐))
8270, 81syl5 34 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) ∧ 𝑅 = 𝐶) → 𝐶 = 𝑐))
8382expd 400 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → (𝑅 = 𝐶𝐶 = 𝑐)))
8483adantr 466 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ((⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩ ∧ ⟨𝐸, 𝐶⟩Cgr⟨𝐸, 𝑐⟩) → (𝑅 = 𝐶𝐶 = 𝑐)))
8564, 66, 84mp2and 679 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → (𝑅 = 𝐶𝐶 = 𝑐))
8685necon3d 2964 . . . . . . . . . . 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 1294 . . . . . . . . . . . 12 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → 𝐶 Btwn ⟨𝑑, 𝑅⟩)
8988ad2antll 708 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝑑, 𝑅⟩)
90 btwncolinear4 32516 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑑, 𝑅⟩ → 𝑅 Colinear ⟨𝐶, 𝑑⟩))
911, 15, 62, 2, 90syl13anc 1478 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝑑, 𝑅⟩ → 𝑅 Colinear ⟨𝐶, 𝑑⟩))
9291adantr 466 . . . . . . . . . . 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 1300 . . . . . . . . . . . 12 (((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))) → ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)
9594ad2antll 708 . . . . . . . . . . 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 32435 . . . . . . . . . 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 32526 . . . . . . . . 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 32526 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑏, 𝑃⟩Cgr⟨𝑏, 𝑄⟩)
99 opeq1 4539 . . . . . . . . . 10 (𝑐 = 𝑏 → ⟨𝑐, 𝑃⟩ = ⟨𝑏, 𝑃⟩)
100 opeq1 4539 . . . . . . . . . 10 (𝑐 = 𝑏 → ⟨𝑐, 𝑄⟩ = ⟨𝑏, 𝑄⟩)
10199, 100breq12d 4799 . . . . . . . . 9 (𝑐 = 𝑏 → (⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩ ↔ ⟨𝑏, 𝑃⟩Cgr⟨𝑏, 𝑄⟩))
102101biimprd 238 . . . . . . . 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 754 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → 𝐵𝑏)
10634adantrl 695 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → 𝑐 Btwn ⟨𝐵, 𝑏⟩)
107 btwncolinear1 32513 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → 𝐵 Colinear ⟨𝑏, 𝑐⟩))
1081, 25, 26, 3, 107syl13anc 1478 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑐 Btwn ⟨𝐵, 𝑏⟩ → 𝐵 Colinear ⟨𝑏, 𝑐⟩))
109108adantr 466 . . . . . . . . . 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 1304 . . . . . . . . . . . . . 14 ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)
112111ad2antrl 707 . . . . . . . . . . . . 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 32465 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝐶 Btwn ⟨𝐵, 𝑑⟩)
114 btwncolinear6 32518 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑑⟩ → 𝐶 Colinear ⟨𝑑, 𝐵⟩))
1151, 25, 15, 2, 114syl13anc 1478 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐵, 𝑑⟩ → 𝐶 Colinear ⟨𝑑, 𝐵⟩))
116115adantr 466 . . . . . . . . . . . 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 32526 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝐵, 𝑃⟩Cgr⟨𝐵, 𝑄⟩)
119118adantrl 695 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝐵, 𝑃⟩Cgr⟨𝐵, 𝑄⟩)
12098adantrl 695 . . . . . . . . 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 32526 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ (𝐵𝑏 ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩)
122121an12s 628 . . . . . . 7 ((𝐵𝑏 ∧ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩)))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩)
123122ex 397 . . . . . 6 (𝐵𝑏 → ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑐, 𝑃⟩Cgr⟨𝑐, 𝑄⟩))
124104, 123pm2.61ine 3026 . . . . 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 32526 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩)
126 cgrid2 32447 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩ → 𝑃 = 𝑄))
1271, 4, 4, 5, 126syl13anc 1478 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝑃, 𝑃⟩Cgr⟨𝑃, 𝑄⟩ → 𝑃 = 𝑄))
128127adantr 466 . . . 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 32540 . . 3 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩)
131 opeq1 4539 . . . . . . 7 (𝑃 = 𝑄 → ⟨𝑃, 𝑄⟩ = ⟨𝑄, 𝑄⟩)
132131breq2d 4798 . . . . . 6 (𝑃 = 𝑄 → (⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩ ↔ ⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩))
133132biimpa 462 . . . . 5 ((𝑃 = 𝑄 ∧ ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩) → ⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩)
134 axcgrid 26017 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩ → 𝑑 = 𝐷))
1351, 15, 14, 5, 134syl13anc 1478 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (⟨𝑑, 𝐷⟩Cgr⟨𝑄, 𝑄⟩ → 𝑑 = 𝐷))
136133, 135syl5 34 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → ((𝑃 = 𝑄 ∧ ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩) → 𝑑 = 𝐷))
137136adantr 466 . . 3 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → ((𝑃 = 𝑄 ∧ ⟨𝑑, 𝐷⟩Cgr⟨𝑃, 𝑄⟩) → 𝑑 = 𝐷))
138129, 130, 137mp2and 679 . 2 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) ∧ ((((𝐴𝐵𝐵𝐶𝐶𝑐) ∧ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐷⟩)) ∧ ((𝐷 Btwn ⟨𝐴, 𝑐⟩ ∧ ⟨𝐷, 𝑐⟩Cgr⟨𝐶, 𝐷⟩) ∧ (𝐶 Btwn ⟨𝐴, 𝑑⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝐶, 𝐷⟩)) ∧ ((𝑐 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑐, 𝑏⟩Cgr⟨𝐶, 𝐵⟩) ∧ (𝑑 Btwn ⟨𝐴, 𝑏⟩ ∧ ⟨𝑑, 𝑏⟩Cgr⟨𝐷, 𝐵⟩))) ∧ ((𝐸 Btwn ⟨𝐶, 𝑐⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝑑⟩) ∧ ((𝐶 Btwn ⟨𝑐, 𝑃⟩ ∧ ⟨𝐶, 𝑃⟩Cgr⟨𝐶, 𝑑⟩) ∧ (𝐶 Btwn ⟨𝑑, 𝑅⟩ ∧ ⟨𝐶, 𝑅⟩Cgr⟨𝐶, 𝐸⟩) ∧ (𝑅 Btwn ⟨𝑃, 𝑄⟩ ∧ ⟨𝑅, 𝑄⟩Cgr⟨𝑅, 𝑃⟩))))) → 𝑑 = 𝐷)
139138eqcomd 2777 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 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  cop 4322   class class class wbr 4786  cfv 6031  cn 11222  𝔼cee 25989   Btwn cbtwn 25990  Cgrccgr 25991   Colinear ccolin 32481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-ee 25992  df-btwn 25993  df-cgr 25994  df-ofs 32427  df-colinear 32483  df-ifs 32484  df-cgr3 32485  df-fs 32486
This theorem is referenced by:  btwnconn1lem13  32543
  Copyright terms: Public domain W3C validator