| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . 3
⊢ (𝐶 ≠ 𝑐 ↔ ¬ 𝐶 = 𝑐) |
| 2 | | simp2rl 1243 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 𝐶 Btwn 〈𝐴, 𝑑〉) |
| 3 | 2 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → 𝐶 Btwn 〈𝐴, 𝑑〉) |
| 4 | | simp2ll 1241 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 𝐷 Btwn 〈𝐴, 𝑐〉) |
| 5 | 4 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → 𝐷 Btwn 〈𝐴, 𝑐〉) |
| 6 | 3, 5 | jca 511 |
. . . . . . . 8
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 𝐷 Btwn 〈𝐴, 𝑐〉)) |
| 7 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑁 ∈ ℕ) |
| 8 | | simprl1 1219 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 9 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 10 | | simprrl 781 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑑 ∈ (𝔼‘𝑁)) |
| 11 | | btwncom 36015 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝑑〉 ↔ 𝐶 Btwn 〈𝑑, 𝐴〉)) |
| 12 | 7, 8, 9, 10, 11 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (𝐶 Btwn 〈𝐴, 𝑑〉 ↔ 𝐶 Btwn 〈𝑑, 𝐴〉)) |
| 13 | | simprl2 1220 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 14 | | simprl3 1221 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑐 ∈ (𝔼‘𝑁)) |
| 15 | | btwncom 36015 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) → (𝐷 Btwn 〈𝐴, 𝑐〉 ↔ 𝐷 Btwn 〈𝑐, 𝐴〉)) |
| 16 | 7, 13, 9, 14, 15 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (𝐷 Btwn 〈𝐴, 𝑐〉 ↔ 𝐷 Btwn 〈𝑐, 𝐴〉)) |
| 17 | 12, 16 | anbi12d 632 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → ((𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 𝐷 Btwn 〈𝐴, 𝑐〉) ↔ (𝐶 Btwn 〈𝑑, 𝐴〉 ∧ 𝐷 Btwn 〈𝑐, 𝐴〉))) |
| 18 | 6, 17 | imbitrid 244 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → (𝐶 Btwn 〈𝑑, 𝐴〉 ∧ 𝐷 Btwn 〈𝑐, 𝐴〉))) |
| 19 | | axpasch 28956 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝑑, 𝐴〉 ∧ 𝐷 Btwn 〈𝑐, 𝐴〉) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) |
| 20 | 7, 10, 14, 9, 8, 13, 19 | syl132anc 1390 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → ((𝐶 Btwn 〈𝑑, 𝐴〉 ∧ 𝐷 Btwn 〈𝑐, 𝐴〉) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) |
| 21 | 18, 20 | syld 47 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) |
| 22 | 21 | imp 406 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) |
| 23 | | simpll1 1213 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 24 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑐 ∈ (𝔼‘𝑁)) |
| 25 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
| 26 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑑 ∈ (𝔼‘𝑁)) |
| 27 | | axsegcon 28942 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ∃𝑝 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉)) |
| 28 | 23, 24, 25, 25, 26, 27 | syl122anc 1381 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑝 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉)) |
| 29 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁)) |
| 30 | | axsegcon 28942 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑟 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)) |
| 31 | 23, 26, 25, 25, 29, 30 | syl122anc 1381 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑟 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)) |
| 32 | | reeanv 3229 |
. . . . . . . . 9
⊢
(∃𝑝 ∈
(𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)) ↔ (∃𝑝 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ ∃𝑟 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) |
| 33 | 28, 31, 32 | sylanbrc 583 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) |
| 34 | 33 | adantr 480 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) → ∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) |
| 35 | 7 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) →
𝑁 ∈
ℕ) |
| 36 | | simprl 771 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) →
𝑝 ∈
(𝔼‘𝑁)) |
| 37 | | simprr 773 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) →
𝑟 ∈
(𝔼‘𝑁)) |
| 38 | | axsegcon 28942 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) ∧ (𝑟 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) |
| 39 | 35, 36, 37, 37, 36, 38 | syl122anc 1381 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) →
∃𝑞 ∈
(𝔼‘𝑁)(𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)))) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) |
| 41 | | simp-4l 783 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
(𝑁 ∈ ℕ ∧
𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁))) |
| 42 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁))) |
| 44 | 10 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
𝑑 ∈
(𝔼‘𝑁)) |
| 45 | | simprrr 782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) → 𝑏 ∈ (𝔼‘𝑁)) |
| 46 | 45 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
𝑏 ∈
(𝔼‘𝑁)) |
| 47 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
𝑒 ∈
(𝔼‘𝑁)) |
| 48 | 44, 46, 47 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁) ∧
𝑒 ∈
(𝔼‘𝑁))) |
| 49 | 43, 48 | jca 511 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁) ∧
𝑒 ∈
(𝔼‘𝑁)))) |
| 50 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
𝑝 ∈
(𝔼‘𝑁)) |
| 51 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
𝑞 ∈
(𝔼‘𝑁)) |
| 52 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
𝑟 ∈
(𝔼‘𝑁)) |
| 53 | 50, 51, 52 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑞 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) |
| 54 | 41, 49, 53 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) →
((𝑁 ∈ ℕ ∧
𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁) ∧
𝑒 ∈
(𝔼‘𝑁))) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑞 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁)))) |
| 55 | | simp1ll 1237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 𝐴 ≠ 𝐵) |
| 56 | 55 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) → 𝐴 ≠ 𝐵) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → 𝐴 ≠ 𝐵) |
| 58 | | simp1lr 1238 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 𝐵 ≠ 𝐶) |
| 59 | 58 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) → 𝐵 ≠ 𝐶) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → 𝐵 ≠ 𝐶) |
| 61 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) → 𝐶 ≠ 𝑐) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → 𝐶 ≠ 𝑐) |
| 63 | 57, 60, 62 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐)) |
| 64 | | simpl1r 1226 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) |
| 65 | 64 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) |
| 66 | 63, 65 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) |
| 67 | | simpll2 1214 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) → ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
| 68 | 67 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
| 69 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → (𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉)) |
| 70 | 69 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉)) |
| 71 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) → (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)) |
| 72 | 71 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)) |
| 73 | 70, 72 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) |
| 74 | 66, 68, 73 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) |
| 75 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) |
| 76 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉)) |
| 77 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)) |
| 78 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) |
| 79 | 76, 77, 78 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉))) |
| 80 | 74, 75, 79 | jca32 515 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉)) → ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ ((𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉))))) |
| 81 | | btwnconn1lem12 36099 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑞 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ ((𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉))))) → 𝐷 = 𝑑) |
| 82 | 54, 80, 81 | syl2an 596 |
. . . . . . . . . . . 12
⊢
(((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
𝑞 ∈
(𝔼‘𝑁)) ∧
(((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉))) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉))) → 𝐷 = 𝑑) |
| 83 | 82 | an4s 660 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)))) ∧ (𝑞 ∈ (𝔼‘𝑁) ∧ (𝑟 Btwn 〈𝑝, 𝑞〉 ∧ 〈𝑟, 𝑞〉Cgr〈𝑟, 𝑝〉))) → 𝐷 = 𝑑) |
| 84 | 40, 83 | rexlimddv 3161 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(𝑝 ∈
(𝔼‘𝑁) ∧
𝑟 ∈
(𝔼‘𝑁))) ∧
((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)))) → 𝐷 = 𝑑) |
| 85 | 84 | an4s 660 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) ∧ ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) ∧ ((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)))) → 𝐷 = 𝑑) |
| 86 | 85 | exp32 420 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) → ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑟 ∈ (𝔼‘𝑁)) → (((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)) → 𝐷 = 𝑑))) |
| 87 | 86 | rexlimdvv 3212 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) → (∃𝑝 ∈ (𝔼‘𝑁)∃𝑟 ∈ (𝔼‘𝑁)((𝐶 Btwn 〈𝑐, 𝑝〉 ∧ 〈𝐶, 𝑝〉Cgr〈𝐶, 𝑑〉) ∧ (𝐶 Btwn 〈𝑑, 𝑟〉 ∧ 〈𝐶, 𝑟〉Cgr〈𝐶, 𝑒〉)) → 𝐷 = 𝑑)) |
| 88 | 34, 87 | mpd 15 |
. . . . . 6
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) → 𝐷 = 𝑑) |
| 89 | 88 | an4s 660 |
. . . . 5
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
((𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝑐 ∈
(𝔼‘𝑁)) ∧
(𝑑 ∈
(𝔼‘𝑁) ∧
𝑏 ∈
(𝔼‘𝑁)))) ∧
((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ (𝑒 Btwn 〈𝐶, 𝑐〉 ∧ 𝑒 Btwn 〈𝐷, 𝑑〉))) → 𝐷 = 𝑑) |
| 90 | 22, 89 | rexlimddv 3161 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ 𝐶 ≠ 𝑐)) → 𝐷 = 𝑑) |
| 91 | 90 | expr 456 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) → (𝐶 ≠ 𝑐 → 𝐷 = 𝑑)) |
| 92 | 1, 91 | biimtrrid 243 |
. 2
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) → (¬ 𝐶 = 𝑐 → 𝐷 = 𝑑)) |
| 93 | 92 | orrd 864 |
1
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)) |