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