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 36264

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 1192	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
2		simpl3l 1229	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆 ∈ (𝔼‘𝑁))
3		simpl21 1252	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
4		simpl22 1253	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
5		brcolinear 36175	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
6	1, 2, 3, 4, 5	syl13anc 1374	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
7	6	biimpa 476	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩))
8		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
9		brcolinear 36175	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
10	1, 8, 3, 4, 9	syl13anc 1374	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
11	10	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
12		btwnconn3 36219	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
13	1, 3, 2, 8, 4, 12	syl122anc 1381	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
14	13	imp 406	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
15		btwncolinear3 36187	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
16	1, 3, 8, 2, 15	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
17		btwncolinear5 36189	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
18	1, 3, 2, 8, 17	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
19	16, 18	jaod 859	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
20	19	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
21	14, 20	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
22	21	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
23		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
24	1, 2, 3, 4, 23	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
25		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
26	1, 4, 2, 3, 8, 24, 25	btwnexch3and 36137	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
27		btwncolinear4 36188	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
28	1, 2, 8, 3, 27	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
29	28	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
30	26, 29	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
31	30	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
32		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
33		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
34	1, 4, 8, 3, 33	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
35	1, 3, 2, 4, 8, 32, 34	btwnexchand 36142	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
36	16	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
37	35, 36	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
38	37	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
39	22, 31, 38	3jaod 1431	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
40	11, 39	sylbid 240	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
41		brcolinear 36175	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
42	1, 8, 3, 2, 41	syl13anc 1374	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
43	42	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
44		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
45		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
46	1, 3, 8, 2, 4, 44, 45	btwnexchand 36142	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
47		btwncolinear5 36189	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
48	1, 3, 4, 8, 47	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
49	48	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
50	46, 49	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
51	50	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
52		simpl3r 1230	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑆)
53	52	necomd 2984	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆 ≠ 𝑃)
54	53	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 ≠ 𝑃)
55		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
56	1, 2, 3, 4, 55	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
57		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
58		btwnouttr2 36138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
59	1, 4, 2, 3, 8, 58	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
60	59	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
61	54, 56, 57, 60	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
62		btwncolinear4 36188	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
63	1, 4, 8, 3, 62	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
64	63	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
65	61, 64	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
66	65	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
67	52	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑆)
68		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
69		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
70	1, 2, 8, 3, 69	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
71		btwnconn1 36217	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
72	1, 3, 2, 4, 8, 71	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
74	67, 68, 70, 73	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
75		btwncolinear3 36187	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
76	1, 3, 8, 4, 75	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
77	76, 48	jaod 859	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
78	77	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
79	74, 78	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
80	79	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
81	51, 66, 80	3jaod 1431	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
82	43, 81	sylbid 240	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
83	40, 82	impbid 212	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
84	10	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
85		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
86	1, 8, 3, 4, 85	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑄, 𝑃⟩)
87		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
88	1, 4, 8, 3, 2, 86, 87	btwnexch3and 36137	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑥, 𝑆⟩)
89		btwncolinear2 36186	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
90	1, 8, 2, 3, 89	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
91	90	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
92	88, 91	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
93	92	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
94		simpl23 1254	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄)
95	94	necomd 2984	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃)
96	95	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 ≠ 𝑃)
97		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
98		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
99		btwnconn2 36218	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
100	1, 4, 3, 2, 8, 99	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
101	100	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
102	96, 97, 98, 101	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
103	19	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
104	102, 103	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
105	104	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
106	94	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑄)
107		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
108	1, 3, 4, 2, 107	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
109		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
110	1, 4, 8, 3, 109	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
111		btwnouttr 36140	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
112	1, 2, 3, 4, 8, 111	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
113	112	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
114	106, 108, 110, 113	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
115	28	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
116	114, 115	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
117	116	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
118	93, 105, 117	3jaod 1431	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
119	84, 118	sylbid 240	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
120	42	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
121		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
122	1, 8, 3, 2, 121	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑆, 𝑃⟩)
123		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
124	1, 3, 4, 2, 123	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
125	1, 2, 8, 3, 4, 122, 124	btwnexch3and 36137	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑥, 𝑄⟩)
126		btwncolinear2 36186	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
127	1, 8, 4, 3, 126	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
128	127	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
129	125, 128	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
130	129	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
131	53	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 ≠ 𝑃)
132		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
133	1, 3, 4, 2, 132	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
134		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
135		btwnconn2 36218	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
136	1, 2, 3, 4, 8, 135	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
137	136	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
138	131, 133, 134, 137	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
139	77	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
140	138, 139	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
141	140	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
142	52	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑆)
143		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
144		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
145	1, 2, 8, 3, 144	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
146		btwnouttr 36140	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
147	1, 4, 3, 2, 8, 146	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
148	147	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
149	142, 143, 145, 148	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
150	63	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
151	149, 150	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
152	151	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
153	130, 141, 152	3jaod 1431	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
154	120, 153	sylbid 240	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
155	119, 154	impbid 212	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
156	10	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
157		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
158		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
159	1, 4, 2, 3, 158	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
160	1, 3, 8, 4, 2, 157, 159	btwnexchand 36142	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
161	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
162	160, 161	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
163	162	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
164	95	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 ≠ 𝑃)
165		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
166		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
167		btwnouttr2 36138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
168	1, 2, 4, 3, 8, 167	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
169	168	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
170	164, 165, 166, 169	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
171	28	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
172	170, 171	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
173	172	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
174	94	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑄)
175		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
176	1, 4, 2, 3, 175	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
177		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
178	1, 4, 8, 3, 177	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
179		btwnconn1 36217	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
180	1, 3, 4, 2, 8, 179	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
181	180	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
182	174, 176, 178, 181	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
183	19	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
184	182, 183	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
185	184	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
186	163, 173, 185	3jaod 1431	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
187	156, 186	sylbid 240	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
188	42	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
189		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
190	1, 4, 2, 3, 189	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
191		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
192		btwnconn3 36219	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
193	1, 3, 4, 8, 2, 192	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
194	193	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
195	190, 191, 194	mp2and 699	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
196	77	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
197	195, 196	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
198	197	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
199		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
200		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
201	1, 2, 4, 3, 8, 199, 200	btwnexch3and 36137	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
202	63	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
203	201, 202	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
204	203	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
205		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
206	1, 4, 2, 3, 205	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
207		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
208	1, 2, 8, 3, 207	btwncomand 36131	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
209	1, 3, 4, 2, 8, 206, 208	btwnexchand 36142	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
210	76	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
211	209, 210	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
212	211	expr 456	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
213	198, 204, 212	3jaod 1431	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
214	188, 213	sylbid 240	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
215	187, 214	impbid 212	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
216	83, 155, 215	3jaodan 1433	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
217	7, 216	syldan 591	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
218	217	adantrl 716	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
219	218	an32s 652	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
220	219	rabbidva 3402	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
221	220	ex 412	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → ((𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
222		fvline2 36262	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
223	222	3adant3 1132	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
224	223	eleq2d 2819	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ 𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩}))
225		breq1 5098	. . . 4 ⊢ (𝑥 = 𝑆 → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
226	225	elrab 3643	. . 3 ⊢ (𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
227	224, 226	bitrdi 287	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)))
228		simp1 1136	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑁 ∈ ℕ)
229		simp21 1207	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑃 ∈ (𝔼‘𝑁))
230		simp3l 1202	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑆 ∈ (𝔼‘𝑁))
231		simp3r 1203	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑃 ≠ 𝑆)
232		fvline2 36262	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
233	228, 229, 230, 231, 232	syl13anc 1374	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
234	223, 233	eqeq12d 2749	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → ((𝑃Line𝑄) = (𝑃Line𝑆) ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
235	221, 227, 234	3imtr4d 294	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 {crab 3396 ⟨cop 4583 class class class wbr 5095 ‘cfv 6489 (class class class)co 7355 ℕcn 12136 𝔼cee 28886 Btwn cbtwn 28887 Colinear ccolin 36153 Linecline2 36250

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 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-inf2 9542 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094 ax-pre-sup 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-er 8631 df-ec 8633 df-map 8761 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9337 df-oi 9407 df-card 9843 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-div 11786 df-nn 12137 df-2 12199 df-3 12200 df-n0 12393 df-z 12480 df-uz 12743 df-rp 12897 df-ico 13258 df-icc 13259 df-fz 13415 df-fzo 13562 df-seq 13916 df-exp 13976 df-hash 14245 df-cj 15013 df-re 15014 df-im 15015 df-sqrt 15149 df-abs 15150 df-clim 15402 df-sum 15601 df-ee 28889 df-btwn 28890 df-cgr 28891 df-ofs 36099 df-colinear 36155 df-ifs 36156 df-cgr3 36157 df-fs 36158 df-line2 36253

This theorem is referenced by: linethru 36269

W3C validator