Proof of Theorem outsideoftr
Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → 𝐴 ≠ 𝑃) |
2 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → 𝐵 ≠ 𝑃) |
3 | | simprr 773 |
. . . . 5
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → 𝐶 ≠ 𝑃) |
4 | 1, 2, 3 | 3jca 1130 |
. . . 4
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) |
5 | | simplr1 1217 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → 𝐴 ≠ 𝑃) |
6 | | simplr3 1219 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → 𝐶 ≠ 𝑃) |
7 | | df-3an 1091 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) |
8 | | simp1 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
9 | | simp3r 1204 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝑃 ∈ (𝔼‘𝑁)) |
10 | | simp2l 1201 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
11 | | simp2r 1202 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
12 | | simp3l 1203 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
13 | | simpr2 1197 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
14 | | simpr3 1198 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝑃, 𝐶〉) |
15 | 8, 9, 10, 11, 12, 13, 14 | btwnexchand 34065 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐴 Btwn 〈𝑃, 𝐶〉) |
16 | 15 | orcd 873 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
17 | 7, 16 | sylan2br 598 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
18 | 17 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → (𝐵 Btwn 〈𝑃, 𝐶〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
19 | | simprlr 780 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
20 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐶 Btwn 〈𝑃, 𝐵〉) |
21 | | btwnconn3 34142 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
22 | 8, 9, 10, 12, 11, 21 | syl122anc 1381 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
23 | 22 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
24 | 19, 20, 23 | mp2and 699 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
25 | 24 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → (𝐶 Btwn 〈𝑃, 𝐵〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
26 | 18, 25 | jaod 859 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
27 | 26 | expr 460 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (𝐴 Btwn 〈𝑃, 𝐵〉 → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
28 | | simpll2 1215 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → 𝐵 ≠ 𝑃) |
29 | 28 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 ≠ 𝑃) |
30 | 29 | necomd 2996 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝑃 ≠ 𝐵) |
31 | | simprlr 780 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝑃, 𝐴〉) |
32 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝑃, 𝐶〉) |
33 | | btwnconn1 34140 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
34 | 8, 9, 11, 10, 12, 33 | syl122anc 1381 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
35 | 34 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → ((𝑃 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
36 | 30, 31, 32, 35 | mp3and 1466 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
37 | 36 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → (𝐵 Btwn 〈𝑃, 𝐶〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
38 | | df-3an 1091 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) |
39 | | simpr3 1198 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐶 Btwn 〈𝑃, 𝐵〉) |
40 | | simpr2 1197 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐵 Btwn 〈𝑃, 𝐴〉) |
41 | 8, 9, 12, 11, 10, 39, 40 | btwnexchand 34065 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐶 Btwn 〈𝑃, 𝐴〉) |
42 | 41 | olcd 874 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
43 | 38, 42 | sylan2br 598 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
44 | 43 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → (𝐶 Btwn 〈𝑃, 𝐵〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
45 | 37, 44 | jaod 859 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
46 | 45 | expr 460 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (𝐵 Btwn 〈𝑃, 𝐴〉 → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
47 | 27, 46 | jaod 859 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
48 | 47 | imp32 422 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
49 | 5, 6, 48 | 3jca 1130 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
50 | 49 | exp31 423 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) → (((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))))) |
51 | 4, 50 | syl5 34 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))))) |
52 | 51 | impd 414 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
53 | | broutsideof2 34161 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)))) |
54 | 8, 9, 10, 11, 53 | syl13anc 1374 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)))) |
55 | | broutsideof2 34161 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐵, 𝐶〉 ↔ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
56 | 8, 9, 11, 12, 55 | syl13anc 1374 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐵, 𝐶〉 ↔ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
57 | 54, 56 | anbi12d 634 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))))) |
58 | | df-3an 1091 |
. . . . 5
⊢ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
59 | | df-3an 1091 |
. . . . 5
⊢ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)) ↔ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) |
60 | 58, 59 | anbi12i 630 |
. . . 4
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
61 | | an4 656 |
. . . 4
⊢ ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
62 | 60, 61 | bitr4i 281 |
. . 3
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
63 | 57, 62 | bitrdi 290 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))))) |
64 | | broutsideof2 34161 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐶〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
65 | 8, 9, 10, 12, 64 | syl13anc 1374 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐶〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
66 | 52, 63, 65 | 3imtr4d 297 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) → 𝑃OutsideOf〈𝐴, 𝐶〉)) |