# Metamath Proof Explorer

## Theorem btwnconn1lem4

Description: Lemma for btwnconn1 . Assuming C =/= c , we now attempt to force D = d from here out via a series of congruences. (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion 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}⟩$

### Proof

Step Hyp Ref Expression
1 simp1rl ${⊢}\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 {B}\mathrm{Btwn}⟨{A},{C}⟩$
2 simp2rl ${⊢}\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}\mathrm{Btwn}⟨{A},{d}⟩$
3 1 2 jca ${⊢}\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 \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {C}\mathrm{Btwn}⟨{A},{d}⟩\right)$
4 3 adantl ${⊢}\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 \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {C}\mathrm{Btwn}⟨{A},{d}⟩\right)$
5 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)\right)\right)\to {N}\in ℕ$
6 simp12 ${⊢}\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)\to {A}\in 𝔼\left({N}\right)$
7 simp13 ${⊢}\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)\to {B}\in 𝔼\left({N}\right)$
8 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)\right)\right)\to {C}\in 𝔼\left({N}\right)$
9 simp3l ${⊢}\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)\to {d}\in 𝔼\left({N}\right)$
10 btwnexch3 ${⊢}\left({N}\in ℕ\wedge \left({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)\right)\right)\to \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {C}\mathrm{Btwn}⟨{A},{d}⟩\right)\to {C}\mathrm{Btwn}⟨{B},{d}⟩\right)$
11 5 6 7 8 9 10 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)\right)\right)\to \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {C}\mathrm{Btwn}⟨{A},{d}⟩\right)\to {C}\mathrm{Btwn}⟨{B},{d}⟩\right)$
12 11 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)\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 \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {C}\mathrm{Btwn}⟨{A},{d}⟩\right)\to {C}\mathrm{Btwn}⟨{B},{d}⟩\right)$
13 4 12 mpd ${⊢}\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 {C}\mathrm{Btwn}⟨{B},{d}⟩$
14 simp3lr ${⊢}\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},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩$
15 14 adantl ${⊢}\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 ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩$
16 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)\right)\right)\to {c}\in 𝔼\left({N}\right)$
17 simp3r ${⊢}\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)\to {b}\in 𝔼\left({N}\right)$
18 cgrcomlr ${⊢}\left({N}\in ℕ\wedge \left({c}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩↔⟨{b},{c}⟩\mathrm{Cgr}⟨{B},{C}⟩\right)$
19 5 16 17 8 7 18 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)\right)\right)\to \left(⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩↔⟨{b},{c}⟩\mathrm{Cgr}⟨{B},{C}⟩\right)$
20 cgrcom ${⊢}\left({N}\in ℕ\wedge \left({b}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{b},{c}⟩\mathrm{Cgr}⟨{B},{C}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\right)$
21 5 17 16 7 8 20 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)\right)\right)\to \left(⟨{b},{c}⟩\mathrm{Cgr}⟨{B},{C}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\right)$
22 19 21 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)\right)\right)\to \left(⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\right)$
23 22 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)\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 \left(⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\right)$
24 15 23 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)\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 ⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩$
25 3simpa ${⊢}\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\to \left({A}\ne {B}\wedge {B}\ne {C}\right)$
26 25 anim1i ${⊢}\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)\to \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)$
27 btwnconn1lem3 ${⊢}\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}\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 ⟨{B},{d}⟩\mathrm{Cgr}⟨{b},{D}⟩$
28 26 27 syl3anr1 ${⊢}\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 ⟨{B},{d}⟩\mathrm{Cgr}⟨{b},{D}⟩$
29 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)\right)\right)\to {D}\in 𝔼\left({N}\right)$
30 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}⟩$
31 30 adantl ${⊢}\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 ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩$
32 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}⟩$
33 32 adantl ${⊢}\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}⟨{C},{D}⟩$
34 5 29 16 8 29 33 cgrcomland ${⊢}\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 ⟨{c},{D}⟩\mathrm{Cgr}⟨{C},{D}⟩$
35 5 8 9 16 29 8 29 31 34 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)\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 ⟨{C},{d}⟩\mathrm{Cgr}⟨{c},{D}⟩$
36 brcgr3 ${⊢}\left({N}\in ℕ\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {d}\in 𝔼\left({N}\right)\right)\wedge \left({b}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩↔\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\wedge ⟨{B},{d}⟩\mathrm{Cgr}⟨{b},{D}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{c},{D}⟩\right)\right)$
37 5 7 8 9 17 16 29 36 syl133anc ${⊢}\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)\to \left(⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩↔\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\wedge ⟨{B},{d}⟩\mathrm{Cgr}⟨{b},{D}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{c},{D}⟩\right)\right)$
38 37 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)\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 \left(⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩↔\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{b},{c}⟩\wedge ⟨{B},{d}⟩\mathrm{Cgr}⟨{b},{D}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{c},{D}⟩\right)\right)$
39 24 28 35 38 mpbir3and ${⊢}\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 ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩$
40 simpl ${⊢}\left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\to {d}\in 𝔼\left({N}\right)$
41 simpr ${⊢}\left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\to {b}\in 𝔼\left({N}\right)$
42 40 41 41 3jca ${⊢}\left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\to \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)$
43 42 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)\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)\wedge {b}\in 𝔼\left({N}\right)\right)\right)$
44 26 3anim1i ${⊢}\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 \left(\left(\left({A}\ne {B}\wedge {B}\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)$
45 btwnconn1lem1 ${⊢}\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 {b}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left({A}\ne {B}\wedge {B}\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 ⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩$
46 43 44 45 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)\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 ⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩$
47 5 8 16 cgrrflx2d ${⊢}\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)\to ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩$
48 47 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)\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 ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩$
49 46 48 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)\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 \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)$
50 13 39 49 3jca ${⊢}\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 \left({C}\mathrm{Btwn}⟨{B},{d}⟩\wedge ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩\wedge \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)\right)$
51 simp1l2 ${⊢}\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 {B}\ne {C}$
52 51 adantl ${⊢}\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 {B}\ne {C}$
53 brofs2 ${⊢}\left(\left({N}\in ℕ\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {c}\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)\right)\to \left(⟨⟨{B},{C}⟩,⟨{d},{c}⟩⟩\mathrm{OuterFiveSeg}⟨⟨{b},{c}⟩,⟨{D},{C}⟩⟩↔\left({C}\mathrm{Btwn}⟨{B},{d}⟩\wedge ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩\wedge \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)\right)\right)$
54 53 anbi1d ${⊢}\left(\left({N}\in ℕ\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {c}\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)\right)\to \left(\left(⟨⟨{B},{C}⟩,⟨{d},{c}⟩⟩\mathrm{OuterFiveSeg}⟨⟨{b},{c}⟩,⟨{D},{C}⟩⟩\wedge {B}\ne {C}\right)↔\left(\left({C}\mathrm{Btwn}⟨{B},{d}⟩\wedge ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩\wedge \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)\right)\wedge {B}\ne {C}\right)\right)$
55 5segofs ${⊢}\left(\left({N}\in ℕ\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {c}\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)\right)\to \left(\left(⟨⟨{B},{C}⟩,⟨{d},{c}⟩⟩\mathrm{OuterFiveSeg}⟨⟨{b},{c}⟩,⟨{D},{C}⟩⟩\wedge {B}\ne {C}\right)\to ⟨{d},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩\right)$
56 54 55 sylbird ${⊢}\left(\left({N}\in ℕ\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {c}\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)\right)\to \left(\left(\left({C}\mathrm{Btwn}⟨{B},{d}⟩\wedge ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩\wedge \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)\right)\wedge {B}\ne {C}\right)\to ⟨{d},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩\right)$
57 5 7 8 9 16 17 16 29 8 56 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)\right)\right)\to \left(\left(\left({C}\mathrm{Btwn}⟨{B},{d}⟩\wedge ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩\wedge \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)\right)\wedge {B}\ne {C}\right)\to ⟨{d},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩\right)$
58 57 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)\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 \left(\left(\left({C}\mathrm{Btwn}⟨{B},{d}⟩\wedge ⟨{B},⟨{C},{d}⟩⟩\mathrm{Cgr3}⟨{b},⟨{c},{D}⟩⟩\wedge \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{b},{C}⟩\wedge ⟨{C},{c}⟩\mathrm{Cgr}⟨{c},{C}⟩\right)\right)\wedge {B}\ne {C}\right)\to ⟨{d},{c}⟩\mathrm{Cgr}⟨{D},{C}⟩\right)$
59 50 52 58 mp2and ${⊢}\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}⟩$