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

Theorem lineelsb2 34541
Description: If 𝑆 lies on 𝑃𝑄, then 𝑃𝑄 = 𝑃𝑆. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
lineelsb2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆)))

Proof of Theorem lineelsb2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1190 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
2 simpl3l 1227 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆 ∈ (𝔼‘𝑁))
3 simpl21 1250 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
4 simpl22 1251 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
5 brcolinear 34452 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
61, 2, 3, 4, 5syl13anc 1371 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
76biimpa 477 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩))
8 simpr 485 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
9 brcolinear 34452 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
101, 8, 3, 4, 9syl13anc 1371 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
1110adantr 481 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
12 btwnconn3 34496 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
131, 3, 2, 8, 4, 12syl122anc 1378 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
1413imp 407 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
15 btwncolinear3 34464 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
161, 3, 8, 2, 15syl13anc 1371 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
17 btwncolinear5 34466 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
181, 3, 2, 8, 17syl13anc 1371 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
1916, 18jaod 856 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
2019adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
2114, 20mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
2221expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
23 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
241, 2, 3, 4, 23btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
25 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
261, 4, 2, 3, 8, 24, 25btwnexch3and 34414 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
27 btwncolinear4 34465 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
281, 2, 8, 3, 27syl13anc 1371 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
2928adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
3026, 29mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
3130expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
32 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
33 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
341, 4, 8, 3, 33btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
351, 3, 2, 4, 8, 32, 34btwnexchand 34419 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
3616adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
3735, 36mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
3837expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
3922, 31, 383jaod 1427 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
4011, 39sylbid 239 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
41 brcolinear 34452 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
421, 8, 3, 2, 41syl13anc 1371 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
4342adantr 481 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
44 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
45 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
461, 3, 8, 2, 4, 44, 45btwnexchand 34419 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
47 btwncolinear5 34466 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
481, 3, 4, 8, 47syl13anc 1371 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
4948adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
5046, 49mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
5150expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
52 simpl3r 1228 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃𝑆)
5352necomd 2996 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆𝑃)
5453adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆𝑃)
55 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
561, 2, 3, 4, 55btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
57 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
58 btwnouttr2 34415 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆𝑃𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
591, 4, 2, 3, 8, 58syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆𝑃𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
6059adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆𝑃𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
6154, 56, 57, 60mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
62 btwncolinear4 34465 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
631, 4, 8, 3, 62syl13anc 1371 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
6463adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
6561, 64mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
6665expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
6752adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃𝑆)
68 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
69 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
701, 2, 8, 3, 69btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
71 btwnconn1 34494 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃𝑆𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
721, 3, 2, 4, 8, 71syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃𝑆𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
7372adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃𝑆𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
7467, 68, 70, 73mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
75 btwncolinear3 34464 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
761, 3, 8, 4, 75syl13anc 1371 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
7776, 48jaod 856 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
7877adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
7974, 78mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
8079expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
8151, 66, 803jaod 1427 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
8243, 81sylbid 239 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
8340, 82impbid 211 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
8410adantr 481 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
85 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
861, 8, 3, 4, 85btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑄, 𝑃⟩)
87 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
881, 4, 8, 3, 2, 86, 87btwnexch3and 34414 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑥, 𝑆⟩)
89 btwncolinear2 34463 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
901, 8, 2, 3, 89syl13anc 1371 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
9190adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
9288, 91mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
9392expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
94 simpl23 1252 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃𝑄)
9594necomd 2996 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄𝑃)
9695adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄𝑃)
97 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
98 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
99 btwnconn2 34495 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄𝑃𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
1001, 4, 3, 2, 8, 99syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄𝑃𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
101100adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄𝑃𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
10296, 97, 98, 101mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
10319adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
104102, 103mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
105104expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
10694adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃𝑄)
107 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
1081, 3, 4, 2, 107btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
109 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
1101, 4, 8, 3, 109btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
111 btwnouttr 34417 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃𝑄𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
1121, 2, 3, 4, 8, 111syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃𝑄𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
113112adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃𝑄𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
114106, 108, 110, 113mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
11528adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
116114, 115mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
117116expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
11893, 105, 1173jaod 1427 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
11984, 118sylbid 239 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
12042adantr 481 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
121 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
1221, 8, 3, 2, 121btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑆, 𝑃⟩)
123 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
1241, 3, 4, 2, 123btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
1251, 2, 8, 3, 4, 122, 124btwnexch3and 34414 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑥, 𝑄⟩)
126 btwncolinear2 34463 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
1271, 8, 4, 3, 126syl13anc 1371 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
128127adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
129125, 128mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
130129expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
13153adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆𝑃)
132 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
1331, 3, 4, 2, 132btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
134 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
135 btwnconn2 34495 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆𝑃𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
1361, 2, 3, 4, 8, 135syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆𝑃𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
137136adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆𝑃𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
138131, 133, 134, 137mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
13977adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
140138, 139mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
141140expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
14252adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃𝑆)
143 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
144 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
1451, 2, 8, 3, 144btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
146 btwnouttr 34417 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃𝑆𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
1471, 4, 3, 2, 8, 146syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃𝑆𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
148147adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃𝑆𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
149142, 143, 145, 148mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
15063adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
151149, 150mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
152151expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
153130, 141, 1523jaod 1427 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
154120, 153sylbid 239 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
155119, 154impbid 211 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
15610adantr 481 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
157 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
158 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
1591, 4, 2, 3, 158btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
1601, 3, 8, 4, 2, 157, 159btwnexchand 34419 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
16118adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
162160, 161mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
163162expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
16495adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄𝑃)
165 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
166 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
167 btwnouttr2 34415 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄𝑃𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
1681, 2, 4, 3, 8, 167syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄𝑃𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
169168adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄𝑃𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
170164, 165, 166, 169mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
17128adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
172170, 171mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
173172expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
17494adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃𝑄)
175 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
1761, 4, 2, 3, 175btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
177 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
1781, 4, 8, 3, 177btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
179 btwnconn1 34494 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃𝑄𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
1801, 3, 4, 2, 8, 179syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃𝑄𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
181180adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃𝑄𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
182174, 176, 178, 181mp3and 1463 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
18319adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
184182, 183mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
185184expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
186163, 173, 1853jaod 1427 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
187156, 186sylbid 239 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
18842adantr 481 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
189 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
1901, 4, 2, 3, 189btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
191 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
192 btwnconn3 34496 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
1931, 3, 4, 8, 2, 192syl122anc 1378 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
194193adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
195190, 191, 194mp2and 696 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
19677adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
197195, 196mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
198197expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
199 simprl 768 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
200 simprr 770 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
2011, 2, 4, 3, 8, 199, 200btwnexch3and 34414 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
20263adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
203201, 202mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
204203expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
205 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
2061, 4, 2, 3, 205btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
207 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
2081, 2, 8, 3, 207btwncomand 34408 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
2091, 3, 4, 2, 8, 206, 208btwnexchand 34419 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
21076adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
211209, 210mpd 15 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
212211expr 457 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
213198, 204, 2123jaod 1427 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
214188, 213sylbid 239 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
215187, 214impbid 211 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
21683, 155, 2153jaodan 1429 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
2177, 216syldan 591 . . . . . 6 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
218217adantrl 713 . . . . 5 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
219218an32s 649 . . . 4 ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
220219rabbidva 3410 . . 3 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
221220ex 413 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → ((𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
222 fvline2 34539 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
2232223adant3 1131 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
224223eleq2d 2822 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ 𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩}))
225 breq1 5092 . . . 4 (𝑥 = 𝑆 → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
226225elrab 3634 . . 3 (𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
227224, 226bitrdi 286 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)))
228 simp1 1135 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → 𝑁 ∈ ℕ)
229 simp21 1205 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → 𝑃 ∈ (𝔼‘𝑁))
230 simp3l 1200 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → 𝑆 ∈ (𝔼‘𝑁))
231 simp3r 1201 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → 𝑃𝑆)
232 fvline2 34539 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
233228, 229, 230, 231, 232syl13anc 1371 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
234223, 233eqeq12d 2752 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → ((𝑃Line𝑄) = (𝑃Line𝑆) ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
235221, 227, 2343imtr4d 293 1 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844  w3o 1085  w3a 1086   = wceq 1540  wcel 2105  wne 2940  {crab 3403  cop 4578   class class class wbr 5089  cfv 6473  (class class class)co 7329  cn 12066  𝔼cee 27486   Btwn cbtwn 27487   Colinear ccolin 34430  Linecline2 34527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-inf2 9490  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-er 8561  df-ec 8563  df-map 8680  df-en 8797  df-dom 8798  df-sdom 8799  df-fin 8800  df-sup 9291  df-oi 9359  df-card 9788  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-div 11726  df-nn 12067  df-2 12129  df-3 12130  df-n0 12327  df-z 12413  df-uz 12676  df-rp 12824  df-ico 13178  df-icc 13179  df-fz 13333  df-fzo 13476  df-seq 13815  df-exp 13876  df-hash 14138  df-cj 14901  df-re 14902  df-im 14903  df-sqrt 15037  df-abs 15038  df-clim 15288  df-sum 15489  df-ee 27489  df-btwn 27490  df-cgr 27491  df-ofs 34376  df-colinear 34432  df-ifs 34433  df-cgr3 34434  df-fs 34435  df-line2 34530
This theorem is referenced by:  linethru  34546
  Copyright terms: Public domain W3C validator