Proof of Theorem btwnconn1lem7
| Step | Hyp | Ref
| Expression |
| 1 | | simp1l3 1269 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 𝐶 ≠ 𝑐) |
| 2 | 1 | adantr 480 |
. . . 4
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ (𝐸 Btwn 〈𝐶, 𝑐〉 ∧ 𝐸 Btwn 〈𝐷, 𝑑〉)) → 𝐶 ≠ 𝑐) |
| 3 | | simp2rr 1244 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉) |
| 4 | 3 | adantr 480 |
. . . 4
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ (𝐸 Btwn 〈𝐶, 𝑐〉 ∧ 𝐸 Btwn 〈𝐷, 𝑑〉)) → 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉) |
| 5 | | simp2lr 1242 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) |
| 6 | 5 | adantr 480 |
. . . 4
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ (𝐸 Btwn 〈𝐶, 𝑐〉 ∧ 𝐸 Btwn 〈𝐷, 𝑑〉)) → 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) |
| 7 | 2, 4, 6 | 3jca 1129 |
. . 3
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ (𝐸 Btwn 〈𝐶, 𝑐〉 ∧ 𝐸 Btwn 〈𝐷, 𝑑〉)) → (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) |
| 8 | | simp11 1204 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 9 | | simp21 1207 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 10 | | simp22 1208 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 11 | | simp23 1209 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝑐 ∈ (𝔼‘𝑁)) |
| 12 | | simp31 1210 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝑑 ∈ (𝔼‘𝑁)) |
| 13 | | simpr1 1195 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → 𝐶 ≠ 𝑐) |
| 14 | | opeq2 4874 |
. . . . . . . . . . . 12
⊢ (𝐶 = 𝑑 → 〈𝐶, 𝐶〉 = 〈𝐶, 𝑑〉) |
| 15 | 14 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝐶 = 𝑑 → (〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) |
| 16 | 15 | 3anbi2d 1443 |
. . . . . . . . . 10
⊢ (𝐶 = 𝑑 → ((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ↔ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉))) |
| 17 | 16 | biimparc 479 |
. . . . . . . . 9
⊢ (((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ 𝐶 = 𝑑) → (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) |
| 18 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) → 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉) |
| 19 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 20 | | simp2l 1200 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 21 | | simp2r 1201 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 22 | | cgrid2 36004 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 → 𝐶 = 𝐷)) |
| 23 | 19, 20, 20, 21, 22 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 → 𝐶 = 𝐷)) |
| 24 | 18, 23 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) → 𝐶 = 𝐷)) |
| 25 | 24 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → 𝐶 = 𝐷) |
| 26 | | opeq1 4873 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 = 𝐷 → 〈𝐶, 𝑐〉 = 〈𝐷, 𝑐〉) |
| 27 | | opeq2 4874 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 = 𝐷 → 〈𝐶, 𝐶〉 = 〈𝐶, 𝐷〉) |
| 28 | 26, 27 | breq12d 5156 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 = 𝐷 → (〈𝐶, 𝑐〉Cgr〈𝐶, 𝐶〉 ↔ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) |
| 29 | 28 | biimparc 479 |
. . . . . . . . . . . . . 14
⊢
((〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉 ∧ 𝐶 = 𝐷) → 〈𝐶, 𝑐〉Cgr〈𝐶, 𝐶〉) |
| 30 | | simp3l 1202 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝑐 ∈ (𝔼‘𝑁)) |
| 31 | | axcgrid 28931 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝑐〉Cgr〈𝐶, 𝐶〉 → 𝐶 = 𝑐)) |
| 32 | 19, 20, 30, 20, 31 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝑐〉Cgr〈𝐶, 𝐶〉 → 𝐶 = 𝑐)) |
| 33 | 29, 32 | syl5 34 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ((〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉 ∧ 𝐶 = 𝐷) → 𝐶 = 𝑐)) |
| 34 | 33 | expdimp 452 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) → (𝐶 = 𝐷 → 𝐶 = 𝑐)) |
| 35 | 34 | 3ad2antr3 1191 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → (𝐶 = 𝐷 → 𝐶 = 𝑐)) |
| 36 | 25, 35 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → 𝐶 = 𝑐) |
| 37 | 36 | ex 412 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝐶〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) → 𝐶 = 𝑐)) |
| 38 | 17, 37 | syl5 34 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ 𝐶 = 𝑑) → 𝐶 = 𝑐)) |
| 39 | 38 | expdimp 452 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → (𝐶 = 𝑑 → 𝐶 = 𝑐)) |
| 40 | 39 | necon3d 2961 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → (𝐶 ≠ 𝑐 → 𝐶 ≠ 𝑑)) |
| 41 | 13, 40 | mpd 15 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) → 𝐶 ≠ 𝑑) |
| 42 | 41 | ex 412 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) → 𝐶 ≠ 𝑑)) |
| 43 | 8, 9, 10, 11, 12, 42 | syl122anc 1381 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐶 ≠ 𝑐 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) → 𝐶 ≠ 𝑑)) |
| 44 | 7, 43 | syl5 34 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ (𝐸 Btwn 〈𝐶, 𝑐〉 ∧ 𝐸 Btwn 〈𝐷, 𝑑〉)) → 𝐶 ≠ 𝑑)) |
| 45 | 44 | imp 406 |
1
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) ∧ (𝐸 Btwn 〈𝐶, 𝑐〉 ∧ 𝐸 Btwn 〈𝐷, 𝑑〉))) → 𝐶 ≠ 𝑑) |