Proof of Theorem broutsideof3
| Step | Hyp | Ref
| Expression |
| 1 | | broutsideof2 36123 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)))) |
| 2 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 3 | | simpr3 1197 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 4 | | simpr1 1195 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝑃 ∈ (𝔼‘𝑁)) |
| 5 | | btwndiff 36028 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) |
| 6 | 2, 3, 4, 5 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) |
| 8 | | df-3an 1089 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁))) |
| 9 | | 3anass 1095 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ (𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐))) |
| 10 | | simpr3 1197 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑃 ≠ 𝑐) |
| 11 | 10 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑐 ≠ 𝑃) |
| 12 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 13 | | simp23 1209 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
| 14 | | simp22 1208 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
| 15 | | simp21 1207 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) |
| 16 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝑐 ∈ (𝔼‘𝑁)) |
| 17 | | simpr1r 1232 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
| 18 | 12, 14, 15, 13, 17 | btwncomand 36016 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝐴 Btwn 〈𝐵, 𝑃〉) |
| 19 | | simpr2 1196 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑃 Btwn 〈𝐵, 𝑐〉) |
| 20 | 12, 13, 14, 15, 16, 18, 19 | btwnexch3and 36022 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑃 Btwn 〈𝐴, 𝑐〉) |
| 21 | 11, 20, 19 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) |
| 22 | 8, 9, 21 | syl2anbr 599 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉) ∧ (𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐))) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) |
| 23 | 22 | expr 456 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → ((𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 24 | 23 | an32s 652 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → ((𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 25 | 24 | reximdva 3168 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → (∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐵, 𝑐〉 ∧ 𝑃 ≠ 𝑐) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 26 | 7, 25 | mpd 15 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐴 Btwn 〈𝑃, 𝐵〉)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) |
| 27 | 26 | expr 456 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) → (𝐴 Btwn 〈𝑃, 𝐵〉 → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 28 | | simpr2 1196 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 29 | | btwndiff 36028 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) |
| 30 | 2, 28, 4, 29 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) |
| 31 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) |
| 32 | | 3anass 1095 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐) ↔ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐))) |
| 33 | | simpr3 1197 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑃 ≠ 𝑐) |
| 34 | 33 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑐 ≠ 𝑃) |
| 35 | | simpr2 1196 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑃 Btwn 〈𝐴, 𝑐〉) |
| 36 | | simpr1r 1232 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝐵 Btwn 〈𝑃, 𝐴〉) |
| 37 | 12, 13, 15, 14, 36 | btwncomand 36016 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝐵 Btwn 〈𝐴, 𝑃〉) |
| 38 | 12, 14, 13, 15, 16, 37, 35 | btwnexch3and 36022 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → 𝑃 Btwn 〈𝐵, 𝑐〉) |
| 39 | 34, 35, 38 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐)) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) |
| 40 | 8, 32, 39 | syl2anbr 599 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉) ∧ (𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐))) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) |
| 41 | 40 | expr 456 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → ((𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 42 | 41 | an32s 652 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → ((𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐) → (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 43 | 42 | reximdva 3168 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → (∃𝑐 ∈ (𝔼‘𝑁)(𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 ≠ 𝑐) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 44 | 31, 43 | mpd 15 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ 𝐵 Btwn 〈𝑃, 𝐴〉)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) |
| 45 | 44 | expr 456 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) → (𝐵 Btwn 〈𝑃, 𝐴〉 → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 46 | 27, 45 | jaod 860 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) → ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 47 | | simprr1 1222 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → 𝑐 ≠ 𝑃) |
| 48 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 49 | | simplr1 1216 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) |
| 50 | | simplr2 1217 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
| 51 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝑐 ∈ (𝔼‘𝑁)) |
| 52 | | simprr2 1223 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → 𝑃 Btwn 〈𝐴, 𝑐〉) |
| 53 | 48, 49, 50, 51, 52 | btwncomand 36016 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → 𝑃 Btwn 〈𝑐, 𝐴〉) |
| 54 | | simplr3 1218 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
| 55 | | simprr3 1224 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → 𝑃 Btwn 〈𝐵, 𝑐〉) |
| 56 | 48, 49, 54, 51, 55 | btwncomand 36016 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → 𝑃 Btwn 〈𝑐, 𝐵〉) |
| 57 | | btwnconn2 36103 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑐, 𝐴〉 ∧ 𝑃 Btwn 〈𝑐, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 58 | 48, 51, 49, 50, 54, 57 | syl122anc 1381 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) → ((𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑐, 𝐴〉 ∧ 𝑃 Btwn 〈𝑐, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → ((𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝑐, 𝐴〉 ∧ 𝑃 Btwn 〈𝑐, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 60 | 47, 53, 56, 59 | mp3and 1466 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) |
| 61 | 60 | expr 456 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) → ((𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 62 | 61 | an32s 652 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) ∧ 𝑐 ∈ (𝔼‘𝑁)) → ((𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 63 | 62 | rexlimdva 3155 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) → (∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 64 | 46, 63 | impbid 212 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃)) → ((𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉) ↔ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 65 | 64 | pm5.32da 579 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)))) |
| 66 | | df-3an 1089 |
. . 3
⊢ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉))) |
| 67 | | df-3an 1089 |
. . 3
⊢ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)) ↔ ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃) ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉))) |
| 68 | 65, 66, 67 | 3bitr4g 314 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)) ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)))) |
| 69 | 1, 68 | bitrd 279 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)))) |