Step | Hyp | Ref
| Expression |
1 | | simpl1 1193 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
2 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
3 | | simpl21 1253 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) |
4 | | simpl22 1254 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ∈ (𝔼‘𝑁)) |
5 | | brcolinear 34098 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉))) |
7 | 6 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉))) |
8 | | olc 868 |
. . . . . . . . . . . . . 14
⊢ (𝑥 Btwn 〈𝑃, 𝑄〉 → (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) |
9 | 8 | orcd 873 |
. . . . . . . . . . . . 13
⊢ (𝑥 Btwn 〈𝑃, 𝑄〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Btwn 〈𝑃, 𝑄〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
11 | | simpl3l 1230 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑄) |
12 | 11 | necomd 2996 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑄 ≠ 𝑃) |
13 | 12 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → 𝑄 ≠ 𝑃) |
14 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑅〉) |
15 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑥〉) |
16 | 13, 14, 15 | 3jca 1130 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → (𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) |
17 | | simpl23 1255 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑅 ∈ (𝔼‘𝑁)) |
18 | | btwnconn2 34141 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
19 | 1, 4, 3, 17, 2, 18 | syl122anc 1381 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
20 | 19 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → ((𝑄 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
21 | 16, 20 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) |
22 | 21 | olcd 874 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑃 Btwn 〈𝑄, 𝑥〉)) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
23 | 22 | expr 460 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑃 Btwn 〈𝑄, 𝑥〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
24 | | btwncom 34053 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑄 Btwn 〈𝑥, 𝑃〉 ↔ 𝑄 Btwn 〈𝑃, 𝑥〉)) |
25 | 1, 4, 2, 3, 24 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑥, 𝑃〉 ↔ 𝑄 Btwn 〈𝑃, 𝑥〉)) |
26 | | orc 867 |
. . . . . . . . . . . . . . 15
⊢ (𝑄 Btwn 〈𝑃, 𝑥〉 → (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) |
27 | 26 | orcd 873 |
. . . . . . . . . . . . . 14
⊢ (𝑄 Btwn 〈𝑃, 𝑥〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
28 | 25, 27 | syl6bi 256 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑥, 𝑃〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
29 | 28 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑄 Btwn 〈𝑥, 𝑃〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
30 | 10, 23, 29 | 3jaod 1430 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑥 Btwn 〈𝑃, 𝑄〉 ∨ 𝑃 Btwn 〈𝑄, 𝑥〉 ∨ 𝑄 Btwn 〈𝑥, 𝑃〉) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
31 | 7, 30 | sylbid 243 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
32 | | olc 868 |
. . . . . . . . . 10
⊢ (((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
33 | 31, 32 | syl6 35 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 → (𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
34 | | colineartriv1 34106 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) → 𝑃 Colinear 〈𝑃, 𝑄〉) |
35 | 1, 3, 4, 34 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 Colinear 〈𝑃, 𝑄〉) |
36 | | breq1 5056 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑃 → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ 𝑃 Colinear 〈𝑃, 𝑄〉)) |
37 | 35, 36 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑃 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
38 | 37 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 = 𝑃 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
39 | | btwncolinear3 34110 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁))) → (𝑄 Btwn 〈𝑃, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
40 | 1, 3, 2, 4, 39 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑃, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
41 | | btwncolinear5 34112 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑥 Btwn 〈𝑃, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
42 | 1, 3, 4, 2, 41 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝑃, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
43 | 40, 42 | jaod 859 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
44 | 43 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
45 | | simpl3r 1231 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑃 ≠ 𝑅) |
46 | 45 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑃 ≠ 𝑅) |
47 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑅〉) |
48 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑅 Btwn 〈𝑃, 𝑥〉) |
49 | 46, 47, 48 | 3jca 1130 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → (𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) |
50 | | btwnouttr 34063 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉) → 𝑃 Btwn 〈𝑄, 𝑥〉)) |
51 | 1, 4, 3, 17, 2, 50 | syl122anc 1381 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉) → 𝑃 Btwn 〈𝑄, 𝑥〉)) |
52 | 51 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → ((𝑃 ≠ 𝑅 ∧ 𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉) → 𝑃 Btwn 〈𝑄, 𝑥〉)) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑃 Btwn 〈𝑄, 𝑥〉) |
54 | | btwncolinear4 34111 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn 〈𝑄, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
55 | 1, 4, 2, 3, 54 | syl13anc 1374 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn 〈𝑄, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → (𝑃 Btwn 〈𝑄, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
57 | 53, 56 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑅 Btwn 〈𝑃, 𝑥〉)) → 𝑥 Colinear 〈𝑃, 𝑄〉) |
58 | 57 | expr 460 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑅 Btwn 〈𝑃, 𝑥〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
59 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Btwn 〈𝑃, 𝑅〉) |
60 | 1, 2, 3, 17, 59 | btwncomand 34054 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Btwn 〈𝑅, 𝑃〉) |
61 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑃 Btwn 〈𝑄, 𝑅〉) |
62 | 1, 3, 4, 17, 61 | btwncomand 34054 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑃 Btwn 〈𝑅, 𝑄〉) |
63 | 1, 17, 2, 3, 4, 60,
62 | btwnexch3and 34060 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑃 Btwn 〈𝑥, 𝑄〉) |
64 | | btwncolinear2 34109 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃 Btwn 〈𝑥, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
65 | 1, 2, 4, 3, 64 | syl13anc 1374 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃 Btwn 〈𝑥, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑃 Btwn 〈𝑥, 𝑄〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
67 | 63, 66 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∧ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Colinear 〈𝑃, 𝑄〉) |
68 | 67 | expr 460 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Btwn 〈𝑃, 𝑅〉 → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
69 | 58, 68 | jaod 859 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
70 | 44, 69 | jaod 859 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
71 | 38, 70 | jaod 859 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) → 𝑥 Colinear 〈𝑃, 𝑄〉)) |
72 | 33, 71 | impbid 215 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
73 | | pm5.63 1020 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ (𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
74 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ 𝑃 ↔ ¬ 𝑥 = 𝑃) |
75 | 74 | anbi1i 627 |
. . . . . . . . . . 11
⊢ ((𝑥 ≠ 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
76 | | andi 1008 |
. . . . . . . . . . 11
⊢ ((𝑥 ≠ 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
77 | 75, 76 | bitr3i 280 |
. . . . . . . . . 10
⊢ ((¬
𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
78 | 77 | orbi2i 913 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑃 ∨ (¬ 𝑥 = 𝑃 ∧ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
79 | 73, 78 | bitri 278 |
. . . . . . . 8
⊢ ((𝑥 = 𝑃 ∨ ((𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉) ∨ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
80 | 72, 79 | bitrdi 290 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))))) |
81 | | broutsideof2 34161 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝑄, 𝑥〉 ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
82 | 1, 3, 4, 2, 81 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑄, 𝑥〉 ↔ (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
83 | | 3simpc 1152 |
. . . . . . . . . . . 12
⊢ ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) → (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉))) |
84 | | simpl3l 1230 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → 𝑃 ≠ 𝑄) |
85 | 84 | necomd 2996 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → 𝑄 ≠ 𝑃) |
86 | | simprrl 781 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → 𝑥 ≠ 𝑃) |
87 | | simprrr 782 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) |
88 | 85, 86, 87 | 3jca 1130 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉))) |
89 | 88 | expr 460 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) → (𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
90 | 83, 89 | impbid2 229 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑄 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
91 | 82, 90 | bitrd 282 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑄, 𝑥〉 ↔ (𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)))) |
92 | | broutsideof2 34161 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝑅, 𝑥〉 ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
93 | 1, 3, 17, 2, 92 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑅, 𝑥〉 ↔ (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
94 | | 3simpc 1152 |
. . . . . . . . . . . 12
⊢ ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
95 | | simpl3r 1231 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → 𝑃 ≠ 𝑅) |
96 | 95 | necomd 2996 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → 𝑅 ≠ 𝑃) |
97 | | simprrl 781 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → 𝑥 ≠ 𝑃) |
98 | | simprrr 782 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) |
99 | 96, 97, 98 | 3jca 1130 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))) |
100 | 99 | expr 460 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) → (𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
101 | 94, 100 | impbid2 229 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑅 ≠ 𝑃 ∧ 𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)) ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
102 | 93, 101 | bitrd 282 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑃OutsideOf〈𝑅, 𝑥〉 ↔ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))) |
103 | 91, 102 | orbi12d 919 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
104 | 103 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ↔ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉))))) |
105 | 104 | orbi2d 916 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → ((𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) ↔ (𝑥 = 𝑃 ∨ ((𝑥 ≠ 𝑃 ∧ (𝑄 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑄〉)) ∨ (𝑥 ≠ 𝑃 ∧ (𝑅 Btwn 〈𝑃, 𝑥〉 ∨ 𝑥 Btwn 〈𝑃, 𝑅〉)))))) |
106 | 80, 105 | bitr4d 285 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ (𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)))) |
107 | | orcom 870 |
. . . . . . 7
⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ∨ 𝑥 = 𝑃)) |
108 | | or32 926 |
. . . . . . 7
⊢ (((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉) ∨ 𝑥 = 𝑃) ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) |
109 | 107, 108 | bitri 278 |
. . . . . 6
⊢ ((𝑥 = 𝑃 ∨ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)) |
110 | 106, 109 | bitrdi 290 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉))) |
111 | 110 | an32s 652 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Colinear 〈𝑃, 𝑄〉 ↔ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉))) |
112 | 111 | rabbidva 3388 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)}) |
113 | | simp1 1138 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑁 ∈ ℕ) |
114 | | simp21 1208 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ∈ (𝔼‘𝑁)) |
115 | | simp22 1209 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑄 ∈ (𝔼‘𝑁)) |
116 | | simp3l 1203 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑄) |
117 | | fvline2 34185 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉}) |
118 | 113, 114,
115, 116, 117 | syl13anc 1374 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉}) |
119 | 118 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑃Line𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝑃, 𝑄〉}) |
120 | | fvray 34180 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉}) |
121 | 113, 114,
115, 116, 120 | syl13anc 1374 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑄) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉}) |
122 | | rabsn 4637 |
. . . . . . . . 9
⊢ (𝑃 ∈ (𝔼‘𝑁) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃}) |
123 | 114, 122 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃} = {𝑃}) |
124 | 123 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → {𝑃} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) |
125 | 121, 124 | uneq12d 4078 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → ((𝑃Ray𝑄) ∪ {𝑃}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃})) |
126 | | simp23 1210 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑅 ∈ (𝔼‘𝑁)) |
127 | | simp3r 1204 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → 𝑃 ≠ 𝑅) |
128 | | fvray 34180 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) |
129 | 113, 114,
126, 127, 128 | syl13anc 1374 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃Ray𝑅) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) |
130 | 125, 129 | uneq12d 4078 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉})) |
131 | 130 | adantr 484 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉})) |
132 | | unrab 4220 |
. . . . . 6
⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) = {𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃)} |
133 | 132 | uneq1i 4073 |
. . . . 5
⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) = ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) |
134 | | unrab 4220 |
. . . . 5
⊢ ({𝑥 ∈ (𝔼‘𝑁) ∣ (𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃)} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)} |
135 | 133, 134 | eqtri 2765 |
. . . 4
⊢ (({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑄, 𝑥〉} ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 = 𝑃}) ∪ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝑅, 𝑥〉}) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)} |
136 | 131, 135 | eqtrdi 2794 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)) = {𝑥 ∈ (𝔼‘𝑁) ∣ ((𝑃OutsideOf〈𝑄, 𝑥〉 ∨ 𝑥 = 𝑃) ∨ 𝑃OutsideOf〈𝑅, 𝑥〉)}) |
137 | 112, 119,
136 | 3eqtr4d 2787 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) ∧ 𝑃 Btwn 〈𝑄, 𝑅〉) → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))) |
138 | 137 | ex 416 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn 〈𝑄, 𝑅〉 → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)))) |