Metamath Proof Explorer

Theorem axsegconlem9

Description: Lemma for axsegcon . Show that B F is congruent to C D . (Contributed by Scott Fenton, 19-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 ⊢S=∑p=1NA⁡p−B⁡p2
axsegconlem7.2 ⊢T=∑p=1NC⁡p−D⁡p2
axsegconlem8.3 ⊢F=k∈1…N⟼S+T⁢B⁡k−T⁢A⁡kS
Assertion axsegconlem9 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NB⁡i−F⁡i2=∑i=1NC⁡i−D⁡i2

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢S=∑p=1NA⁡p−B⁡p2
2 axsegconlem7.2 ⊢T=∑p=1NC⁡p−D⁡p2
3 axsegconlem8.3 ⊢F=k∈1…N⟼S+T⁢B⁡k−T⁢A⁡kS
4 fveq2 ⊢k=i→B⁡k=B⁡i
5 4 oveq2d ⊢k=i→S+T⁢B⁡k=S+T⁢B⁡i
6 fveq2 ⊢k=i→A⁡k=A⁡i
7 6 oveq2d ⊢k=i→T⁢A⁡k=T⁢A⁡i
8 5 7 oveq12d ⊢k=i→S+T⁢B⁡k−T⁢A⁡k=S+T⁢B⁡i−T⁢A⁡i
9 8 oveq1d ⊢k=i→S+T⁢B⁡k−T⁢A⁡kS=S+T⁢B⁡i−T⁢A⁡iS
10 ovex ⊢S+T⁢B⁡i−T⁢A⁡iS∈V
11 9 3 10 fvmpt ⊢i∈1…N→F⁡i=S+T⁢B⁡i−T⁢A⁡iS
12 11 adantl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→F⁡i=S+T⁢B⁡i−T⁢A⁡iS
13 12 oveq2d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−F⁡i=B⁡i−S+T⁢B⁡i−T⁢A⁡iS
14 1 axsegconlem4 ⊢A∈𝔼⁡N∧B∈𝔼⁡N→S∈ℝ
15 14 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→S∈ℝ
16 15 ad2antrr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S∈ℝ
17 simpl2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→B∈𝔼⁡N
18 fveere ⊢B∈𝔼⁡N∧i∈1…N→B⁡i∈ℝ
19 17 18 sylan ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i∈ℝ
20 16 19 remulcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i∈ℝ
21 20 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i∈ℂ
22 2 axsegconlem4 ⊢C∈𝔼⁡N∧D∈𝔼⁡N→T∈ℝ
23 readdcl ⊢S∈ℝ∧T∈ℝ→S+T∈ℝ
24 15 22 23 syl2an ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→S+T∈ℝ
25 24 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T∈ℝ
26 25 19 remulcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T⁢B⁡i∈ℝ
27 22 ad2antlr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T∈ℝ
28 simpl1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→A∈𝔼⁡N
29 fveere ⊢A∈𝔼⁡N∧i∈1…N→A⁡i∈ℝ
30 28 29 sylan ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i∈ℝ
31 27 30 remulcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i∈ℝ
32 26 31 resubcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T⁢B⁡i−T⁢A⁡i∈ℝ
33 32 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T⁢B⁡i−T⁢A⁡i∈ℂ
34 16 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S∈ℂ
35 1 axsegconlem6 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→0<S
36 35 gt0ne0d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→S≠0
37 36 ad2antrr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S≠0
38 21 33 34 37 divsubdird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i−S+T⁢B⁡i−T⁢A⁡iS=S⁢B⁡iS−S+T⁢B⁡i−T⁢A⁡iS
39 26 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T⁢B⁡i∈ℂ
40 31 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i∈ℂ
41 21 39 40 subsubd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i−S+T⁢B⁡i−T⁢A⁡i=S⁢B⁡i-S+T⁢B⁡i+T⁢A⁡i
42 27 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T∈ℂ
43 19 renegcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→−B⁡i∈ℝ
44 43 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→−B⁡i∈ℂ
45 30 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i∈ℂ
46 42 44 45 adddid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢-B⁡i+A⁡i=T⁢−B⁡i+T⁢A⁡i
47 44 45 addcomd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→-B⁡i+A⁡i=A⁡i+−B⁡i
48 19 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i∈ℂ
49 45 48 negsubd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i+−B⁡i=A⁡i−B⁡i
50 47 49 eqtrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→-B⁡i+A⁡i=A⁡i−B⁡i
51 50 oveq2d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢-B⁡i+A⁡i=T⁢A⁡i−B⁡i
52 25 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T∈ℂ
53 52 34 negsubdi2d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→−S+T-S=S−S+T
54 34 42 pncan2d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S+T-S=T
55 54 negeqd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→−S+T-S=−T
56 53 55 eqtr3d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S−S+T=−T
57 56 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S−S+T⁢B⁡i=−T⁢B⁡i
58 34 52 48 subdird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S−S+T⁢B⁡i=S⁢B⁡i−S+T⁢B⁡i
59 mulneg12 ⊢T∈ℂ∧B⁡i∈ℂ→−T⁢B⁡i=T⁢−B⁡i
60 42 48 59 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→−T⁢B⁡i=T⁢−B⁡i
61 57 58 60 3eqtr3rd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢−B⁡i=S⁢B⁡i−S+T⁢B⁡i
62 61 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢−B⁡i+T⁢A⁡i=S⁢B⁡i-S+T⁢B⁡i+T⁢A⁡i
63 46 51 62 3eqtr3rd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i-S+T⁢B⁡i+T⁢A⁡i=T⁢A⁡i−B⁡i
64 41 63 eqtrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i−S+T⁢B⁡i−T⁢A⁡i=T⁢A⁡i−B⁡i
65 64 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡i−S+T⁢B⁡i−T⁢A⁡iS=T⁢A⁡i−B⁡iS
66 48 34 37 divcan3d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡iS=B⁡i
67 66 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S⁢B⁡iS−S+T⁢B⁡i−T⁢A⁡iS=B⁡i−S+T⁢B⁡i−T⁢A⁡iS
68 38 65 67 3eqtr3rd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−S+T⁢B⁡i−T⁢A⁡iS=T⁢A⁡i−B⁡iS
69 13 68 eqtrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−F⁡i=T⁢A⁡i−B⁡iS
70 69 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−F⁡i2=T⁢A⁡i−B⁡iS2
71 30 19 resubcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i∈ℝ
72 27 71 remulcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i∈ℝ
73 72 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i∈ℂ
74 73 34 37 sqdivd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡iS2=T⁢A⁡i−B⁡i2S2
75 71 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i∈ℂ
76 42 75 sqmuld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i2=T2⁢A⁡i−B⁡i2
77 2 axsegconlem2 ⊢C∈𝔼⁡N∧D∈𝔼⁡N→T∈ℝ
78 77 ad2antlr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T∈ℝ
79 2 axsegconlem3 ⊢C∈𝔼⁡N∧D∈𝔼⁡N→0≤T
80 79 ad2antlr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→0≤T
81 resqrtth ⊢T∈ℝ∧0≤T→T2=T
82 78 80 81 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T2=T
83 82 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T2⁢A⁡i−B⁡i2=T⁢A⁡i−B⁡i2
84 76 83 eqtrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i2=T⁢A⁡i−B⁡i2
85 1 axsegconlem2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N→S∈ℝ
86 1 axsegconlem3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N→0≤S
87 resqrtth ⊢S∈ℝ∧0≤S→S2=S
88 85 86 87 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N→S2=S
89 88 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→S2=S
90 89 ad2antrr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→S2=S
91 84 90 oveq12d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i2S2=T⁢A⁡i−B⁡i2S
92 70 74 91 3eqtrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−F⁡i2=T⁢A⁡i−B⁡i2S
93 92 sumeq2dv ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NB⁡i−F⁡i2=∑i=1NT⁢A⁡i−B⁡i2S
94 fzfid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→1…N∈Fin
95 77 adantl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T∈ℝ
96 95 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T∈ℂ
97 71 resqcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i2∈ℝ
98 97 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i2∈ℂ
99 94 96 98 fsummulc2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T⁢∑i=1NA⁡i−B⁡i2=∑i=1NT⁢A⁡i−B⁡i2
100 99 oveq1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T⁢∑i=1NA⁡i−B⁡i2S=∑i=1NT⁢A⁡i−B⁡i2S
101 fveq2 ⊢p=i→C⁡p=C⁡i
102 fveq2 ⊢p=i→D⁡p=D⁡i
103 101 102 oveq12d ⊢p=i→C⁡p−D⁡p=C⁡i−D⁡i
104 103 oveq1d ⊢p=i→C⁡p−D⁡p2=C⁡i−D⁡i2
105 104 cbvsumv ⊢∑p=1NC⁡p−D⁡p2=∑i=1NC⁡i−D⁡i2
106 2 105 eqtri ⊢T=∑i=1NC⁡i−D⁡i2
107 fveq2 ⊢i=p→A⁡i=A⁡p
108 fveq2 ⊢i=p→B⁡i=B⁡p
109 107 108 oveq12d ⊢i=p→A⁡i−B⁡i=A⁡p−B⁡p
110 109 oveq1d ⊢i=p→A⁡i−B⁡i2=A⁡p−B⁡p2
111 110 cbvsumv ⊢∑i=1NA⁡i−B⁡i2=∑p=1NA⁡p−B⁡p2
112 111 1 eqtr4i ⊢∑i=1NA⁡i−B⁡i2=S
113 106 112 oveq12i ⊢T⁢∑i=1NA⁡i−B⁡i2=∑i=1NC⁡i−D⁡i2⁢S
114 eqid ⊢∑i=1NA⁡i−B⁡i2=∑i=1NA⁡i−B⁡i2
115 114 axsegconlem2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N→∑i=1NA⁡i−B⁡i2∈ℝ
116 115 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→∑i=1NA⁡i−B⁡i2∈ℝ
117 116 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NA⁡i−B⁡i2∈ℝ
118 95 117 remulcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T⁢∑i=1NA⁡i−B⁡i2∈ℝ
119 118 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T⁢∑i=1NA⁡i−B⁡i2∈ℂ
120 eqid ⊢∑i=1NC⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2
121 120 axsegconlem2 ⊢C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NC⁡i−D⁡i2∈ℝ
122 121 adantl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NC⁡i−D⁡i2∈ℝ
123 122 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NC⁡i−D⁡i2∈ℂ
124 85 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→S∈ℝ
125 124 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→S∈ℝ
126 125 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→S∈ℂ
127 86 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→0≤S
128 sqrt00 ⊢S∈ℝ∧0≤S→S=0↔S=0
129 128 necon3bid ⊢S∈ℝ∧0≤S→S≠0↔S≠0
130 124 127 129 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→S≠0↔S≠0
131 36 130 mpbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→S≠0
132 131 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→S≠0
133 119 123 126 132 divmul3d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T⁢∑i=1NA⁡i−B⁡i2S=∑i=1NC⁡i−D⁡i2↔T⁢∑i=1NA⁡i−B⁡i2=∑i=1NC⁡i−D⁡i2⁢S
134 113 133 mpbiri ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→T⁢∑i=1NA⁡i−B⁡i2S=∑i=1NC⁡i−D⁡i2
135 78 97 remulcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i2∈ℝ
136 135 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→T⁢A⁡i−B⁡i2∈ℂ
137 94 126 136 132 fsumdivc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NT⁢A⁡i−B⁡i2S=∑i=1NT⁢A⁡i−B⁡i2S
138 100 134 137 3eqtr3rd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NT⁢A⁡i−B⁡i2S=∑i=1NC⁡i−D⁡i2
139 93 138 eqtrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NB⁡i−F⁡i2=∑i=1NC⁡i−D⁡i2