Metamath Proof Explorer

Theorem ax5seglem3

Description: Lemma for ax5seg . Combine congruences for points on a line. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2

Proof

Step Hyp Ref Expression
1 1re ⊢1∈ℝ
2 elicc01 ⊢T∈01↔T∈ℝ∧0≤T∧T≤1
3 2 simp1bi ⊢T∈01→T∈ℝ
4 resubcl ⊢1∈ℝ∧T∈ℝ→1−T∈ℝ
5 1 3 4 sylancr ⊢T∈01→1−T∈ℝ
6 5 ad2antrr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→1−T∈ℝ
7 6 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T∈ℝ
8 fzfid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→1…N∈Fin
9 ax5seglem3a ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j∈ℝ∧D⁡j−F⁡j∈ℝ
10 9 simpld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j∈ℝ
11 10 resqcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j2∈ℝ
12 8 11 fsumrecl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1NA⁡j−C⁡j2∈ℝ
13 10 sqge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→0≤A⁡j−C⁡j2
14 8 11 13 fsumge0 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→0≤∑j=1NA⁡j−C⁡j2
15 12 14 resqrtcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1NA⁡j−C⁡j2∈ℝ
16 15 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j2∈ℝ
17 7 16 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T⁢∑j=1NA⁡j−C⁡j2∈ℝ
18 elicc01 ⊢S∈01↔S∈ℝ∧0≤S∧S≤1
19 18 simp1bi ⊢S∈01→S∈ℝ
20 resubcl ⊢1∈ℝ∧S∈ℝ→1−S∈ℝ
21 1 19 20 sylancr ⊢S∈01→1−S∈ℝ
22 21 ad2antlr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→1−S∈ℝ
23 22 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−S∈ℝ
24 9 simprd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→D⁡j−F⁡j∈ℝ
25 24 resqcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→D⁡j−F⁡j2∈ℝ
26 8 25 fsumrecl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1ND⁡j−F⁡j2∈ℝ
27 24 sqge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧j∈1…N→0≤D⁡j−F⁡j2
28 8 25 27 fsumge0 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→0≤∑j=1ND⁡j−F⁡j2
29 26 28 resqrtcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1ND⁡j−F⁡j2∈ℝ
30 29 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1ND⁡j−F⁡j2∈ℝ
31 23 30 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−S⁢∑j=1ND⁡j−F⁡j2∈ℝ
32 2 simp3bi ⊢T∈01→T≤1
33 subge0 ⊢1∈ℝ∧T∈ℝ→0≤1−T↔T≤1
34 1 3 33 sylancr ⊢T∈01→0≤1−T↔T≤1
35 32 34 mpbird ⊢T∈01→0≤1−T
36 35 ad2antrr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→0≤1−T
37 36 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤1−T
38 12 14 sqrtge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→0≤∑j=1NA⁡j−C⁡j2
39 38 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤∑j=1NA⁡j−C⁡j2
40 7 16 37 39 mulge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤1−T⁢∑j=1NA⁡j−C⁡j2
41 18 simp3bi ⊢S∈01→S≤1
42 subge0 ⊢1∈ℝ∧S∈ℝ→0≤1−S↔S≤1
43 1 19 42 sylancr ⊢S∈01→0≤1−S↔S≤1
44 41 43 mpbird ⊢S∈01→0≤1−S
45 44 ad2antlr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→0≤1−S
46 45 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤1−S
47 26 28 sqrtge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→0≤∑j=1ND⁡j−F⁡j2
48 47 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤∑j=1ND⁡j−F⁡j2
49 23 30 46 48 mulge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤1−S⁢∑j=1ND⁡j−F⁡j2
50 resqrtth ⊢∑j=1NA⁡j−C⁡j2∈ℝ∧0≤∑j=1NA⁡j−C⁡j2→∑j=1NA⁡j−C⁡j22=∑j=1NA⁡j−C⁡j2
51 12 14 50 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1NA⁡j−C⁡j22=∑j=1NA⁡j−C⁡j2
52 51 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j22=∑j=1NA⁡j−C⁡j2
53 52 oveq2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T2⁢∑j=1NA⁡j−C⁡j22=1−T2⁢∑j=1NA⁡j−C⁡j2
54 ax-1cn ⊢1∈ℂ
55 3 recnd ⊢T∈01→T∈ℂ
56 55 ad2antrr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→T∈ℂ
57 56 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T∈ℂ
58 subcl ⊢1∈ℂ∧T∈ℂ→1−T∈ℂ
59 54 57 58 sylancr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T∈ℂ
60 15 recnd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1NA⁡j−C⁡j2∈ℂ
61 60 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j2∈ℂ
62 59 61 sqmuld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T⁢∑j=1NA⁡j−C⁡j22=1−T2⁢∑j=1NA⁡j−C⁡j22
63 resqrtth ⊢∑j=1ND⁡j−F⁡j2∈ℝ∧0≤∑j=1ND⁡j−F⁡j2→∑j=1ND⁡j−F⁡j22=∑j=1ND⁡j−F⁡j2
64 26 28 63 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1ND⁡j−F⁡j22=∑j=1ND⁡j−F⁡j2
65 64 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1ND⁡j−F⁡j22=∑j=1ND⁡j−F⁡j2
66 65 oveq2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−S2⁢∑j=1ND⁡j−F⁡j22=1−S2⁢∑j=1ND⁡j−F⁡j2
67 19 recnd ⊢S∈01→S∈ℂ
68 67 ad2antlr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→S∈ℂ
69 68 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S∈ℂ
70 subcl ⊢1∈ℂ∧S∈ℂ→1−S∈ℂ
71 54 69 70 sylancr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−S∈ℂ
72 29 recnd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1ND⁡j−F⁡j2∈ℂ
73 72 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1ND⁡j−F⁡j2∈ℂ
74 71 73 sqmuld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−S⁢∑j=1ND⁡j−F⁡j22=1−S2⁢∑j=1ND⁡j−F⁡j22
75 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→BCCgrEF
76 simp122 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→B∈𝔼⁡N
77 simp123 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→C∈𝔼⁡N
78 simp132 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→E∈𝔼⁡N
79 simp133 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→F∈𝔼⁡N
80 brcgr ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCCgrEF↔∑j=1NB⁡j−C⁡j2=∑j=1NE⁡j−F⁡j2
81 76 77 78 79 80 syl22anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→BCCgrEF↔∑j=1NB⁡j−C⁡j2=∑j=1NE⁡j−F⁡j2
82 75 81 mpbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NB⁡j−C⁡j2=∑j=1NE⁡j−F⁡j2
83 simp11 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→N∈ℕ
84 simp121 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→A∈𝔼⁡N
85 simp2ll ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T∈01
86 simp2rl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i
87 ax5seglem2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NB⁡j−C⁡j2=1−T2⁢∑j=1NA⁡j−C⁡j2
88 83 84 77 85 86 87 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NB⁡j−C⁡j2=1−T2⁢∑j=1NA⁡j−C⁡j2
89 simp131 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→D∈𝔼⁡N
90 simp2lr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S∈01
91 simp2rr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i
92 ax5seglem2 ⊢N∈ℕ∧D∈𝔼⁡N∧F∈𝔼⁡N∧S∈01∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→∑j=1NE⁡j−F⁡j2=1−S2⁢∑j=1ND⁡j−F⁡j2
93 83 89 79 90 91 92 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NE⁡j−F⁡j2=1−S2⁢∑j=1ND⁡j−F⁡j2
94 82 88 93 3eqtr3d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T2⁢∑j=1NA⁡j−C⁡j2=1−S2⁢∑j=1ND⁡j−F⁡j2
95 66 74 94 3eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−S⁢∑j=1ND⁡j−F⁡j22=1−T2⁢∑j=1NA⁡j−C⁡j2
96 53 62 95 3eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T⁢∑j=1NA⁡j−C⁡j22=1−S⁢∑j=1ND⁡j−F⁡j22
97 17 31 40 49 96 sq11d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T⁢∑j=1NA⁡j−C⁡j2=1−S⁢∑j=1ND⁡j−F⁡j2
98 3 ad2antrr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→T∈ℝ
99 98 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T∈ℝ
100 99 16 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T⁢∑j=1NA⁡j−C⁡j2∈ℝ
101 19 ad2antlr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→S∈ℝ
102 101 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S∈ℝ
103 102 30 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S⁢∑j=1ND⁡j−F⁡j2∈ℝ
104 2 simp2bi ⊢T∈01→0≤T
105 104 ad2antrr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→0≤T
106 105 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤T
107 99 16 106 39 mulge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤T⁢∑j=1NA⁡j−C⁡j2
108 18 simp2bi ⊢S∈01→0≤S
109 108 ad2antlr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→0≤S
110 109 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤S
111 102 30 110 48 mulge0d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→0≤S⁢∑j=1ND⁡j−F⁡j2
112 51 oveq2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→T2⁢∑j=1NA⁡j−C⁡j22=T2⁢∑j=1NA⁡j−C⁡j2
113 112 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T2⁢∑j=1NA⁡j−C⁡j22=T2⁢∑j=1NA⁡j−C⁡j2
114 57 61 sqmuld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T⁢∑j=1NA⁡j−C⁡j22=T2⁢∑j=1NA⁡j−C⁡j22
115 65 oveq2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S2⁢∑j=1ND⁡j−F⁡j22=S2⁢∑j=1ND⁡j−F⁡j2
116 69 73 sqmuld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S⁢∑j=1ND⁡j−F⁡j22=S2⁢∑j=1ND⁡j−F⁡j22
117 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→ABCgrDE
118 brcgr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABCgrDE↔∑j=1NA⁡j−B⁡j2=∑j=1ND⁡j−E⁡j2
119 84 76 89 78 118 syl22anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→ABCgrDE↔∑j=1NA⁡j−B⁡j2=∑j=1ND⁡j−E⁡j2
120 117 119 mpbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−B⁡j2=∑j=1ND⁡j−E⁡j2
121 ax5seglem1 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NA⁡j−B⁡j2=T2⁢∑j=1NA⁡j−C⁡j2
122 83 84 77 85 86 121 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−B⁡j2=T2⁢∑j=1NA⁡j−C⁡j2
123 ax5seglem1 ⊢N∈ℕ∧D∈𝔼⁡N∧F∈𝔼⁡N∧S∈01∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→∑j=1ND⁡j−E⁡j2=S2⁢∑j=1ND⁡j−F⁡j2
124 83 89 79 90 91 123 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1ND⁡j−E⁡j2=S2⁢∑j=1ND⁡j−F⁡j2
125 120 122 124 3eqtr3d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T2⁢∑j=1NA⁡j−C⁡j2=S2⁢∑j=1ND⁡j−F⁡j2
126 115 116 125 3eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→S⁢∑j=1ND⁡j−F⁡j22=T2⁢∑j=1NA⁡j−C⁡j2
127 113 114 126 3eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T⁢∑j=1NA⁡j−C⁡j22=S⁢∑j=1ND⁡j−F⁡j22
128 100 103 107 111 127 sq11d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→T⁢∑j=1NA⁡j−C⁡j2=S⁢∑j=1ND⁡j−F⁡j2
129 97 128 oveq12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1−T⁢∑j=1NA⁡j−C⁡j2+T⁢∑j=1NA⁡j−C⁡j2=1−S⁢∑j=1ND⁡j−F⁡j2+S⁢∑j=1ND⁡j−F⁡j2
130 59 57 61 adddird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-T+T⁢∑j=1NA⁡j−C⁡j2=1−T⁢∑j=1NA⁡j−C⁡j2+T⁢∑j=1NA⁡j−C⁡j2
131 71 69 73 adddird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-S+S⁢∑j=1ND⁡j−F⁡j2=1−S⁢∑j=1ND⁡j−F⁡j2+S⁢∑j=1ND⁡j−F⁡j2
132 129 130 131 3eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-T+T⁢∑j=1NA⁡j−C⁡j2=1-S+S⁢∑j=1ND⁡j−F⁡j2
133 npcan ⊢1∈ℂ∧T∈ℂ→1-T+T=1
134 54 55 133 sylancr ⊢T∈01→1-T+T=1
135 134 adantr ⊢T∈01∧S∈01→1-T+T=1
136 135 oveq1d ⊢T∈01∧S∈01→1-T+T⁢∑j=1NA⁡j−C⁡j2=1⁢∑j=1NA⁡j−C⁡j2
137 136 adantr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→1-T+T⁢∑j=1NA⁡j−C⁡j2=1⁢∑j=1NA⁡j−C⁡j2
138 137 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-T+T⁢∑j=1NA⁡j−C⁡j2=1⁢∑j=1NA⁡j−C⁡j2
139 60 mullidd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→1⁢∑j=1NA⁡j−C⁡j2=∑j=1NA⁡j−C⁡j2
140 139 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1⁢∑j=1NA⁡j−C⁡j2=∑j=1NA⁡j−C⁡j2
141 138 140 eqtrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-T+T⁢∑j=1NA⁡j−C⁡j2=∑j=1NA⁡j−C⁡j2
142 npcan ⊢1∈ℂ∧S∈ℂ→1-S+S=1
143 54 67 142 sylancr ⊢S∈01→1-S+S=1
144 143 oveq1d ⊢S∈01→1-S+S⁢∑j=1ND⁡j−F⁡j2=1⁢∑j=1ND⁡j−F⁡j2
145 144 ad2antlr ⊢T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i→1-S+S⁢∑j=1ND⁡j−F⁡j2=1⁢∑j=1ND⁡j−F⁡j2
146 145 3ad2ant2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-S+S⁢∑j=1ND⁡j−F⁡j2=1⁢∑j=1ND⁡j−F⁡j2
147 72 mullidd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→1⁢∑j=1ND⁡j−F⁡j2=∑j=1ND⁡j−F⁡j2
148 147 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1⁢∑j=1ND⁡j−F⁡j2=∑j=1ND⁡j−F⁡j2
149 146 148 eqtrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→1-S+S⁢∑j=1ND⁡j−F⁡j2=∑j=1ND⁡j−F⁡j2
150 132 141 149 3eqtr3d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2
151 sqrt11 ⊢∑j=1NA⁡j−C⁡j2∈ℝ∧0≤∑j=1NA⁡j−C⁡j2∧∑j=1ND⁡j−F⁡j2∈ℝ∧0≤∑j=1ND⁡j−F⁡j2→∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2↔∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2
152 12 14 26 28 151 syl22anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2↔∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2
153 152 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2↔∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2
154 150 153 mpbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧T∈01∧S∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧∀i∈1…NE⁡i=1−S⁢D⁡i+S⁢F⁡i∧ABCgrDE∧BCCgrEF→∑j=1NA⁡j−C⁡j2=∑j=1ND⁡j−F⁡j2