lineunray - Mathbox for Scott Fenton

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

Theorem lineunray 34376

Description: A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
lineunray	⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn ⟨𝑄, 𝑅⟩ → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))))

Proof of Theorem lineunray Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1189	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
2		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
3		simpl21 1249	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
4		simpl22 1250	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
5		brcolinear 34288	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
6	1, 2, 3, 4, 5	syl13anc 1370	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
7	6	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
8		olc 864	. . . . . . . . . . . . . 14 ⊢ (𝑥 Btwn ⟨𝑃, 𝑄⟩ → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
9	8	orcd 869	. . . . . . . . . . . . 13 ⊢ (𝑥 Btwn ⟨𝑃, 𝑄⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
10	9	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
11		simpl3l 1226	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄)
12	11	necomd 2998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃)
13	12	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 ≠ 𝑃)
14		simprl 767	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑅⟩)
15		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
16	13, 14, 15	3jca 1126	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩))
17		simpl23 1251	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑅 ∈ (𝔼‘𝑁))
18		btwnconn2 34331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
19	1, 4, 3, 17, 2, 18	syl122anc 1377	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
20	19	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
21	16, 20	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))
22	21	olcd 870	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
23	22	expr 456	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
24		btwncom 34243	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ ↔ 𝑄 Btwn ⟨𝑃, 𝑥⟩))
25	1, 4, 2, 3, 24	syl13anc 1370	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ ↔ 𝑄 Btwn ⟨𝑃, 𝑥⟩))
26		orc 863	. . . . . . . . . . . . . . 15 ⊢ (𝑄 Btwn ⟨𝑃, 𝑥⟩ → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
27	26	orcd 869	. . . . . . . . . . . . . 14 ⊢ (𝑄 Btwn ⟨𝑃, 𝑥⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
28	25, 27	syl6bi 252	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
29	28	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
30	10, 23, 29	3jaod 1426	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
31	7, 30	sylbid 239	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
32		olc 864	. . . . . . . . . 10 ⊢ (((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
33	31, 32	syl6 35	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ → (𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
34		colineartriv1 34296	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) → 𝑃 Colinear ⟨𝑃, 𝑄⟩)
35	1, 3, 4, 34	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 Colinear ⟨𝑃, 𝑄⟩)
36		breq1 5073	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑃 → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑃 Colinear ⟨𝑃, 𝑄⟩))
37	35, 36	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑃 → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
38	37	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 = 𝑃 → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
39		btwncolinear3 34300	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
40	1, 3, 2, 4, 39	syl13anc 1370	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
41		btwncolinear5 34302	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
42	1, 3, 4, 2, 41	syl13anc 1370	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
43	40, 42	jaod 855	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
44	43	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
45		simpl3r 1227	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑅)
46	45	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑃 ≠ 𝑅)
47		simprl 767	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑅⟩)
48		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑅 Btwn ⟨𝑃, 𝑥⟩)
49	46, 47, 48	3jca 1126	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → (𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩))
50		btwnouttr 34253	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
51	1, 4, 3, 17, 2, 50	syl122anc 1377	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
52	51	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
53	49, 52	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
54		btwncolinear4 34301	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
55	1, 4, 2, 3, 54	syl13anc 1370	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
56	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
57	53, 56	mpd 15	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
58	57	expr 456	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
59		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Btwn ⟨𝑃, 𝑅⟩)
60	1, 2, 3, 17, 59	btwncomand 34244	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Btwn ⟨𝑅, 𝑃⟩)
61		simprl 767	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑃 Btwn ⟨𝑄, 𝑅⟩)
62	1, 3, 4, 17, 61	btwncomand 34244	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑃 Btwn ⟨𝑅, 𝑄⟩)
63	1, 17, 2, 3, 4, 60, 62	btwnexch3and 34250	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑃 Btwn ⟨𝑥, 𝑄⟩)
64		btwncolinear2 34299	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
65	1, 2, 4, 3, 64	syl13anc 1370	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
66	65	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
67	63, 66	mpd 15	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
68	67	expr 456	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Btwn ⟨𝑃, 𝑅⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
69	58, 68	jaod 855	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
70	44, 69	jaod 855	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
71	38, 70	jaod 855	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
72	33, 71	impbid 211	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
73		pm5.63 1016	. . . . . . . . 9 ⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ (𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
74		df-ne 2943	. . . . . . . . . . . 12 ⊢ (𝑥 ≠ 𝑃 ↔ ¬ 𝑥 = 𝑃)
75	74	anbi1i 623	. . . . . . . . . . 11 ⊢ ((𝑥 ≠ 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
76		andi 1004	. . . . . . . . . . 11 ⊢ ((𝑥 ≠ 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
77	75, 76	bitr3i 276	. . . . . . . . . 10 ⊢ ((¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
78	77	orbi2i 909	. . . . . . . . 9 ⊢ ((𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
79	73, 78	bitri 274	. . . . . . . 8 ⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
80	72, 79	bitrdi 286	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))))
81		broutsideof2 34351	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝑄, 𝑥⟩ ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
82	1, 3, 4, 2, 81	syl13anc 1370	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑄, 𝑥⟩ ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
83		3simpc 1148	. . . . . . . . . . . 12 ⊢ ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
84		simpl3l 1226	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → 𝑃 ≠ 𝑄)
85	84	necomd 2998	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → 𝑄 ≠ 𝑃)
86		simprrl 777	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → 𝑥 ≠ 𝑃)
87		simprrr 778	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
88	85, 86, 87	3jca 1126	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
89	88	expr 456	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
90	83, 89	impbid2 225	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
91	82, 90	bitrd 278	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑄, 𝑥⟩ ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
92		broutsideof2 34351	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝑅, 𝑥⟩ ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
93	1, 3, 17, 2, 92	syl13anc 1370	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑅, 𝑥⟩ ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
94		3simpc 1148	. . . . . . . . . . . 12 ⊢ ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
95		simpl3r 1227	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → 𝑃 ≠ 𝑅)
96	95	necomd 2998	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → 𝑅 ≠ 𝑃)
97		simprrl 777	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → 𝑥 ≠ 𝑃)
98		simprrr 778	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))
99	96, 97, 98	3jca 1126	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
100	99	expr 456	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
101	94, 100	impbid2 225	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
102	93, 101	bitrd 278	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑅, 𝑥⟩ ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
103	91, 102	orbi12d 915	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
104	103	adantr 480	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
105	104	orbi2d 912	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑥 = 𝑃 ∨ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))))
106	80, 105	bitr4d 281	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 = 𝑃 ∨ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩))))
107		orcom 866	. . . . . . 7 ⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)) ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩) ∨ 𝑥 = 𝑃))
108		or32 922	. . . . . . 7 ⊢ (((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩) ∨ 𝑥 = 𝑃) ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩))
109	107, 108	bitri 274	. . . . . 6 ⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)) ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩))
110	106, 109	bitrdi 286	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)))
111	110	an32s 648	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)))
112	111	rabbidva 3402	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)})
113		simp1 1134	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑁 ∈ ℕ)
114		simp21 1204	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ∈ (𝔼‘𝑁))
115		simp22 1205	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑄 ∈ (𝔼‘𝑁))
116		simp3l 1199	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑄)
117		fvline2 34375	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
118	113, 114, 115, 116, 117	syl13anc 1370	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
119	118	adantr 480	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
120		fvray 34370	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩})
121	113, 114, 115, 116, 120	syl13anc 1370	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩})
122		rabsn 4654	. . . . . . . . 9 ⊢ (𝑃 ∈ (𝔼‘𝑁) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃})
123	114, 122	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃})
124	123	eqcomd 2744	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑃} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃})
125	121, 124	uneq12d 4094	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → ((𝑃Ray𝑄) ∪ {𝑃}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}))
126		simp23 1206	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑅 ∈ (𝔼‘𝑁))
127		simp3r 1200	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑅)
128		fvray 34370	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩})
129	113, 114, 126, 127, 128	syl13anc 1370	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩})
130	125, 129	uneq12d 4094	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}))
131	130	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}))
132		unrab 4236	. . . . . 6 ⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) = {𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃)}
133	132	uneq1i 4089	. . . . 5 ⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩})
134		unrab 4236	. . . . 5 ⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)}
135	133, 134	eqtri 2766	. . . 4 ⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)}
136	131, 135	eqtrdi 2795	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)})
137	112, 119, 136	3eqtr4d 2788	. 2 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)))
138	137	ex 412	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn ⟨𝑄, 𝑅⟩ → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∨ w3o 1084 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 {crab 3067 ∪ cun 3881 {csn 4558 ⟨cop 4564 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 ℕcn 11903 𝔼cee 27159 Btwn cbtwn 27160 Colinear ccolin 34266 OutsideOfcoutsideof 34348 Linecline2 34363 Raycray 34364

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-ec 8458 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-sum 15326 df-ee 27162 df-btwn 27163 df-cgr 27164 df-ofs 34212 df-colinear 34268 df-ifs 34269 df-cgr3 34270 df-fs 34271 df-outsideof 34349 df-line2 34366 df-ray 34367

This theorem is referenced by: (None)

W3C validator