Metamath Proof Explorer

Theorem ax5seglem1

Description: Lemma for ax5seg . Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
2 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
3 1 2 sylancom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
4 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
6 4 5 sylancom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
7 elicc01 ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1 ) )
8 7 simp1bi ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℝ )
9 8 adantr ⊢ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) → 𝑇 ∈ ℝ )
10 9 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → 𝑇 ∈ ℝ )
11 10 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → 𝑇 ∈ ℂ )
12 11 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑇 ∈ ℂ )
13 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑗 ) )
14 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑗 ) )
15 14 oveq2d ⊢ ( 𝑖 = 𝑗 → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) )
16 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) )
17 16 oveq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) = ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) )
18 15 17 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
19 13 18 eqeq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) )
20 19 rspccva ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
21 20 adantll ⊢ ( ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
22 21 3ad2antl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
23 oveq2 ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) = ( ( 𝐴 ‘ 𝑗 ) − ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) )
24 23 oveq1d ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑗 ) − ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) ↑ 2 ) )
25 subdi ⊢ ( ( 𝑇 ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( 𝑇 · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
26 25 3coml ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝑇 · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
27 ax-1cn ⊢ 1 ∈ ℂ
28 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
29 27 28 mpan ⊢ ( 𝑇 ∈ ℂ → ( 1 − 𝑇 ) ∈ ℂ )
30 29 adantl ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
31 simpl ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
32 subdir ⊢ ( ( 1 ∈ ℂ ∧ ( 1 − 𝑇 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐴 ‘ 𝑗 ) ) = ( ( 1 · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) )
33 27 30 31 32 mp3an2i ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐴 ‘ 𝑗 ) ) = ( ( 1 · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) )
34 nncan ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
35 27 34 mpan ⊢ ( 𝑇 ∈ ℂ → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
36 35 oveq1d ⊢ ( 𝑇 ∈ ℂ → ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐴 ‘ 𝑗 ) ) = ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) )
37 36 adantl ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − ( 1 − 𝑇 ) ) · ( 𝐴 ‘ 𝑗 ) ) = ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) )
38 mullid ⊢ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ → ( 1 · ( 𝐴 ‘ 𝑗 ) ) = ( 𝐴 ‘ 𝑗 ) )
39 38 oveq1d ⊢ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ → ( ( 1 · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) = ( ( 𝐴 ‘ 𝑗 ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) )
40 39 adantr ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) = ( ( 𝐴 ‘ 𝑗 ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) )
41 33 37 40 3eqtr3rd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑗 ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) = ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) )
42 41 oveq1d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
43 42 3adant2 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝑇 · ( 𝐴 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
44 simp1 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
45 mulcl ⊢ ( ( ( 1 − 𝑇 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
46 29 45 sylan ⊢ ( ( 𝑇 ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
47 46 ancoms ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
48 47 3adant2 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
49 mulcl ⊢ ( ( 𝑇 ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
50 49 ancoms ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
51 50 3adant1 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
52 44 48 51 subsub4d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝐴 ‘ 𝑗 ) − ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) )
53 26 43 52 3eqtr2rd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑗 ) − ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) = ( 𝑇 · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) )
54 53 oveq1d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) ↑ 2 ) = ( ( 𝑇 · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) ↑ 2 ) )
55 simp3 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → 𝑇 ∈ ℂ )
56 subcl ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
57 56 3adant3 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
58 55 57 sqmuld ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 𝑇 · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
59 54 58 eqtrd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
60 24 59 sylan9eqr ⊢ ( ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
61 3 6 12 22 60 syl31anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
62 61 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
63 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
64 8 resqcld ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 𝑇 ↑ 2 ) ∈ ℝ )
65 64 recnd ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 𝑇 ↑ 2 ) ∈ ℂ )
66 65 adantr ⊢ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( 𝑇 ↑ 2 ) ∈ ℂ )
67 66 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝑇 ↑ 2 ) ∈ ℂ )
68 2 3adant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
69 68 3adant2r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
70 5 3adant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
71 70 3adant2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
72 69 71 subcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
73 72 sqcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
74 73 3expa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
75 74 3adantl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
76 63 67 75 fsummulc2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
77 62 76 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )