# Metamath Proof Explorer

## Theorem btwnconn1lem5

Description: Lemma for btwnconn1 . Now, we introduce E , the intersection of C c and D d . We begin by showing that it is the midpoint of C and c . (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem5 ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{E},{C}⟩\mathrm{Cgr}⟨{E},{c}⟩$

### Proof

Step Hyp Ref Expression
1 simprrr ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to {E}\mathrm{Btwn}⟨{D},{d}⟩$
2 simp11 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
3 simp22 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
4 simp33 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {E}\in 𝔼\left({N}\right)$
5 simp31 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {d}\in 𝔼\left({N}\right)$
6 cgr3rflx ${⊢}\left({N}\in ℕ\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {d}\in 𝔼\left({N}\right)\right)\right)\to ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩$
7 2 3 4 5 6 syl13anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩$
8 7 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩$
9 simp2lr ${⊢}\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\to ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩$
10 9 ad2antrl ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩$
11 simp23 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {c}\in 𝔼\left({N}\right)$
12 simp21 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
13 cgrcomr ${⊢}\left({N}\in ℕ\wedge \left({D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩↔⟨{D},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩\right)$
14 2 3 11 12 3 13 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩↔⟨{D},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩\right)$
15 cgrcom ${⊢}\left({N}\in ℕ\wedge \left({D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{D},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩↔⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\right)$
16 2 3 11 3 12 15 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{D},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩↔⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\right)$
17 14 16 bitrd ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩↔⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\right)$
18 17 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to \left(⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩↔⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\right)$
19 10 18 mpbid ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩$
20 simp2rr ${⊢}\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\to ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩$
21 20 ad2antrl ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩$
22 2 12 5 12 3 21 cgrcomlrand ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{d},{C}⟩\mathrm{Cgr}⟨{D},{C}⟩$
23 3simpa ${⊢}\left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\to \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)$
24 23 3anim3i ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\right)$
25 simpl ${⊢}\left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\to \left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)$
26 btwnconn1lem4 ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\right)\to ⟨{d},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩$
27 24 25 26 syl2an ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{d},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩$
28 2 5 12 5 11 3 12 22 27 cgrtr3and ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{d},{C}⟩\mathrm{Cgr}⟨{d},{c}⟩$
29 19 28 jca ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to \left(⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\wedge ⟨{d},{C}⟩\mathrm{Cgr}⟨{d},{c}⟩\right)$
30 brifs2 ${⊢}\left(\left({N}\in ℕ\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {d}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨⟨{D},{E}⟩,⟨{d},{C}⟩⟩\mathrm{InnerFiveSeg}⟨⟨{D},{E}⟩,⟨{d},{c}⟩⟩↔\left({E}\mathrm{Btwn}⟨{D},{d}⟩\wedge ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩\wedge \left(⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\wedge ⟨{d},{C}⟩\mathrm{Cgr}⟨{d},{c}⟩\right)\right)\right)$
31 ifscgr ${⊢}\left(\left({N}\in ℕ\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {d}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨⟨{D},{E}⟩,⟨{d},{C}⟩⟩\mathrm{InnerFiveSeg}⟨⟨{D},{E}⟩,⟨{d},{c}⟩⟩\to ⟨{E},{C}⟩\mathrm{Cgr}⟨{E},{c}⟩\right)$
32 30 31 sylbird ${⊢}\left(\left({N}\in ℕ\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {d}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({E}\mathrm{Btwn}⟨{D},{d}⟩\wedge ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩\wedge \left(⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\wedge ⟨{d},{C}⟩\mathrm{Cgr}⟨{d},{c}⟩\right)\right)\to ⟨{E},{C}⟩\mathrm{Cgr}⟨{E},{c}⟩\right)$
33 2 3 4 5 12 3 4 5 11 32 syl333anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({E}\mathrm{Btwn}⟨{D},{d}⟩\wedge ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩\wedge \left(⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\wedge ⟨{d},{C}⟩\mathrm{Cgr}⟨{d},{c}⟩\right)\right)\to ⟨{E},{C}⟩\mathrm{Cgr}⟨{E},{c}⟩\right)$
34 33 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to \left(\left({E}\mathrm{Btwn}⟨{D},{d}⟩\wedge ⟨{D},⟨{E},{d}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{d}⟩⟩\wedge \left(⟨{D},{C}⟩\mathrm{Cgr}⟨{D},{c}⟩\wedge ⟨{d},{C}⟩\mathrm{Cgr}⟨{d},{c}⟩\right)\right)\to ⟨{E},{C}⟩\mathrm{Cgr}⟨{E},{c}⟩\right)$
35 1 8 29 34 mp3and ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{E},{C}⟩\mathrm{Cgr}⟨{E},{c}⟩$