Step | Hyp | Ref
| Expression |
1 | | simpl1 1190 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝑁 ∈ ℕ) |
2 | | simpl23 1252 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐶 ∈ (𝔼‘𝑁)) |
3 | | simpl21 1250 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐴 ∈ (𝔼‘𝑁)) |
4 | | simpl31 1253 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐷 ∈ (𝔼‘𝑁)) |
5 | 2, 3, 4 | 3jca 1127 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) |
6 | | simpl32 1254 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐸 ∈ (𝔼‘𝑁)) |
7 | | simpl33 1255 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝑃 ∈ (𝔼‘𝑁)) |
8 | 6, 7 | jca 512 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) |
9 | 1, 5, 8 | 3jca 1127 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → (𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)))) |
10 | | simpr2 1194 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐸 Btwn 〈𝐷, 𝐶〉) |
11 | | btwncom 34316 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐸 Btwn 〈𝐷, 𝐶〉 ↔ 𝐸 Btwn 〈𝐶, 𝐷〉)) |
12 | 1, 6, 4, 2, 11 | syl13anc 1371 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → (𝐸 Btwn 〈𝐷, 𝐶〉 ↔ 𝐸 Btwn 〈𝐶, 𝐷〉)) |
13 | 10, 12 | mpbid 231 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐸 Btwn 〈𝐶, 𝐷〉) |
14 | | simpr3 1195 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝑃 Btwn 〈𝐴, 𝐷〉) |
15 | 13, 14 | jca 512 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → (𝐸 Btwn 〈𝐶, 𝐷〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) |
16 | | axpasch 27309 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐸 Btwn 〈𝐶, 𝐷〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉) → ∃𝑟 ∈ (𝔼‘𝑁)(𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉))) |
17 | 9, 15, 16 | sylc 65 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → ∃𝑟 ∈ (𝔼‘𝑁)(𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) |
18 | | simp1l1 1265 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝑁 ∈ ℕ) |
19 | 6 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝐸 ∈ (𝔼‘𝑁)) |
20 | 2 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝐶 ∈ (𝔼‘𝑁)) |
21 | 3 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝐴 ∈ (𝔼‘𝑁)) |
22 | 19, 20, 21 | 3jca 1127 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) |
23 | | simp2 1136 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝑟 ∈ (𝔼‘𝑁)) |
24 | | simpl22 1251 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → 𝐵 ∈ (𝔼‘𝑁)) |
25 | 24 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝐵 ∈ (𝔼‘𝑁)) |
26 | 23, 25 | jca 512 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → (𝑟 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
27 | 18, 22, 26 | 3jca 1127 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → (𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑟 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))) |
28 | | simp3l 1200 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝑟 Btwn 〈𝐸, 𝐴〉) |
29 | | simp1r1 1268 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
30 | | btwncom 34316 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
31 | 18, 25, 21, 20, 30 | syl13anc 1371 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
32 | 29, 31 | mpbid 231 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → 𝐵 Btwn 〈𝐶, 𝐴〉) |
33 | 28, 32 | jca 512 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
34 | | axpasch 27309 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑟 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝐵 Btwn 〈𝐶, 𝐴〉) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑟, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉))) |
35 | 27, 33, 34 | sylc 65 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑟, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉)) |
36 | | simpll1 1211 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉))) |
37 | 36, 1 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝑁 ∈ ℕ) |
38 | 36, 7 | syl 17 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝑃 ∈ (𝔼‘𝑁)) |
39 | | simpll2 1212 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝑟 ∈ (𝔼‘𝑁)) |
40 | 38, 39 | jca 512 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) |
41 | | simplr 766 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝑞 ∈ (𝔼‘𝑁)) |
42 | 36, 2 | syl 17 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝐶 ∈ (𝔼‘𝑁)) |
43 | 41, 42 | jca 512 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → (𝑞 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) |
44 | 37, 40, 43 | 3jca 1127 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → (𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) ∧ (𝑞 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)))) |
45 | | simpl3r 1228 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) → 𝑟 Btwn 〈𝑃, 𝐶〉) |
46 | 45 | anim1i 615 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → (𝑟 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝑟, 𝐶〉)) |
47 | | btwnexch2 34325 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) ∧ (𝑞 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑟 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝑞 Btwn 〈𝑃, 𝐶〉)) |
48 | 44, 46, 47 | sylc 65 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) ∧ 𝑞 Btwn 〈𝑟, 𝐶〉) → 𝑞 Btwn 〈𝑃, 𝐶〉) |
49 | 48 | ex 413 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) → (𝑞 Btwn 〈𝑟, 𝐶〉 → 𝑞 Btwn 〈𝑃, 𝐶〉)) |
50 | 49 | anim1d 611 |
. . . . . 6
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝑃 ∈
(𝔼‘𝑁))) ∧
(𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) ∧ 𝑞 ∈ (𝔼‘𝑁)) → ((𝑞 Btwn 〈𝑟, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉) → (𝑞 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉))) |
51 | 50 | reximdva 3203 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → (∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑟, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉))) |
52 | 35, 51 | mpd 15 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) ∧ 𝑟 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉)) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉)) |
53 | 52 | rexlimdv3a 3215 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → (∃𝑟 ∈ (𝔼‘𝑁)(𝑟 Btwn 〈𝐸, 𝐴〉 ∧ 𝑟 Btwn 〈𝑃, 𝐶〉) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉))) |
54 | 17, 53 | mpd 15 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉)) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉)) |
55 | 54 | ex 413 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐶〉 ∧ 𝑃 Btwn 〈𝐴, 𝐷〉) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn 〈𝑃, 𝐶〉 ∧ 𝑞 Btwn 〈𝐵, 𝐸〉))) |