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