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 33615

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 1187	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
2		simpr 487	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
3		simpl21 1247	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
4		simpl22 1248	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁))
5		brcolinear 33527	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
6	1, 2, 3, 4, 5	syl13anc 1368	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩)))
7	6	adantr 483	. . . . . . . . . . 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 1224	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄)
12	11	necomd 3071	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃)
13	12	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑄 ≠ 𝑃)
14		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑅⟩)
15		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
16	13, 14, 15	3jca 1124	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩)) → (𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩))
17		simpl23 1249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑅 ∈ (𝔼‘𝑁))
18		btwnconn2 33570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
19	1, 4, 3, 17, 2, 18	syl122anc 1375	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑃 Btwn ⟨𝑄, 𝑥⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
20	19	adantr 483	. . . . . . . . . . . . . . 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 459	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
24		btwncom 33482	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ ↔ 𝑄 Btwn ⟨𝑃, 𝑥⟩))
25	1, 4, 2, 3, 24	syl13anc 1368	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ ↔ 𝑄 Btwn ⟨𝑃, 𝑥⟩))
26		orc 863	. . . . . . . . . . . . . . 15 ⊢ (𝑄 Btwn ⟨𝑃, 𝑥⟩ → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
27	26	orcd 869	. . . . . . . . . . . . . 14 ⊢ (𝑄 Btwn ⟨𝑃, 𝑥⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
28	25, 27	syl6bi 255	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
29	28	adantr 483	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑄 Btwn ⟨𝑥, 𝑃⟩ → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
30	10, 23, 29	3jaod 1424	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑥 Btwn ⟨𝑃, 𝑄⟩ ∨ 𝑃 Btwn ⟨𝑄, 𝑥⟩ ∨ 𝑄 Btwn ⟨𝑥, 𝑃⟩) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
31	7, 30	sylbid 242	. . . . . . . . . 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 33535	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) → 𝑃 Colinear ⟨𝑃, 𝑄⟩)
35	1, 3, 4, 34	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 Colinear ⟨𝑃, 𝑄⟩)
36		breq1 5055	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑃 → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ 𝑃 Colinear ⟨𝑃, 𝑄⟩))
37	35, 36	syl5ibrcom 249	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑃 → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
38	37	adantr 483	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 = 𝑃 → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
39		btwncolinear3 33539	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
40	1, 3, 2, 4, 39	syl13anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
41		btwncolinear5 33541	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
42	1, 3, 4, 2, 41	syl13anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑃, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
43	40, 42	jaod 855	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
44	43	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
45		simpl3r 1225	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑅)
46	45	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑃 ≠ 𝑅)
47		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑅⟩)
48		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑅 Btwn ⟨𝑃, 𝑥⟩)
49	46, 47, 48	3jca 1124	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → (𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩))
50		btwnouttr 33492	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
51	1, 4, 3, 17, 2, 50	syl122anc 1375	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
52	51	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩) → 𝑃 Btwn ⟨𝑄, 𝑥⟩))
53	49, 52	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑃 Btwn ⟨𝑄, 𝑥⟩)
54		btwncolinear4 33540	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
55	1, 4, 2, 3, 54	syl13anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
56	55	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → (𝑃 Btwn ⟨𝑄, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
57	53, 56	mpd 15	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑅 Btwn ⟨𝑃, 𝑥⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
58	57	expr 459	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
59		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Btwn ⟨𝑃, 𝑅⟩)
60	1, 2, 3, 17, 59	btwncomand 33483	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Btwn ⟨𝑅, 𝑃⟩)
61		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑃 Btwn ⟨𝑄, 𝑅⟩)
62	1, 3, 4, 17, 61	btwncomand 33483	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑃 Btwn ⟨𝑅, 𝑄⟩)
63	1, 17, 2, 3, 4, 60, 62	btwnexch3and 33489	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑃 Btwn ⟨𝑥, 𝑄⟩)
64		btwncolinear2 33538	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
65	1, 2, 4, 3, 64	syl13anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
66	65	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑃 Btwn ⟨𝑥, 𝑄⟩ → 𝑥 Colinear ⟨𝑃, 𝑄⟩))
67	63, 66	mpd 15	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∧ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → 𝑥 Colinear ⟨𝑃, 𝑄⟩)
68	67	expr 459	. . . . . . . . . . . 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 214	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
73		pm5.63 1016	. . . . . . . . 9 ⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ (𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
74		df-ne 3017	. . . . . . . . . . . 12 ⊢ (𝑥 ≠ 𝑃 ↔ ¬ 𝑥 = 𝑃)
75	74	anbi1i 625	. . . . . . . . . . 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 279	. . . . . . . . . 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 277	. . . . . . . 8 ⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩) ∨ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
80	72, 79	syl6bb 289	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))))
81		broutsideof2 33590	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝑄, 𝑥⟩ ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
82	1, 3, 4, 2, 81	syl13anc 1368	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑄, 𝑥⟩ ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
83		3simpc 1146	. . . . . . . . . . . 12 ⊢ ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
84		simpl3l 1224	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → 𝑃 ≠ 𝑄)
85	84	necomd 3071	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → 𝑄 ≠ 𝑃)
86		simprrl 779	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → 𝑥 ≠ 𝑃)
87		simprrr 780	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))
88	85, 86, 87	3jca 1124	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)))
89	88	expr 459	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
90	83, 89	impbid2 228	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
91	82, 90	bitrd 281	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑄, 𝑥⟩ ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩))))
92		broutsideof2 33590	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝑅, 𝑥⟩ ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
93	1, 3, 17, 2, 92	syl13anc 1368	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑅, 𝑥⟩ ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
94		3simpc 1146	. . . . . . . . . . . 12 ⊢ ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
95		simpl3r 1225	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → 𝑃 ≠ 𝑅)
96	95	necomd 3071	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → 𝑅 ≠ 𝑃)
97		simprrl 779	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → 𝑥 ≠ 𝑃)
98		simprrr 780	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))
99	96, 97, 98	3jca 1124	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))
100	99	expr 459	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
101	94, 100	impbid2 228	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
102	93, 101	bitrd 281	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf⟨𝑅, 𝑥⟩ ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))
103	91, 102	orbi12d 915	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
104	103	adantr 483	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩)))))
105	104	orbi2d 912	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → ((𝑥 = 𝑃 ∨ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑄⟩)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn ⟨𝑃, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑃, 𝑅⟩))))))
106	80, 105	bitr4d 284	. . . . . 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 277	. . . . . 6 ⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)) ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩))
110	106, 109	syl6bb 289	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)))
111	110	an32s 650	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear ⟨𝑃, 𝑄⟩ ↔ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)))
112	111	rabbidva 3470	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)})
113		simp1 1132	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑁 ∈ ℕ)
114		simp21 1202	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ∈ (𝔼‘𝑁))
115		simp22 1203	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑄 ∈ (𝔼‘𝑁))
116		simp3l 1197	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑄)
117		fvline2 33614	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
118	113, 114, 115, 116, 117	syl13anc 1368	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
119	118	adantr 483	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝑃, 𝑄⟩})
120		fvray 33609	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩})
121	113, 114, 115, 116, 120	syl13anc 1368	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩})
122		rabsn 4643	. . . . . . . . 9 ⊢ (𝑃 ∈ (𝔼‘𝑁) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃})
123	114, 122	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃})
124	123	eqcomd 2827	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑃} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃})
125	121, 124	uneq12d 4128	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → ((𝑃Ray𝑄) ∪ {𝑃}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}))
126		simp23 1204	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑅 ∈ (𝔼‘𝑁))
127		simp3r 1198	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑅)
128		fvray 33609	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩})
129	113, 114, 126, 127, 128	syl13anc 1368	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩})
130	125, 129	uneq12d 4128	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}))
131	130	adantr 483	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}))
132		unrab 4262	. . . . . 6 ⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) = {𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃)}
133	132	uneq1i 4123	. . . . 5 ⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩})
134		unrab 4262	. . . . 5 ⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)}
135	133, 134	eqtri 2844	. . . 4 ⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑄, 𝑥⟩} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝑅, 𝑥⟩}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)}
136	131, 135	syl6eq 2872	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf⟨𝑄, 𝑥⟩ ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf⟨𝑅, 𝑥⟩)})
137	112, 119, 136	3eqtr4d 2866	. 2 ⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn ⟨𝑄, 𝑅⟩) → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)))
138	137	ex 415	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn ⟨𝑄, 𝑅⟩ → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∨ w3o 1082 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 {crab 3142 ∪ cun 3922 {csn 4553 ⟨cop 4559 class class class wbr 5052 ‘cfv 6341 (class class class)co 7142 ℕcn 11624 𝔼cee 26660 Btwn cbtwn 26661 Colinear ccolin 33505 OutsideOfcoutsideof 33587 Linecline2 33602 Raycray 33603

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5176 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-inf2 9090 ax-cnex 10579 ax-resscn 10580 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-mulcom 10587 ax-addass 10588 ax-mulass 10589 ax-distr 10590 ax-i2m1 10591 ax-1ne0 10592 ax-1rid 10593 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 ax-pre-lttri 10597 ax-pre-lttrn 10598 ax-pre-ltadd 10599 ax-pre-mulgt0 10600 ax-pre-sup 10601

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-pss 3942 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-tp 4558 df-op 4560 df-uni 4825 df-int 4863 df-iun 4907 df-br 5053 df-opab 5115 df-mpt 5133 df-tr 5159 df-id 5446 df-eprel 5451 df-po 5460 df-so 5461 df-fr 5500 df-se 5501 df-we 5502 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-pred 6134 df-ord 6180 df-on 6181 df-lim 6182 df-suc 6183 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-isom 6350 df-riota 7100 df-ov 7145 df-oprab 7146 df-mpo 7147 df-om 7567 df-1st 7675 df-2nd 7676 df-wrecs 7933 df-recs 7994 df-rdg 8032 df-1o 8088 df-oadd 8092 df-er 8275 df-ec 8277 df-map 8394 df-en 8496 df-dom 8497 df-sdom 8498 df-fin 8499 df-sup 8892 df-oi 8960 df-card 9354 df-pnf 10663 df-mnf 10664 df-xr 10665 df-ltxr 10666 df-le 10667 df-sub 10858 df-neg 10859 df-div 11284 df-nn 11625 df-2 11687 df-3 11688 df-n0 11885 df-z 11969 df-uz 12231 df-rp 12377 df-ico 12731 df-icc 12732 df-fz 12883 df-fzo 13024 df-seq 13360 df-exp 13420 df-hash 13681 df-cj 14443 df-re 14444 df-im 14445 df-sqrt 14579 df-abs 14580 df-clim 14830 df-sum 15028 df-ee 26663 df-btwn 26664 df-cgr 26665 df-ofs 33451 df-colinear 33507 df-ifs 33508 df-cgr3 33509 df-fs 33510 df-outsideof 33588 df-line2 33605 df-ray 33606

This theorem is referenced by: (None)

W3C validator