# Metamath Proof Explorer

## Theorem ax5seglem6

Description: Lemma for ax5seg . Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion ax5seglem6 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {T}={S}$

### Proof

Step Hyp Ref Expression
1 simp22l ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {T}\in \left[0,1\right]$
2 elicc01 ${⊢}{T}\in \left[0,1\right]↔\left({T}\in ℝ\wedge 0\le {T}\wedge {T}\le 1\right)$
3 2 simp1bi ${⊢}{T}\in \left[0,1\right]\to {T}\in ℝ$
4 resqcl ${⊢}{T}\in ℝ\to {{T}}^{2}\in ℝ$
5 4 recnd ${⊢}{T}\in ℝ\to {{T}}^{2}\in ℂ$
6 1 3 5 3syl ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {{T}}^{2}\in ℂ$
7 simp22r ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {S}\in \left[0,1\right]$
8 elicc01 ${⊢}{S}\in \left[0,1\right]↔\left({S}\in ℝ\wedge 0\le {S}\wedge {S}\le 1\right)$
9 8 simp1bi ${⊢}{S}\in \left[0,1\right]\to {S}\in ℝ$
10 resqcl ${⊢}{S}\in ℝ\to {{S}}^{2}\in ℝ$
11 10 recnd ${⊢}{S}\in ℝ\to {{S}}^{2}\in ℂ$
12 7 9 11 3syl ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {{S}}^{2}\in ℂ$
13 fzfid ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left(1\dots {N}\right)\in \mathrm{Fin}$
14 simprl1 ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
15 14 3ad2ant1 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {A}\in 𝔼\left({N}\right)$
16 fveecn ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {j}\in \left(1\dots {N}\right)\right)\to {A}\left({j}\right)\in ℂ$
17 15 16 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\wedge {j}\in \left(1\dots {N}\right)\right)\to {A}\left({j}\right)\in ℂ$
18 simprl3 ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
19 18 3ad2ant1 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {C}\in 𝔼\left({N}\right)$
20 fveecn ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {j}\in \left(1\dots {N}\right)\right)\to {C}\left({j}\right)\in ℂ$
21 19 20 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\wedge {j}\in \left(1\dots {N}\right)\right)\to {C}\left({j}\right)\in ℂ$
22 17 21 subcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\wedge {j}\in \left(1\dots {N}\right)\right)\to {A}\left({j}\right)-{C}\left({j}\right)\in ℂ$
23 22 sqcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\wedge {j}\in \left(1\dots {N}\right)\right)\to {\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}\in ℂ$
24 13 23 fsumcl ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}\in ℂ$
25 simp1l ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {N}\in ℕ$
26 simp1rl ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)$
27 simp21 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {A}\ne {B}$
28 simp23l ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)$
29 ax5seglem5 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\wedge \left({A}\ne {B}\wedge {T}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}\ne 0$
30 25 26 27 1 28 29 syl23anc ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}\ne 0$
31 simp3l ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩$
32 simprl2 ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
33 simprr1 ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
34 simprr2 ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to {E}\in 𝔼\left({N}\right)$
35 brcgr ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩↔\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{B}\left({j}\right)\right)}^{2}=\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{E}\left({j}\right)\right)}^{2}\right)$
36 14 32 33 34 35 syl22anc ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩↔\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{B}\left({j}\right)\right)}^{2}=\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{E}\left({j}\right)\right)}^{2}\right)$
37 36 3ad2ant1 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩↔\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{B}\left({j}\right)\right)}^{2}=\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{E}\left({j}\right)\right)}^{2}\right)$
38 31 37 mpbid ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{B}\left({j}\right)\right)}^{2}=\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{E}\left({j}\right)\right)}^{2}$
39 ax5seglem1 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({T}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{B}\left({j}\right)\right)}^{2}={{T}}^{2}\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}$
40 25 15 19 1 28 39 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{B}\left({j}\right)\right)}^{2}={{T}}^{2}\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}$
41 33 3ad2ant1 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {D}\in 𝔼\left({N}\right)$
42 simprr3 ${⊢}\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\to {F}\in 𝔼\left({N}\right)$
43 42 3ad2ant1 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {F}\in 𝔼\left({N}\right)$
44 simp23r ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)$
45 ax5seglem1 ${⊢}\left({N}\in ℕ\wedge \left({D}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\wedge \left({S}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\to \sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{E}\left({j}\right)\right)}^{2}={{S}}^{2}\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{F}\left({j}\right)\right)}^{2}$
46 25 41 43 7 44 45 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{E}\left({j}\right)\right)}^{2}={{S}}^{2}\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{F}\left({j}\right)\right)}^{2}$
47 38 40 46 3eqtr3d ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {{T}}^{2}\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}={{S}}^{2}\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{F}\left({j}\right)\right)}^{2}$
48 simp1rr ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)$
49 simp22 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)$
50 simp23 ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)$
51 simp3r ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩$
52 ax5seglem3 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}=\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{F}\left({j}\right)\right)}^{2}$
53 25 26 48 49 50 31 51 52 syl322anc ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}=\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{F}\left({j}\right)\right)}^{2}$
54 53 oveq2d ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {{S}}^{2}\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}={{S}}^{2}\sum _{{j}=1}^{{N}}{\left({D}\left({j}\right)-{F}\left({j}\right)\right)}^{2}$
55 47 54 eqtr4d ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {{T}}^{2}\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}={{S}}^{2}\sum _{{j}=1}^{{N}}{\left({A}\left({j}\right)-{C}\left({j}\right)\right)}^{2}$
56 6 12 24 30 55 mulcan2ad ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {{T}}^{2}={{S}}^{2}$
57 2 simp2bi ${⊢}{T}\in \left[0,1\right]\to 0\le {T}$
58 3 57 jca ${⊢}{T}\in \left[0,1\right]\to \left({T}\in ℝ\wedge 0\le {T}\right)$
59 1 58 syl ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left({T}\in ℝ\wedge 0\le {T}\right)$
60 8 simp2bi ${⊢}{S}\in \left[0,1\right]\to 0\le {S}$
61 9 60 jca ${⊢}{S}\in \left[0,1\right]\to \left({S}\in ℝ\wedge 0\le {S}\right)$
62 7 61 syl ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left({S}\in ℝ\wedge 0\le {S}\right)$
63 sq11 ${⊢}\left(\left({T}\in ℝ\wedge 0\le {T}\right)\wedge \left({S}\in ℝ\wedge 0\le {S}\right)\right)\to \left({{T}}^{2}={{S}}^{2}↔{T}={S}\right)$
64 59 62 63 syl2anc ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to \left({{T}}^{2}={{S}}^{2}↔{T}={S}\right)$
65 56 64 mpbid ${⊢}\left(\left({N}\in ℕ\wedge \left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\right)\wedge \left({A}\ne {B}\wedge \left({T}\in \left[0,1\right]\wedge {S}\in \left[0,1\right]\right)\wedge \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{B}\left({i}\right)=\left(1-{T}\right){A}\left({i}\right)+{T}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{S}\right){D}\left({i}\right)+{S}{F}\left({i}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to {T}={S}$