Proof of Theorem outsideoftr
Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . . 5
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → 𝐴 ≠ 𝑃) |
2 | | simplr 792 |
. . . . 5
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → 𝐵 ≠ 𝑃) |
3 | | simprr 796 |
. . . . 5
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → 𝐶 ≠ 𝑃) |
4 | 1, 2, 3 | 3jca 1242 |
. . . 4
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) |
5 | | simplr1 1103 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → 𝐴 ≠ 𝑃) |
6 | | simplr3 1105 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → 𝐶 ≠ 𝑃) |
7 | | df-3an 1039 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) |
8 | | simp1 1061 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
9 | | simp3r 1090 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝑃 ∈ (𝔼‘𝑁)) |
10 | | simp2l 1087 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
11 | | simp2r 1088 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
12 | | simp3l 1089 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
13 | | simpr2 1068 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
14 | | simpr3 1069 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝑃, 𝐶〉) |
15 | 8, 9, 10, 11, 12, 13, 14 | btwnexchand 32133 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐴 Btwn 〈𝑃, 𝐶〉) |
16 | 15 | orcd 407 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
17 | 7, 16 | sylan2br 493 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
18 | 17 | expr 643 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → (𝐵 Btwn 〈𝑃, 𝐶〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
19 | | simprlr 803 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
20 | | simprr 796 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐶 Btwn 〈𝑃, 𝐵〉) |
21 | | btwnconn3 32210 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
22 | 8, 9, 10, 12, 11, 21 | syl122anc 1335 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
24 | 19, 20, 23 | mp2and 715 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
25 | 24 | expr 643 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → (𝐶 Btwn 〈𝑃, 𝐵〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
26 | 18, 25 | jaod 395 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
27 | 26 | expr 643 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (𝐴 Btwn 〈𝑃, 𝐵〉 → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
28 | | simpll2 1101 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → 𝐵 ≠ 𝑃) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 ≠ 𝑃) |
30 | 29 | necomd 2849 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝑃 ≠ 𝐵) |
31 | | simprlr 803 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝑃, 𝐴〉) |
32 | | simprr 796 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝑃, 𝐶〉) |
33 | | btwnconn1 32208 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
34 | 8, 9, 11, 10, 12, 33 | syl122anc 1335 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
35 | 34 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → ((𝑃 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐵 Btwn 〈𝑃, 𝐶〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
36 | 30, 31, 32, 35 | mp3and 1427 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐵 Btwn 〈𝑃, 𝐶〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
37 | 36 | expr 643 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → (𝐵 Btwn 〈𝑃, 𝐶〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
38 | | df-3an 1039 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) |
39 | | simpr3 1069 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐶 Btwn 〈𝑃, 𝐵〉) |
40 | | simpr2 1068 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐵 Btwn 〈𝑃, 𝐴〉) |
41 | 8, 9, 12, 11, 10, 39, 40 | btwnexchand 32133 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → 𝐶 Btwn 〈𝑃, 𝐴〉) |
42 | 41 | olcd 408 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉 ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
43 | 38, 42 | sylan2br 493 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
44 | 43 | expr 643 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → (𝐶 Btwn 〈𝑃, 𝐵〉 → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
45 | 37, 44 | jaod 395 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
46 | 45 | expr 643 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (𝐵 Btwn 〈𝑃, 𝐴〉 → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
47 | 27, 46 | jaod 395 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) → ((𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
48 | 47 | imp32 449 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)) |
49 | 5, 6, 48 | 3jca 1242 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))) |
50 | 49 | exp31 630 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) → (((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))))) |
51 | 4, 50 | syl5 34 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) → (((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉))))) |
52 | 51 | impd 447 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) → (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
53 | | broutsideof2 32229 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)))) |
54 | 8, 9, 10, 11, 53 | syl13anc 1328 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)))) |
55 | | broutsideof2 32229 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐵, 𝐶〉 ↔ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
56 | 8, 9, 11, 12, 55 | syl13anc 1328 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐵, 𝐶〉 ↔ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
57 | 54, 56 | anbi12d 747 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))))) |
58 | | df-3an 1039 |
. . . . 5
⊢ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
59 | | df-3an 1039 |
. . . . 5
⊢ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)) ↔ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) |
60 | 58, 59 | anbi12i 733 |
. . . 4
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
61 | | an4 865 |
. . . 4
⊢ ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ ((𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
62 | 60, 61 | bitr4i 267 |
. . 3
⊢ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉)))) |
63 | 57, 62 | syl6bb 276 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃)) ∧ ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝐵 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐵〉))))) |
64 | | broutsideof2 32229 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐶〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
65 | 8, 9, 10, 12, 64 | syl13anc 1328 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐶〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐶〉 ∨ 𝐶 Btwn 〈𝑃, 𝐴〉)))) |
66 | 52, 63, 65 | 3imtr4d 283 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) → 𝑃OutsideOf〈𝐴, 𝐶〉)) |