lineelsb2 - Mathbox for Scott Fenton

	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.

Step	Hyp	Ref	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 ⟨𝑆, 𝑃⟩)))
6	1, 2, 3, 4, 5	syl13anc 1371	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
7	6	biimpa 477	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩))
8		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
9		brcolinear 34452	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
10	1, 8, 3, 4, 9	syl13anc 1371	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
11	10	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
12		btwnconn3 34496	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
13	1, 3, 2, 8, 4, 12	syl122anc 1378	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
14	13	imp 407	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
15		btwncolinear3 34464	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
16	1, 3, 8, 2, 15	syl13anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
17		btwncolinear5 34466	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
18	1, 3, 2, 8, 17	syl13anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
19	16, 18	jaod 856	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
20	19	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
21	14, 20	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
22	21	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
23		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
24	1, 2, 3, 4, 23	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
25		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
26	1, 4, 2, 3, 8, 24, 25	btwnexch3and 34414	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
27		btwncolinear4 34465	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
28	1, 2, 8, 3, 27	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
29	28	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
30	26, 29	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
31	30	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
32		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
33		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
34	1, 4, 8, 3, 33	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
35	1, 3, 2, 4, 8, 32, 34	btwnexchand 34419	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
36	16	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
37	35, 36	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
38	37	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
39	22, 31, 38	3jaod 1427	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
40	11, 39	sylbid 239	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
41		brcolinear 34452	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
42	1, 8, 3, 2, 41	syl13anc 1371	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
43	42	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
44		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
45		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
46	1, 3, 8, 2, 4, 44, 45	btwnexchand 34419	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
47		btwncolinear5 34466	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
48	1, 3, 4, 8, 47	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
49	48	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
50	46, 49	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
51	50	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
52		simpl3r 1228	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑆)
53	52	necomd 2996	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆 ≠ 𝑃)
54	53	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 ≠ 𝑃)
55		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
56	1, 2, 3, 4, 55	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
57		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
58		btwnouttr2 34415	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
59	1, 4, 2, 3, 8, 58	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
60	59	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
61	54, 56, 57, 60	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
62		btwncolinear4 34465	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
63	1, 4, 8, 3, 62	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
64	63	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
65	61, 64	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
66	65	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
67	52	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑆)
68		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
69		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
70	1, 2, 8, 3, 69	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
71		btwnconn1 34494	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
72	1, 3, 2, 4, 8, 71	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
73	72	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
74	67, 68, 70, 73	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
75		btwncolinear3 34464	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
76	1, 3, 8, 4, 75	syl13anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
77	76, 48	jaod 856	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
78	77	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
79	74, 78	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
80	79	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
81	51, 66, 80	3jaod 1427	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
82	43, 81	sylbid 239	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
83	40, 82	impbid 211	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
84	10	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
85		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
86	1, 8, 3, 4, 85	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑄, 𝑃⟩)
87		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
88	1, 4, 8, 3, 2, 86, 87	btwnexch3and 34414	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑥, 𝑆⟩)
89		btwncolinear2 34463	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
90	1, 8, 2, 3, 89	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
91	90	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
92	88, 91	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
93	92	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
94		simpl23 1252	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄)
95	94	necomd 2996	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃)
96	95	adantr 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 ⟨𝑃, 𝑆⟩)))
100	1, 4, 3, 2, 8, 99	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
101	100	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
102	96, 97, 98, 101	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
103	19	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
104	102, 103	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
105	104	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
106	94	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑄)
107		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
108	1, 3, 4, 2, 107	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
109		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
110	1, 4, 8, 3, 109	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
111		btwnouttr 34417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
112	1, 2, 3, 4, 8, 111	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
113	112	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
114	106, 108, 110, 113	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
115	28	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
116	114, 115	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
117	116	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
118	93, 105, 117	3jaod 1427	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
119	84, 118	sylbid 239	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
120	42	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
121		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
122	1, 8, 3, 2, 121	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑆, 𝑃⟩)
123		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
124	1, 3, 4, 2, 123	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
125	1, 2, 8, 3, 4, 122, 124	btwnexch3and 34414	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑥, 𝑄⟩)
126		btwncolinear2 34463	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
127	1, 8, 4, 3, 126	syl13anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
128	127	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
129	125, 128	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
130	129	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
131	53	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 ≠ 𝑃)
132		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
133	1, 3, 4, 2, 132	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
134		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
135		btwnconn2 34495	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
136	1, 2, 3, 4, 8, 135	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
137	136	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
138	131, 133, 134, 137	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
139	77	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
140	138, 139	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
141	140	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
142	52	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑆)
143		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
144		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
145	1, 2, 8, 3, 144	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
146		btwnouttr 34417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
147	1, 4, 3, 2, 8, 146	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
148	147	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
149	142, 143, 145, 148	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
150	63	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
151	149, 150	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
152	151	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
153	130, 141, 152	3jaod 1427	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
154	120, 153	sylbid 239	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
155	119, 154	impbid 211	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
156	10	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
157		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
158		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
159	1, 4, 2, 3, 158	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
160	1, 3, 8, 4, 2, 157, 159	btwnexchand 34419	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
161	18	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
162	160, 161	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
163	162	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
164	95	adantr 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 ⟨𝑆, 𝑥⟩))
168	1, 2, 4, 3, 8, 167	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
169	168	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
170	164, 165, 166, 169	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
171	28	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
172	170, 171	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
173	172	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
174	94	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑄)
175		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
176	1, 4, 2, 3, 175	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
177		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
178	1, 4, 8, 3, 177	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
179		btwnconn1 34494	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
180	1, 3, 4, 2, 8, 179	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
181	180	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
182	174, 176, 178, 181	mp3and 1463	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
183	19	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
184	182, 183	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
185	184	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
186	163, 173, 185	3jaod 1427	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
187	156, 186	sylbid 239	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
188	42	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
189		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
190	1, 4, 2, 3, 189	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
191		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
192		btwnconn3 34496	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
193	1, 3, 4, 8, 2, 192	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
194	193	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
195	190, 191, 194	mp2and 696	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
196	77	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
197	195, 196	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
198	197	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
199		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
200		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
201	1, 2, 4, 3, 8, 199, 200	btwnexch3and 34414	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
202	63	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
203	201, 202	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
204	203	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
205		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
206	1, 4, 2, 3, 205	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
207		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
208	1, 2, 8, 3, 207	btwncomand 34408	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
209	1, 3, 4, 2, 8, 206, 208	btwnexchand 34419	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
210	76	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
211	209, 210	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
212	211	expr 457	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
213	198, 204, 212	3jaod 1427	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
214	188, 213	sylbid 239	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
215	187, 214	impbid 211	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
216	83, 155, 215	3jaodan 1429	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
217	7, 216	syldan 591	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
218	217	adantrl 713	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
219	218	an32s 649	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
220	219	rabbidva 3410	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
221	220	ex 413	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → ((𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
222		fvline2 34539	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
223	222	3adant3 1131	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
224	223	eleq2d 2822	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ 𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩}))
225		breq1 5092	. . . 4 ⊢ (𝑥 = 𝑆 → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
226	225	elrab 3634	. . 3 ⊢ (𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
227	224, 226	bitrdi 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 ⟨𝑃, 𝑆⟩})
233	228, 229, 230, 231, 232	syl13anc 1371	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
234	223, 233	eqeq12d 2752	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → ((𝑃Line𝑄) = (𝑃Line𝑆) ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
235	221, 227, 234	3imtr4d 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

W3C validator