lineelsb2

Description: If S lies on P Q , then P Q = P S . Theorem 6.16 of Schwabhauser p. 45. (Contributed by Scott Fenton, 27-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	lineelsb2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to (S \in (P Line Q) \to P Line Q = P Line S)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to N \in ℕ$
2		simpl3l	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to S \in 𝔼 (N)$
3		simpl21	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to P \in 𝔼 (N)$
4		simpl22	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to Q \in 𝔼 (N)$
5		brcolinear	$⊢ (N \in ℕ \land (S \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (S Colinear ⟨P, Q⟩ \leftrightarrow (S Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, S⟩ \lor Q Btwn ⟨S, P⟩))$
6	1 2 3 4 5	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (S Colinear ⟨P, Q⟩ \leftrightarrow (S Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, S⟩ \lor Q Btwn ⟨S, P⟩))$
7	6	biimpa	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Colinear ⟨P, Q⟩) \to (S Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, S⟩ \lor Q Btwn ⟨S, P⟩)$
8		simpr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
9		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⟩))$
10	1 8 3 4 9	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
11	10	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
12		btwnconn3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land S \in 𝔼 (N)) \land (x \in 𝔼 (N) \land Q \in 𝔼 (N))) \to ((S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, Q⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
13	1 3 2 8 4 12	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, Q⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
14	13	imp	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, Q⟩)) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩)$
15		btwncolinear3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land x \in 𝔼 (N) \land S \in 𝔼 (N))) \to (S Btwn ⟨P, x⟩ \to x Colinear ⟨P, S⟩)$
16	1 3 8 2 15	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (S Btwn ⟨P, x⟩ \to x Colinear ⟨P, S⟩)$
17		btwncolinear5	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land S \in 𝔼 (N) \land x \in 𝔼 (N))) \to (x Btwn ⟨P, S⟩ \to x Colinear ⟨P, S⟩)$
18	1 3 2 8 17	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (x Btwn ⟨P, S⟩ \to x Colinear ⟨P, S⟩)$
19	16 18	jaod	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩) \to x Colinear ⟨P, S⟩)$
20	19	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, Q⟩)) \to ((S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩) \to x Colinear ⟨P, S⟩)$
21	14 20	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, Q⟩)) \to x Colinear ⟨P, S⟩$
22	21	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, S⟩)$
23		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨Q, x⟩)) \to S Btwn ⟨P, Q⟩$
24	1 2 3 4 23	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨Q, x⟩)) \to S Btwn ⟨Q, P⟩$
25		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨Q, x⟩$
26	1 4 2 3 8 24 25	btwnexch3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨S, x⟩$
27		btwncolinear4	$⊢ (N \in ℕ \land (S \in 𝔼 (N) \land x \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, S⟩)$
28	1 2 8 3 27	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, S⟩)$
29	28	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨Q, x⟩)) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, S⟩)$
30	26 29	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨Q, x⟩)) \to x Colinear ⟨P, S⟩$
31	30	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, S⟩)$
32		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land Q Btwn ⟨x, P⟩)) \to S Btwn ⟨P, Q⟩$
33		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨x, P⟩$
34	1 4 8 3 33	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨P, x⟩$
35	1 3 2 4 8 32 34	btwnexchand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land Q Btwn ⟨x, P⟩)) \to S Btwn ⟨P, x⟩$
36	16	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land Q Btwn ⟨x, P⟩)) \to (S Btwn ⟨P, x⟩ \to x Colinear ⟨P, S⟩)$
37	35 36	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land Q Btwn ⟨x, P⟩)) \to x Colinear ⟨P, S⟩$
38	37	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (Q Btwn ⟨x, P⟩ \to x Colinear ⟨P, S⟩)$
39	22 31 38	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to ((x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩) \to x Colinear ⟨P, S⟩)$
40	11 39	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Colinear ⟨P, Q⟩ \to x Colinear ⟨P, S⟩)$
41		brcolinear	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land P \in 𝔼 (N) \land S \in 𝔼 (N))) \to (x Colinear ⟨P, S⟩ \leftrightarrow (x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩))$
42	1 8 3 2 41	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, S⟩ \leftrightarrow (x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩))$
43	42	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Colinear ⟨P, S⟩ \leftrightarrow (x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩))$
44		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, S⟩)) \to x Btwn ⟨P, S⟩$
45		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, S⟩)) \to S Btwn ⟨P, Q⟩$
46	1 3 8 2 4 44 45	btwnexchand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, S⟩)) \to x Btwn ⟨P, Q⟩$
47		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⟩)$
48	1 3 4 8 47	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, Q⟩)$
49	48	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, S⟩)) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, Q⟩)$
50	46 49	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land x Btwn ⟨P, S⟩)) \to x Colinear ⟨P, Q⟩$
51	50	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Btwn ⟨P, S⟩ \to x Colinear ⟨P, Q⟩)$
52		simpl3r	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to P \neq S$
53	52	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to S \neq P$
54	53	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to S \neq P$
55		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to S Btwn ⟨P, Q⟩$
56	1 2 3 4 55	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to S Btwn ⟨Q, P⟩$
57		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨S, x⟩$
58		btwnouttr2	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land S \in 𝔼 (N)) \land (P \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((S \neq P \land S Btwn ⟨Q, P⟩ \land P Btwn ⟨S, x⟩) \to P Btwn ⟨Q, x⟩)$
59	1 4 2 3 8 58	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((S \neq P \land S Btwn ⟨Q, P⟩ \land P Btwn ⟨S, x⟩) \to P Btwn ⟨Q, x⟩)$
60	59	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to ((S \neq P \land S Btwn ⟨Q, P⟩ \land P Btwn ⟨S, x⟩) \to P Btwn ⟨Q, x⟩)$
61	54 56 57 60	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨Q, x⟩$
62		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⟩)$
63	1 4 8 3 62	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
64	63	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
65	61 64	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land P Btwn ⟨S, x⟩)) \to x Colinear ⟨P, Q⟩$
66	65	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, Q⟩)$
67	52	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to P \neq S$
68		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨P, Q⟩$
69		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨x, P⟩$
70	1 2 8 3 69	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨P, x⟩$
71		btwnconn1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land S \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((P \neq S \land S Btwn ⟨P, Q⟩ \land S Btwn ⟨P, x⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
72	1 3 2 4 8 71	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((P \neq S \land S Btwn ⟨P, Q⟩ \land S Btwn ⟨P, x⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
73	72	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to ((P \neq S \land S Btwn ⟨P, Q⟩ \land S Btwn ⟨P, x⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
74	67 68 70 73	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)$
75		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⟩)$
76	1 3 8 4 75	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (Q Btwn ⟨P, x⟩ \to x Colinear ⟨P, Q⟩)$
77	76 48	jaod	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \to x Colinear ⟨P, Q⟩)$
78	77	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \to x Colinear ⟨P, Q⟩)$
79	74 78	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \land S Btwn ⟨x, P⟩)) \to x Colinear ⟨P, Q⟩$
80	79	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (S Btwn ⟨x, P⟩ \to x Colinear ⟨P, Q⟩)$
81	51 66 80	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to ((x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩) \to x Colinear ⟨P, Q⟩)$
82	43 81	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Colinear ⟨P, S⟩ \to x Colinear ⟨P, Q⟩)$
83	40 82	impbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Btwn ⟨P, Q⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
84	10	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
85		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, Q⟩)) \to x Btwn ⟨P, Q⟩$
86	1 8 3 4 85	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, Q⟩)) \to x Btwn ⟨Q, P⟩$
87		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, Q⟩)) \to P Btwn ⟨Q, S⟩$
88	1 4 8 3 2 86 87	btwnexch3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, Q⟩)) \to P Btwn ⟨x, S⟩$
89		btwncolinear2	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land S \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P Btwn ⟨x, S⟩ \to x Colinear ⟨P, S⟩)$
90	1 8 2 3 89	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (P Btwn ⟨x, S⟩ \to x Colinear ⟨P, S⟩)$
91	90	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, Q⟩)) \to (P Btwn ⟨x, S⟩ \to x Colinear ⟨P, S⟩)$
92	88 91	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, Q⟩)) \to x Colinear ⟨P, S⟩$
93	92	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, S⟩)$
94		simpl23	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to P \neq Q$
95	94	necomd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to Q \neq P$
96	95	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to Q \neq P$
97		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨Q, S⟩$
98		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨Q, x⟩$
99		btwnconn2	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N)) \land (S \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((Q \neq P \land P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
100	1 4 3 2 8 99	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((Q \neq P \land P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
101	100	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to ((Q \neq P \land P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
102	96 97 98 101	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩)$
103	19	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to ((S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩) \to x Colinear ⟨P, S⟩)$
104	102 103	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨Q, x⟩)) \to x Colinear ⟨P, S⟩$
105	104	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, S⟩)$
106	94	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to P \neq Q$
107		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to P Btwn ⟨Q, S⟩$
108	1 3 4 2 107	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to P Btwn ⟨S, Q⟩$
109		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨x, P⟩$
110	1 4 8 3 109	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨P, x⟩$
111		btwnouttr	$⊢ (N \in ℕ \land (S \in 𝔼 (N) \land P \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((P \neq Q \land P Btwn ⟨S, Q⟩ \land Q Btwn ⟨P, x⟩) \to P Btwn ⟨S, x⟩)$
112	1 2 3 4 8 111	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((P \neq Q \land P Btwn ⟨S, Q⟩ \land Q Btwn ⟨P, x⟩) \to P Btwn ⟨S, x⟩)$
113	112	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to ((P \neq Q \land P Btwn ⟨S, Q⟩ \land Q Btwn ⟨P, x⟩) \to P Btwn ⟨S, x⟩)$
114	106 108 110 113	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to P Btwn ⟨S, x⟩$
115	28	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, S⟩)$
116	114 115	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land Q Btwn ⟨x, P⟩)) \to x Colinear ⟨P, S⟩$
117	116	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (Q Btwn ⟨x, P⟩ \to x Colinear ⟨P, S⟩)$
118	93 105 117	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to ((x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩) \to x Colinear ⟨P, S⟩)$
119	84 118	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Colinear ⟨P, Q⟩ \to x Colinear ⟨P, S⟩)$
120	42	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Colinear ⟨P, S⟩ \leftrightarrow (x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩))$
121		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to x Btwn ⟨P, S⟩$
122	1 8 3 2 121	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to x Btwn ⟨S, P⟩$
123		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to P Btwn ⟨Q, S⟩$
124	1 3 4 2 123	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to P Btwn ⟨S, Q⟩$
125	1 2 8 3 4 122 124	btwnexch3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to P Btwn ⟨x, Q⟩$
126		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⟩)$
127	1 8 4 3 126	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to (P Btwn ⟨x, Q⟩ \to x Colinear ⟨P, Q⟩)$
128	127	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to (P Btwn ⟨x, Q⟩ \to x Colinear ⟨P, Q⟩)$
129	125 128	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land x Btwn ⟨P, S⟩)) \to x Colinear ⟨P, Q⟩$
130	129	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Btwn ⟨P, S⟩ \to x Colinear ⟨P, Q⟩)$
131	53	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to S \neq P$
132		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨Q, S⟩$
133	1 3 4 2 132	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨S, Q⟩$
134		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨S, x⟩$
135		btwnconn2	$⊢ (N \in ℕ \land (S \in 𝔼 (N) \land P \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((S \neq P \land P Btwn ⟨S, Q⟩ \land P Btwn ⟨S, x⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
136	1 2 3 4 8 135	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((S \neq P \land P Btwn ⟨S, Q⟩ \land P Btwn ⟨S, x⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
137	136	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to ((S \neq P \land P Btwn ⟨S, Q⟩ \land P Btwn ⟨S, x⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
138	131 133 134 137	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)$
139	77	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \to x Colinear ⟨P, Q⟩)$
140	138 139	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land P Btwn ⟨S, x⟩)) \to x Colinear ⟨P, Q⟩$
141	140	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, Q⟩)$
142	52	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to P \neq S$
143		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to P Btwn ⟨Q, S⟩$
144		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨x, P⟩$
145	1 2 8 3 144	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨P, x⟩$
146		btwnouttr	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N)) \land (S \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((P \neq S \land P Btwn ⟨Q, S⟩ \land S Btwn ⟨P, x⟩) \to P Btwn ⟨Q, x⟩)$
147	1 4 3 2 8 146	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((P \neq S \land P Btwn ⟨Q, S⟩ \land S Btwn ⟨P, x⟩) \to P Btwn ⟨Q, x⟩)$
148	147	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to ((P \neq S \land P Btwn ⟨Q, S⟩ \land S Btwn ⟨P, x⟩) \to P Btwn ⟨Q, x⟩)$
149	142 143 145 148	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to P Btwn ⟨Q, x⟩$
150	63	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
151	149 150	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (P Btwn ⟨Q, S⟩ \land S Btwn ⟨x, P⟩)) \to x Colinear ⟨P, Q⟩$
152	151	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (S Btwn ⟨x, P⟩ \to x Colinear ⟨P, Q⟩)$
153	130 141 152	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to ((x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩) \to x Colinear ⟨P, Q⟩)$
154	120 153	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Colinear ⟨P, S⟩ \to x Colinear ⟨P, Q⟩)$
155	119 154	impbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land P Btwn ⟨Q, S⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
156	10	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow (x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩))$
157		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, Q⟩)) \to x Btwn ⟨P, Q⟩$
158		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, Q⟩)) \to Q Btwn ⟨S, P⟩$
159	1 4 2 3 158	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, Q⟩)) \to Q Btwn ⟨P, S⟩$
160	1 3 8 4 2 157 159	btwnexchand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, Q⟩)) \to x Btwn ⟨P, S⟩$
161	18	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, Q⟩)) \to (x Btwn ⟨P, S⟩ \to x Colinear ⟨P, S⟩)$
162	160 161	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, Q⟩)) \to x Colinear ⟨P, S⟩$
163	162	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Btwn ⟨P, Q⟩ \to x Colinear ⟨P, S⟩)$
164	95	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to Q \neq P$
165		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to Q Btwn ⟨S, P⟩$
166		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨Q, x⟩$
167		btwnouttr2	$⊢ (N \in ℕ \land (S \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (P \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((Q \neq P \land Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩) \to P Btwn ⟨S, x⟩)$
168	1 2 4 3 8 167	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((Q \neq P \land Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩) \to P Btwn ⟨S, x⟩)$
169	168	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to ((Q \neq P \land Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩) \to P Btwn ⟨S, x⟩)$
170	164 165 166 169	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to P Btwn ⟨S, x⟩$
171	28	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, S⟩)$
172	170 171	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨Q, x⟩)) \to x Colinear ⟨P, S⟩$
173	172	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, S⟩)$
174	94	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to P \neq Q$
175		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨S, P⟩$
176	1 4 2 3 175	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨P, S⟩$
177		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨x, P⟩$
178	1 4 8 3 177	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to Q Btwn ⟨P, x⟩$
179		btwnconn1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (S \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((P \neq Q \land Q Btwn ⟨P, S⟩ \land Q Btwn ⟨P, x⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
180	1 3 4 2 8 179	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((P \neq Q \land Q Btwn ⟨P, S⟩ \land Q Btwn ⟨P, x⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
181	180	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to ((P \neq Q \land Q Btwn ⟨P, S⟩ \land Q Btwn ⟨P, x⟩) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩))$
182	174 176 178 181	mp3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to (S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩)$
183	19	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to ((S Btwn ⟨P, x⟩ \lor x Btwn ⟨P, S⟩) \to x Colinear ⟨P, S⟩)$
184	182 183	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land Q Btwn ⟨x, P⟩)) \to x Colinear ⟨P, S⟩$
185	184	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (Q Btwn ⟨x, P⟩ \to x Colinear ⟨P, S⟩)$
186	163 173 185	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to ((x Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, x⟩ \lor Q Btwn ⟨x, P⟩) \to x Colinear ⟨P, S⟩)$
187	156 186	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Colinear ⟨P, Q⟩ \to x Colinear ⟨P, S⟩)$
188	42	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Colinear ⟨P, S⟩ \leftrightarrow (x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩))$
189		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to Q Btwn ⟨S, P⟩$
190	1 4 2 3 189	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to Q Btwn ⟨P, S⟩$
191		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to x Btwn ⟨P, S⟩$
192		btwnconn3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (x \in 𝔼 (N) \land S \in 𝔼 (N))) \to ((Q Btwn ⟨P, S⟩ \land x Btwn ⟨P, S⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
193	1 3 4 8 2 192	syl122anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \to ((Q Btwn ⟨P, S⟩ \land x Btwn ⟨P, S⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
194	193	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to ((Q Btwn ⟨P, S⟩ \land x Btwn ⟨P, S⟩) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩))$
195	190 191 194	mp2and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to (Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩)$
196	77	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to ((Q Btwn ⟨P, x⟩ \lor x Btwn ⟨P, Q⟩) \to x Colinear ⟨P, Q⟩)$
197	195 196	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land x Btwn ⟨P, S⟩)) \to x Colinear ⟨P, Q⟩$
198	197	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Btwn ⟨P, S⟩ \to x Colinear ⟨P, Q⟩)$
199		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨S, x⟩)) \to Q Btwn ⟨S, P⟩$
200		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨S, x⟩$
201	1 2 4 3 8 199 200	btwnexch3and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨S, x⟩)) \to P Btwn ⟨Q, x⟩$
202	63	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨S, x⟩)) \to (P Btwn ⟨Q, x⟩ \to x Colinear ⟨P, Q⟩)$
203	201 202	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land P Btwn ⟨S, x⟩)) \to x Colinear ⟨P, Q⟩$
204	203	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (P Btwn ⟨S, x⟩ \to x Colinear ⟨P, Q⟩)$
205		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to Q Btwn ⟨S, P⟩$
206	1 4 2 3 205	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to Q Btwn ⟨P, S⟩$
207		simprr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨x, P⟩$
208	1 2 8 3 207	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to S Btwn ⟨P, x⟩$
209	1 3 4 2 8 206 208	btwnexchand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to Q Btwn ⟨P, x⟩$
210	76	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to (Q Btwn ⟨P, x⟩ \to x Colinear ⟨P, Q⟩)$
211	209 210	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (Q Btwn ⟨S, P⟩ \land S Btwn ⟨x, P⟩)) \to x Colinear ⟨P, Q⟩$
212	211	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (S Btwn ⟨x, P⟩ \to x Colinear ⟨P, Q⟩)$
213	198 204 212	3jaod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to ((x Btwn ⟨P, S⟩ \lor P Btwn ⟨S, x⟩ \lor S Btwn ⟨x, P⟩) \to x Colinear ⟨P, Q⟩)$
214	188 213	sylbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Colinear ⟨P, S⟩ \to x Colinear ⟨P, Q⟩)$
215	187 214	impbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land Q Btwn ⟨S, P⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
216	83 155 215	3jaodan	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S Btwn ⟨P, Q⟩ \lor P Btwn ⟨Q, S⟩ \lor Q Btwn ⟨S, P⟩)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
217	7 216	syldan	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land S Colinear ⟨P, Q⟩) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
218	217	adantrl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land x \in 𝔼 (N)) \land (S \in 𝔼 (N) \land S Colinear ⟨P, Q⟩)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
219	218	an32s	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land (S \in 𝔼 (N) \land S Colinear ⟨P, Q⟩)) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨P, S⟩)$
220	219	rabbidva	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \land (S \in 𝔼 (N) \land S Colinear ⟨P, Q⟩)) \to \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} = \{x \in 𝔼 (N) \| x Colinear ⟨P, S⟩\}$
221	220	ex	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to ((S \in 𝔼 (N) \land S Colinear ⟨P, Q⟩) \to \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} = \{x \in 𝔼 (N) \| x Colinear ⟨P, S⟩\})$
222		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⟩\}$
223	222	3adant3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to P Line Q = \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
224	223	eleq2d	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to (S \in (P Line Q) \leftrightarrow S \in \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\})$
225		breq1	$⊢ x = S \to (x Colinear ⟨P, Q⟩ \leftrightarrow S Colinear ⟨P, Q⟩)$
226	225	elrab	$⊢ S \in \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} \leftrightarrow (S \in 𝔼 (N) \land S Colinear ⟨P, Q⟩)$
227	224 226	syl6bb	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to (S \in (P Line Q) \leftrightarrow (S \in 𝔼 (N) \land S Colinear ⟨P, Q⟩))$
228		simp1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to N \in ℕ$
229		simp21	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to P \in 𝔼 (N)$
230		simp3l	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to S \in 𝔼 (N)$
231		simp3r	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to P \neq S$
232		fvline2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land S \in 𝔼 (N) \land P \neq S)) \to P Line S = \{x \in 𝔼 (N) \| x Colinear ⟨P, S⟩\}$
233	228 229 230 231 232	syl13anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to P Line S = \{x \in 𝔼 (N) \| x Colinear ⟨P, S⟩\}$
234	223 233	eqeq12d	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to (P Line Q = P Line S \leftrightarrow \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} = \{x \in 𝔼 (N) \| x Colinear ⟨P, S⟩\})$
235	221 227 234	3imtr4d	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land (S \in 𝔼 (N) \land P \neq S)) \to (S \in (P Line Q) \to P Line Q = P Line S)$

Metamath Proof Explorer

Theorem lineelsb2

Proof