lineunray

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)

		Ref	Expression
	Assertion	lineunray	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to (P Btwn ⟨Q, R⟩ \to P Line Q = ((P Ray Q) \cup \{P\}) \cup (P Ray R))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to N \in ℕ$
2		simpr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
3		simpl21	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to P \in 𝔼 (N)$
4		simpl22	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to Q \in 𝔼 (N)$
5		brcolinear	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
6	1 2 3 4 5	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
7	6	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
8		olc	$⊢ x Btwn ⟨P, Q⟩ \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)$
9	8	orcd	$⊢ x Btwn ⟨P, Q⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
10	9	a1i	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Btwn ⟨P, Q⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
11		simpl3l	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to P \neq Q$
12	11	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to Q \neq P$
13	12	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to Q \neq P$
14		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨Q, R⟩$
15		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨Q, x⟩$
16	13 14 15	3jca	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to (Q \neq P \land P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)$
17		simpl23	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to R \in 𝔼 (N)$
18		btwnconn2	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N)) \land (R \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((Q \neq P \land P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩) \to (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
19	1 4 3 17 2 18	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((Q \neq P \land P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩) \to (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
20	19	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to ((Q \neq P \land P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩) \to (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
21	16 20	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)$
22	21	olcd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land P Btwn ⟨Q, x⟩)) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
23	22	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (P Btwn ⟨Q, x⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
24		btwncom	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land x \in 𝔼 (N) \land P \in 𝔼 (N))) \to (Q Btwn ⟨x, P⟩ \leftrightarrow Q Btwn ⟨P, x⟩)$
25	1 4 2 3 24	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (Q Btwn ⟨x, P⟩ \leftrightarrow Q Btwn ⟨P, x⟩)$
26		orc	$⊢ Q Btwn ⟨P, x⟩ \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)$
27	26	orcd	$⊢ Q Btwn ⟨P, x⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
28	25 27	biimtrdi	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (Q Btwn ⟨x, P⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
29	28	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (Q Btwn ⟨x, P⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
30	10 23 29	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to ((x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
31	7 30	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
32		olc	$⊢ ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)) \to (x = P \lor ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
33	31 32	syl6	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \to (x = P \lor ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
34		colineartriv1	$⊢ (N \in ℕ \land P \in 𝔼 (N) \land Q \in 𝔼 (N)) \to P Colinear ⟨P, Q⟩$
35	1 3 4 34	syl3anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to P Colinear ⟨P, Q⟩$
36		breq1	$⊢ x = P \to (x Colinear ⟨P, Q⟩ \leftrightarrow P Colinear ⟨P, Q⟩)$
37	35 36	syl5ibrcom	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (x = P \to x Colinear ⟨P, Q⟩)$
38	37	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x = P \to x Colinear ⟨P, Q⟩)$
39		btwncolinear3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land x \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (Q Btwn ⟨P, x⟩ \to x Colinear ⟨P, Q⟩)$
40	1 3 2 4 39	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (Q Btwn ⟨P, x⟩ \to x Colinear ⟨P, Q⟩)$
41		btwncolinear5	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land x \in 𝔼 (N))) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, Q⟩)$
42	1 3 4 2 41	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, Q⟩)$
43	40 42	jaod	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \to x Colinear ⟨P, Q⟩)$
44	43	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \to x Colinear ⟨P, Q⟩)$
45		simpl3r	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to P \neq R$
46	45	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to P \neq R$
47		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to P Btwn ⟨Q, R⟩$
48		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to R Btwn ⟨P, x⟩$
49	46 47 48	3jca	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to (P \neq R \land P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)$
50		btwnouttr	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N)) \land (R \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((P \neq R \land P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩) \to P Btwn ⟨Q, x⟩)$
51	1 4 3 17 2 50	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((P \neq R \land P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩) \to P Btwn ⟨Q, x⟩)$
52	51	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to ((P \neq R \land P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩) \to P Btwn ⟨Q, x⟩)$
53	49 52	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to P Btwn ⟨Q, x⟩$
54		btwncolinear4	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land x \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
55	1 4 2 3 54	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
56	55	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
57	53 56	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land R Btwn ⟨P, x⟩)) \to x Colinear ⟨P, Q⟩$
58	57	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (R Btwn ⟨P, x⟩ \to x Colinear ⟨P, Q⟩)$
59		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to x Btwn ⟨P, R⟩$
60	1 2 3 17 59	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to x Btwn ⟨R, P⟩$
61		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to P Btwn ⟨Q, R⟩$
62	1 3 4 17 61	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to P Btwn ⟨R, Q⟩$
63	1 17 2 3 4 60 62	btwnexch3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to P Btwn ⟨x, Q⟩$
64		btwncolinear2	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P Btwn ⟨x, Q⟩ \to x Colinear ⟨P, Q⟩)$
65	1 2 4 3 64	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (P Btwn ⟨x, Q⟩ \to x Colinear ⟨P, Q⟩)$
66	65	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to (P Btwn ⟨x, Q⟩ \to x Colinear ⟨P, Q⟩)$
67	63 66	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, R⟩ \land x Btwn ⟨P, R⟩)) \to x Colinear ⟨P, Q⟩$
68	67	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Btwn ⟨P, R⟩ \to x Colinear ⟨P, Q⟩)$
69	58 68	jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to ((R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩) \to x Colinear ⟨P, Q⟩)$
70	44 69	jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)) \to x Colinear ⟨P, Q⟩)$
71	38 70	jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to ((x = P \lor ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))) \to x Colinear ⟨P, Q⟩)$
72	33 71	impbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x = P \lor ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
73		pm5.63	$⊢ (x = P \lor ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))) \leftrightarrow (x = P \lor (\neg x = P \land ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
74		df-ne	$⊢ x \neq P \leftrightarrow \neg x = P$
75	74	anbi1i	$⊢ (x \neq P \land ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))) \leftrightarrow (\neg x = P \land ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
76		andi	$⊢ (x \neq P \land ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))) \leftrightarrow ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
77	75 76	bitr3i	$⊢ (\neg x = P \land ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))) \leftrightarrow ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
78	77	orbi2i	$⊢ (x = P \lor (\neg x = P \land ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))) \leftrightarrow (x = P \lor ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
79	73 78	bitri	$⊢ (x = P \lor ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \lor (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))) \leftrightarrow (x = P \lor ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
80	72 79	bitrdi	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x = P \lor ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))))$
81		broutsideof2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land x \in 𝔼 (N))) \to (P OutsideOf ⟨Q, x⟩ \leftrightarrow (Q \neq P \land x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))$
82	1 3 4 2 81	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (P OutsideOf ⟨Q, x⟩ \leftrightarrow (Q \neq P \land x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))$
83		3simpc	$⊢ (Q \neq P \land x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \to (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
84		simpl3l	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))) \to P \neq Q$
85	84	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))) \to Q \neq P$
86		simprrl	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))) \to x \neq P$
87		simprrr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)$
88	85 86 87	3jca	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))) \to (Q \neq P \land x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
89	88	expr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \to (Q \neq P \land x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))$
90	83 89	impbid2	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((Q \neq P \land x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \leftrightarrow (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))$
91	82 90	bitrd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (P OutsideOf ⟨Q, x⟩ \leftrightarrow (x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)))$
92		broutsideof2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land R \in 𝔼 (N) \land x \in 𝔼 (N))) \to (P OutsideOf ⟨R, x⟩ \leftrightarrow (R \neq P \land x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
93	1 3 17 2 92	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (P OutsideOf ⟨R, x⟩ \leftrightarrow (R \neq P \land x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
94		3simpc	$⊢ (R \neq P \land x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)) \to (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
95		simpl3r	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))) \to P \neq R$
96	95	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))) \to R \neq P$
97		simprrl	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))) \to x \neq P$
98		simprrr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))) \to (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)$
99	96 97 98	3jca	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land (x \in 𝔼 (N) \land (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))) \to (R \neq P \land x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))$
100	99	expr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)) \to (R \neq P \land x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
101	94 100	impbid2	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((R \neq P \land x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)) \leftrightarrow (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
102	93 101	bitrd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to (P OutsideOf ⟨R, x⟩ \leftrightarrow (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))$
103	91 102	orbi12d	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \to ((P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩) \leftrightarrow ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
104	103	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to ((P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩) \leftrightarrow ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩))))$
105	104	orbi2d	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to ((x = P \lor (P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩)) \leftrightarrow (x = P \lor ((x \neq P \land (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)) \lor (x \neq P \land (R Btwn ⟨P, x⟩ \lor x Btwn ⟨P, R⟩)))))$
106	80 105	bitr4d	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x = P \lor (P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩)))$
107		orcom	$⊢ (x = P \lor (P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩)) \leftrightarrow ((P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩) \lor x = P)$
108		or32	$⊢ ((P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩) \lor x = P) \leftrightarrow ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩)$
109	107 108	bitri	$⊢ (x = P \lor (P OutsideOf ⟨Q, x⟩ \lor P OutsideOf ⟨R, x⟩)) \leftrightarrow ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩)$
110	106 109	bitrdi	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, R⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩))$
111	110	an32s	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land P Btwn ⟨Q, R⟩) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩))$
112	111	rabbidva	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land P Btwn ⟨Q, R⟩) \to \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} = \{x \in 𝔼 (N) \| ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩)\}$
113		simp1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to N \in ℕ$
114		simp21	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to P \in 𝔼 (N)$
115		simp22	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to Q \in 𝔼 (N)$
116		simp3l	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to P \neq Q$
117		fvline2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q = \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
118	113 114 115 116 117	syl13anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to P Line Q = \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
119	118	adantr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land P Btwn ⟨Q, R⟩) \to P Line Q = \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
120		fvray	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Ray Q = \{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\}$
121	113 114 115 116 120	syl13anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to P Ray Q = \{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\}$
122		rabsn	$⊢ P \in 𝔼 (N) \to \{x \in 𝔼 (N) \| x = P\} = \{P\}$
123	114 122	syl	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to \{x \in 𝔼 (N) \| x = P\} = \{P\}$
124	123	eqcomd	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to \{P\} = \{x \in 𝔼 (N) \| x = P\}$
125	121 124	uneq12d	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to (P Ray Q) \cup \{P\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\} \cup \{x \in 𝔼 (N) \| x = P\}$
126		simp23	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to R \in 𝔼 (N)$
127		simp3r	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to P \neq R$
128		fvray	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land R \in 𝔼 (N) \land P \neq R)) \to P Ray R = \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\}$
129	113 114 126 127 128	syl13anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to P Ray R = \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\}$
130	125 129	uneq12d	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to ((P Ray Q) \cup \{P\}) \cup (P Ray R) = (\{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\} \cup \{x \in 𝔼 (N) \| x = P\}) \cup \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\}$
131	130	adantr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land P Btwn ⟨Q, R⟩) \to ((P Ray Q) \cup \{P\}) \cup (P Ray R) = (\{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\} \cup \{x \in 𝔼 (N) \| x = P\}) \cup \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\}$
132		unrab	$⊢ \{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\} \cup \{x \in 𝔼 (N) \| x = P\} = \{x \in 𝔼 (N) \| (P OutsideOf ⟨Q, x⟩ \lor x = P)\}$
133	132	uneq1i	$⊢ (\{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\} \cup \{x \in 𝔼 (N) \| x = P\}) \cup \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\} = \{x \in 𝔼 (N) \| (P OutsideOf ⟨Q, x⟩ \lor x = P)\} \cup \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\}$
134		unrab	$⊢ \{x \in 𝔼 (N) \| (P OutsideOf ⟨Q, x⟩ \lor x = P)\} \cup \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\} = \{x \in 𝔼 (N) \| ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩)\}$
135	133 134	eqtri	$⊢ (\{x \in 𝔼 (N) \| P OutsideOf ⟨Q, x⟩\} \cup \{x \in 𝔼 (N) \| x = P\}) \cup \{x \in 𝔼 (N) \| P OutsideOf ⟨R, x⟩\} = \{x \in 𝔼 (N) \| ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩)\}$
136	131 135	eqtrdi	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land P Btwn ⟨Q, R⟩) \to ((P Ray Q) \cup \{P\}) \cup (P Ray R) = \{x \in 𝔼 (N) \| ((P OutsideOf ⟨Q, x⟩ \lor x = P) \lor P OutsideOf ⟨R, x⟩)\}$
137	112 119 136	3eqtr4d	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \land P Btwn ⟨Q, R⟩) \to P Line Q = ((P Ray Q) \cup \{P\}) \cup (P Ray R)$
138	137	ex	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N)) \land (P \neq Q \land P \neq R)) \to (P Btwn ⟨Q, R⟩ \to P Line Q = ((P Ray Q) \cup \{P\}) \cup (P Ray R))$

Metamath Proof Explorer

Theorem lineunray

Proof