Proof of Theorem midofsegid
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simp1 1154 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 2 | | simp2l 1218 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 3 | | simp3r 1221 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 4 | | simp3l 1220 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 5 | | simprr 785 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐷 Btwn ⟨𝐴, 𝐸⟩)) → 𝐷 Btwn ⟨𝐴, 𝐸⟩) |
| 6 | | simprl3 1239 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐷 Btwn ⟨𝐴, 𝐸⟩)) → ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) |
| 7 | 1, 2, 4, 2, 3, 6 | cgrcomand 36579 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐷 Btwn ⟨𝐴, 𝐸⟩)) → ⟨𝐴, 𝐸⟩Cgr⟨𝐴, 𝐷⟩) |
| 8 | 1, 2, 3, 4, 5, 7 | endofsegidand 36674 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐷 Btwn ⟨𝐴, 𝐸⟩)) → 𝐸 = 𝐷) |
| 9 | 8 | eqcomd 2768 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐷 Btwn ⟨𝐴, 𝐸⟩)) → 𝐷 = 𝐸) |
| 10 | 9 | expr 462 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩)) → (𝐷 Btwn ⟨𝐴, 𝐸⟩ → 𝐷 = 𝐸)) |
| 11 | | simprr 785 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐸 Btwn ⟨𝐴, 𝐷⟩)) → 𝐸 Btwn ⟨𝐴, 𝐷⟩) |
| 12 | | simprl3 1239 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐸 Btwn ⟨𝐴, 𝐷⟩)) → ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) |
| 13 | 1, 2, 4, 3, 11, 12 | endofsegidand 36674 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) ∧ 𝐸 Btwn ⟨𝐴, 𝐷⟩)) → 𝐷 = 𝐸) |
| 14 | 13 | expr 462 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩)) → (𝐸 Btwn ⟨𝐴, 𝐷⟩ → 𝐷 = 𝐸)) |
| 15 | | 3simpa 1166 |
. . . . 5
⊢ ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) → (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩)) |
| 16 | 15 | adantl 487 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩)) → (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩)) |
| 17 | | simp2r 1219 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 18 | | btwnconn3 36691 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩) → (𝐷 Btwn ⟨𝐴, 𝐸⟩ ∨ 𝐸 Btwn ⟨𝐴, 𝐷⟩))) |
| 19 | 1, 2, 4, 3, 17, 18 | syl122anc 1406 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩) → (𝐷 Btwn ⟨𝐴, 𝐸⟩ ∨ 𝐸 Btwn ⟨𝐴, 𝐷⟩))) |
| 20 | 19 | adantr 486 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩)) → ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩) → (𝐷 Btwn ⟨𝐴, 𝐸⟩ ∨ 𝐸 Btwn ⟨𝐴, 𝐷⟩))) |
| 21 | 16, 20 | mpd 16 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩)) → (𝐷 Btwn ⟨𝐴, 𝐸⟩ ∨ 𝐸 Btwn ⟨𝐴, 𝐷⟩)) |
| 22 | 10, 14, 21 | mpjaod 874 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ (𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩)) → 𝐷 = 𝐸) |
| 23 | 22 | ex 418 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐵⟩ ∧ 𝐸 Btwn ⟨𝐴, 𝐵⟩ ∧ ⟨𝐴, 𝐷⟩Cgr⟨𝐴, 𝐸⟩) → 𝐷 = 𝐸)) |
