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 36459

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 1204	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
2		simpl3l 1241	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆 ∈ (𝔼‘𝑁))
3		simpl21 1264	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
4		simpl22 1265	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
5		brcolinear 36370	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
6	1, 2, 3, 4, 5	syl13anc 1390	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)))
7	6	biimpa 480	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩))
8		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
9		brcolinear 36370	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
10	1, 8, 3, 4, 9	syl13anc 1390	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
11	10	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
12		btwnconn3 36414	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
13	1, 3, 2, 8, 4, 12	syl122anc 1397	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
14	13	imp 410	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
15		btwncolinear3 36382	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
16	1, 3, 8, 2, 15	syl13anc 1390	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
17		btwncolinear5 36384	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
18	1, 3, 2, 8, 17	syl13anc 1390	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
19	16, 18	jaod 870	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
20	19	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
21	14, 20	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
22	21	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
23		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
24	1, 2, 3, 4, 23	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
25		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
26	1, 4, 2, 3, 8, 24, 25	btwnexch3and 36332	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
27		btwncolinear4 36383	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
28	1, 2, 8, 3, 27	syl13anc 1390	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
29	28	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
30	26, 29	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
31	30	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
32		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
33		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
34	1, 4, 8, 3, 33	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
35	1, 3, 2, 4, 8, 32, 34	btwnexchand 36337	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
36	16	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
37	35, 36	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
38	37	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
39	22, 31, 38	3jaod 1448	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
40	11, 39	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
41		brcolinear 36370	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
42	1, 8, 3, 2, 41	syl13anc 1390	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
43	42	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
44		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
45		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
46	1, 3, 8, 2, 4, 44, 45	btwnexchand 36337	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
47		btwncolinear5 36384	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
48	1, 3, 4, 8, 47	syl13anc 1390	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
49	48	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
50	46, 49	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
51	50	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
52		simpl3r 1242	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑆)
53	52	necomd 3011	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑆 ≠ 𝑃)
54	53	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 ≠ 𝑃)
55		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
56	1, 2, 3, 4, 55	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 Btwn ⟨𝑄, 𝑃⟩)
57		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
58		btwnouttr2 36333	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
59	1, 4, 2, 3, 8, 58	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
60	59	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆 ≠ 𝑃 ∧ 𝑆 Btwn ⟨𝑄, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
61	54, 56, 57, 60	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
62		btwncolinear4 36383	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
63	1, 4, 8, 3, 62	syl13anc 1390	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
64	63	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
65	61, 64	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
66	65	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
67	52	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑆)
68		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑄⟩)
69		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
70	1, 2, 8, 3, 69	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
71		btwnconn1 36412	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
72	1, 3, 2, 4, 8, 71	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
73	72	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑆 ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
74	67, 68, 70, 73	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
75		btwncolinear3 36382	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
76	1, 3, 8, 4, 75	syl13anc 1390	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
77	76, 48	jaod 870	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
78	77	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
79	74, 78	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
80	79	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
81	51, 66, 80	3jaod 1448	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
82	43, 81	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
83	40, 82	impbid 214	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Btwn ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
84	10	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
85		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
86	1, 8, 3, 4, 85	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑄, 𝑃⟩)
87		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
88	1, 4, 8, 3, 2, 86, 87	btwnexch3and 36332	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 Btwn ⟨𝑥, 𝑆⟩)
89		btwncolinear2 36381	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
90	1, 8, 2, 3, 89	syl13anc 1390	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
91	90	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑃 Btwn ⟨𝑥, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
92	88, 91	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
93	92	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
94		simpl23 1266	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄)
95	94	necomd 3011	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃)
96	95	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 ≠ 𝑃)
97		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
98		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
99		btwnconn2 36413	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
100	1, 4, 3, 2, 8, 99	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
101	100	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
102	96, 97, 98, 101	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
103	19	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
104	102, 103	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
105	104	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
106	94	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑄)
107		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
108	1, 3, 4, 2, 107	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
109		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
110	1, 4, 8, 3, 109	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
111		btwnouttr 36335	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
112	1, 2, 3, 4, 8, 111	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
113	112	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑄 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
114	106, 108, 110, 113	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
115	28	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
116	114, 115	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
117	116	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
118	93, 105, 117	3jaod 1448	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
119	84, 118	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
120	42	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
121		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
122	1, 8, 3, 2, 121	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑆, 𝑃⟩)
123		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
124	1, 3, 4, 2, 123	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
125	1, 2, 8, 3, 4, 122, 124	btwnexch3and 36332	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑃 Btwn ⟨𝑥, 𝑄⟩)
126		btwncolinear2 36381	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
127	1, 8, 4, 3, 126	syl13anc 1390	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
128	127	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
129	125, 128	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
130	129	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
131	53	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑆 ≠ 𝑃)
132		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
133	1, 3, 4, 2, 132	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑄⟩)
134		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
135		btwnconn2 36413	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
136	1, 2, 3, 4, 8, 135	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
137	136	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑆 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑆, 𝑄⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
138	131, 133, 134, 137	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
139	77	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
140	138, 139	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
141	140	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
142	52	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑆)
143		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑆⟩)
144		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
145	1, 2, 8, 3, 144	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
146		btwnouttr 36335	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
147	1, 4, 3, 2, 8, 146	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
148	147	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑆 ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
149	142, 143, 145, 148	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
150	63	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
151	149, 150	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑆⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
152	151	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
153	130, 141, 152	3jaod 1448	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
154	120, 153	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
155	119, 154	impbid 214	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑆⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
156	10	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
157		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑄⟩)
158		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
159	1, 4, 2, 3, 158	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
160	1, 3, 8, 4, 2, 157, 159	btwnexchand 36337	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
161	18	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
162	160, 161	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
163	162	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
164	95	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 ≠ 𝑃)
165		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
166		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
167		btwnouttr2 36333	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
168	1, 2, 4, 3, 8, 167	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
169	168	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → 𝑃 Btwn ⟨𝑆, 𝑥⟩))
170	164, 165, 166, 169	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
171	28	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
172	170, 171	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
173	172	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
174	94	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑃 ≠ 𝑄)
175		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
176	1, 4, 2, 3, 175	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
177		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑥, 𝑃⟩)
178	1, 4, 8, 3, 177	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
179		btwnconn1 36412	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
180	1, 3, 4, 2, 8, 179	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
181	180	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑃 ≠ 𝑄 ∧ 𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑄 Btwn ⟨𝑃, 𝑥⟩) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩)))
182	174, 176, 178, 181	mp3and 1484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → (𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩))
183	19	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → ((𝑆 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
184	182, 183	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑄 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑆⟩)
185	184	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
186	163, 173, 185	3jaod 1448	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
187	156, 186	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑆⟩))
188	42	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩)))
189		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
190	1, 4, 2, 3, 189	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
191		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Btwn ⟨𝑃, 𝑆⟩)
192		btwnconn3 36414	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁))) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
193	1, 3, 4, 8, 2, 192	syl122anc 1397	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
194	193	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑆⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
195	190, 191, 194	mp2and 709	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
196	77	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
197	195, 196	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑆⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
198	197	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Btwn ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
199		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
200		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑆, 𝑥⟩)
201	1, 2, 4, 3, 8, 199, 200	btwnexch3and 36332	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
202	63	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
203	201, 202	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑃 Btwn ⟨𝑆, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
204	203	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑃 Btwn ⟨𝑆, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
205		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑆, 𝑃⟩)
206	1, 4, 2, 3, 205	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑆⟩)
207		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑥, 𝑃⟩)
208	1, 2, 8, 3, 207	btwncomand 36326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑆 Btwn ⟨𝑃, 𝑥⟩)
209	1, 3, 4, 2, 8, 206, 208	btwnexchand 36337	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑄 Btwn ⟨𝑃, 𝑥⟩)
210	76	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
211	209, 210	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑄 Btwn ⟨𝑆, 𝑃⟩ ∧ 𝑆 Btwn ⟨𝑥, 𝑃⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
212	211	expr 460	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑆 Btwn ⟨𝑥, 𝑃⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
213	198, 204, 212	3jaod 1448	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → ((𝑥 Btwn ⟨𝑃, 𝑆⟩ ∨ 𝑃 Btwn ⟨𝑆, 𝑥⟩ ∨ 𝑆 Btwn ⟨𝑥, 𝑃⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
214	188, 213	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑆⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
215	187, 214	impbid 214	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑄 Btwn ⟨𝑆, 𝑃⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
216	83, 155, 215	3jaodan 1450	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑆⟩ ∨ 𝑄 Btwn ⟨𝑆, 𝑃⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
217	7, 216	syldan 600	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
218	217	adantrl 726	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
219	218	an32s 662	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑥 Colinear ⟨𝑃, 𝑆⟩))
220	219	rabbidva 3419	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
221	220	ex 416	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → ((𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
222		fvline2 36457	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
223	222	3adant3 1144	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
224	223	eleq2d 2847	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ 𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩}))
225		breq1 5100	. . . 4 ⊢ (𝑥 = 𝑆 → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
226	225	elrab 3649	. . 3 ⊢ (𝑆 ∈ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩))
227	224, 226	bitrdi 289	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) ↔ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑆 Colinear ⟨𝑃, 𝑄⟩)))
228		simp1 1148	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑁 ∈ ℕ)
229		simp21 1219	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑃 ∈ (𝔼‘𝑁))
230		simp3l 1214	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑆 ∈ (𝔼‘𝑁))
231		simp3r 1215	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → 𝑃 ≠ 𝑆)
232		fvline2 36457	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
233	228, 229, 230, 231, 232	syl13anc 1390	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑃Line𝑆) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩})
234	223, 233	eqeq12d 2777	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → ((𝑃Line𝑄) = (𝑃Line𝑆) ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑆⟩}))
235	221, 227, 234	3imtr4d 296	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∨ w3o 1096 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 {crab 3413 ⟨cop 4585 class class class wbr 5097 ‘cfv 6516 (class class class)co 7391 ℕcn 12204 𝔼cee 29045 Btwn cbtwn 29046 Colinear ccolin 36348 Linecline2 36445

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-inf2 9590 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-er 8672 df-ec 8674 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9382 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-n0 12476 df-z 12563 df-uz 12834 df-rp 12988 df-ico 13349 df-icc 13350 df-fz 13507 df-fzo 13654 df-seq 14009 df-exp 14069 df-hash 14338 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-clim 15506 df-sum 15705 df-ee 29048 df-btwn 29049 df-cgr 29050 df-ofs 36294 df-colinear 36350 df-ifs 36351 df-cgr3 36352 df-fs 36353 df-line2 36448

This theorem is referenced by: linethru 36464

W3C validator