Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
2 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
3 | | simpl21 1139 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) |
4 | | simpl22 1140 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁)) |
5 | | brcolinear 32166 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1328 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉))) |
7 | 6 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉))) |
8 | | olc 399 |
. . . . . . . . . . . . . 14
⊢ (𝑥 Btwn 〈𝑃, 𝑄〉 → (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) |
9 | 8 | orcd 407 |
. . . . . . . . . . . . 13
⊢ (𝑥 Btwn 〈𝑃, 𝑄〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Btwn 〈𝑃, 𝑄〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
11 | | simpl3l 1116 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄) |
12 | 11 | necomd 2849 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃) |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → 𝑄 ≠ 𝑃) |
14 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑅〉) |
15 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑥〉) |
16 | 13, 14, 15 | 3jca 1242 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → (𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) |
17 | | simpl23 1141 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑅 ∈ (𝔼‘𝑁)) |
18 | | btwnconn2 32209 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
19 | 1, 4, 3, 17, 2, 18 | syl122anc 1335 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
21 | 16, 20 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) |
22 | 21 | olcd 408 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
23 | 22 | expr 643 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑃 Btwn 〈𝑄, 𝑥〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
24 | | btwncom 32121 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑄 Btwn 〈𝑥, 𝑃〉 ↔ 𝑄 Btwn 〈𝑃, 𝑥〉)) |
25 | 1, 4, 2, 3, 24 | syl13anc 1328 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑥, 𝑃〉 ↔ 𝑄 Btwn 〈𝑃, 𝑥〉)) |
26 | | orc 400 |
. . . . . . . . . . . . . . 15
⊢ (𝑄 Btwn 〈𝑃, 𝑥〉 → (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) |
27 | 26 | orcd 407 |
. . . . . . . . . . . . . 14
⊢ (𝑄 Btwn 〈𝑃, 𝑥〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
28 | 25, 27 | syl6bi 243 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑥, 𝑃〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑄 Btwn 〈𝑥, 𝑃〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
30 | 10, 23, 29 | 3jaod 1392 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
31 | 7, 30 | sylbid 230 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
32 | | olc 399 |
. . . . . . . . . 10
⊢ (((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
33 | 31, 32 | syl6 35 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 → (𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
34 | | colineartriv1 32174 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) → 𝑃 Colinear 〈𝑃, 𝑄〉) |
35 | 1, 3, 4, 34 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 Colinear 〈𝑃, 𝑄〉) |
36 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑃 → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ 𝑃 Colinear 〈𝑃, 𝑄〉)) |
37 | 35, 36 | syl5ibrcom 237 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑃 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
38 | 37 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 = 𝑃 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
39 | | btwncolinear3 32178 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn 〈𝑃, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
40 | 1, 3, 2, 4, 39 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑃, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
41 | | btwncolinear5 32180 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn 〈𝑃, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
42 | 1, 3, 4, 2, 41 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝑃, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
43 | 40, 42 | jaod 395 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
44 | 43 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
45 | | simpl3r 1117 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑅) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑃 ≠ 𝑅) |
47 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑅〉) |
48 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑅 Btwn 〈𝑃, 𝑥〉) |
49 | 46, 47, 48 | 3jca 1242 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → (𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) |
50 | | btwnouttr 32131 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉) → 𝑃 Btwn 〈𝑄, 𝑥〉)) |
51 | 1, 4, 3, 17, 2, 50 | syl122anc 1335 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉) → 𝑃 Btwn 〈𝑄, 𝑥〉)) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉) → 𝑃 Btwn 〈𝑄, 𝑥〉)) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑥〉) |
54 | | btwncolinear4 32179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn 〈𝑄, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
55 | 1, 4, 2, 3, 54 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn 〈𝑄, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → (𝑃 Btwn 〈𝑄, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
57 | 53, 56 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑥 Colinear 〈𝑃, 𝑄〉) |
58 | 57 | expr 643 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
59 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Btwn 〈𝑃, 𝑅〉) |
60 | 1, 2, 3, 17, 59 | btwncomand 32122 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Btwn 〈𝑅, 𝑃〉) |
61 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑃 Btwn 〈𝑄, 𝑅〉) |
62 | 1, 3, 4, 17, 61 | btwncomand 32122 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑃 Btwn 〈𝑅, 𝑄〉) |
63 | 1, 17, 2, 3, 4, 60,
62 | btwnexch3and 32128 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑃 Btwn 〈𝑥, 𝑄〉) |
64 | | btwncolinear2 32177 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn 〈𝑥, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
65 | 1, 2, 4, 3, 64 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn 〈𝑥, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑃 Btwn 〈𝑥, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
67 | 63, 66 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Colinear 〈𝑃, 𝑄〉) |
68 | 67 | expr 643 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Btwn 〈𝑃, 𝑅〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
69 | 58, 68 | jaod 395 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
70 | 44, 69 | jaod 395 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
71 | 38, 70 | jaod 395 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
72 | 33, 71 | impbid 202 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
73 | | pm5.63 959 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ (𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
74 | | df-ne 2795 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ 𝑃 ↔ ¬ 𝑥 = 𝑃) |
75 | 74 | anbi1i 731 |
. . . . . . . . . . 11
⊢ ((𝑥 ≠ 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
76 | | andi 911 |
. . . . . . . . . . 11
⊢ ((𝑥 ≠ 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
77 | 75, 76 | bitr3i 266 |
. . . . . . . . . 10
⊢ ((¬
𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
78 | 77 | orbi2i 541 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
79 | 73, 78 | bitri 264 |
. . . . . . . 8
⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
80 | 72, 79 | syl6bb 276 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))))) |
81 | | broutsideof2 32229 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝑄, 𝑥〉 ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
82 | 1, 3, 4, 2, 81 | syl13anc 1328 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑄, 𝑥〉 ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
83 | | 3simpc 1060 |
. . . . . . . . . . . 12
⊢ ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) → (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉))) |
84 | | simpl3l 1116 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → 𝑃 ≠ 𝑄) |
85 | 84 | necomd 2849 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → 𝑄 ≠ 𝑃) |
86 | | simprrl 804 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → 𝑥 ≠ 𝑃) |
87 | | simprrr 805 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) |
88 | 85, 86, 87 | 3jca 1242 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉))) |
89 | 88 | expr 643 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
90 | 83, 89 | impbid2 216 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
91 | 82, 90 | bitrd 268 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑄, 𝑥〉 ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
92 | | broutsideof2 32229 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝑅, 𝑥〉 ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
93 | 1, 3, 17, 2, 92 | syl13anc 1328 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑅, 𝑥〉 ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
94 | | 3simpc 1060 |
. . . . . . . . . . . 12
⊢ ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
95 | | simpl3r 1117 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → 𝑃 ≠ 𝑅) |
96 | 95 | necomd 2849 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → 𝑅 ≠ 𝑃) |
97 | | simprrl 804 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → 𝑥 ≠ 𝑃) |
98 | | simprrr 805 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) |
99 | 96, 97, 98 | 3jca 1242 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
100 | 99 | expr 643 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
101 | 94, 100 | impbid2 216 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
102 | 93, 101 | bitrd 268 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑅, 𝑥〉 ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
103 | 91, 102 | orbi12d 746 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
104 | 103 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
105 | 104 | orbi2d 738 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))))) |
106 | 80, 105 | bitr4d 271 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)))) |
107 | | orcom 402 |
. . . . . . 7
⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ∨ 𝑥 = 𝑃)) |
108 | | or32 549 |
. . . . . . 7
⊢ (((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ∨ 𝑥 = 𝑃) ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) |
109 | 107, 108 | bitri 264 |
. . . . . 6
⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) |
110 | 106, 109 | syl6bb 276 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉))) |
111 | 110 | an32s 846 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉))) |
112 | 111 | rabbidva 3188 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)}) |
113 | | simp1 1061 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑁 ∈ ℕ) |
114 | | simp21 1094 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ∈ (𝔼‘𝑁)) |
115 | | simp22 1095 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑄 ∈ (𝔼‘𝑁)) |
116 | | simp3l 1089 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑄) |
117 | | fvline2 32253 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉}) |
118 | 113, 114,
115, 116, 117 | syl13anc 1328 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉}) |
119 | 118 | adantr 481 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉}) |
120 | | fvray 32248 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉}) |
121 | 113, 114,
115, 116, 120 | syl13anc 1328 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉}) |
122 | | rabsn 4256 |
. . . . . . . . 9
⊢ (𝑃 ∈ (𝔼‘𝑁) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃}) |
123 | 114, 122 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃}) |
124 | 123 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑃} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) |
125 | 121, 124 | uneq12d 3768 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → ((𝑃Ray𝑄) ∪ {𝑃}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃})) |
126 | | simp23 1096 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑅 ∈ (𝔼‘𝑁)) |
127 | | simp3r 1090 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑅) |
128 | | fvray 32248 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) |
129 | 113, 114,
126, 127, 128 | syl13anc 1328 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) |
130 | 125, 129 | uneq12d 3768 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉})) |
131 | 130 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉})) |
132 | | unrab 3898 |
. . . . . 6
⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) = {𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃)} |
133 | 132 | uneq1i 3763 |
. . . . 5
⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) |
134 | | unrab 3898 |
. . . . 5
⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)} |
135 | 133, 134 | eqtri 2644 |
. . . 4
⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)} |
136 | 131, 135 | syl6eq 2672 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)}) |
137 | 112, 119,
136 | 3eqtr4d 2666 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))) |
138 | 137 | ex 450 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn 〈𝑄, 𝑅〉 → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)))) |