Metamath Proof Explorer

Theorem 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 ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅 ) ) → ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ → ( 𝑃 Line 𝑄 ) = ( ( ( 𝑃 Ray 𝑄 ) ∪ { 𝑃 } ) ∪ ( 𝑃 Ray 𝑅 ) ) ) )

Proof

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