Metamath Proof Explorer

Theorem ax5seglem2

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

Ref Expression
Assertion ax5seglem2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 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 recnd ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℂ )
10 9 adantr ⊢ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) → 𝑇 ∈ ℂ )
11 10 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 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 oveq1 ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) = ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐶 ‘ 𝑗 ) ) )
24 23 oveq1d ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) )
25 ax-1cn ⊢ 1 ∈ ℂ
26 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
27 25 26 mpan ⊢ ( 𝑇 ∈ ℂ → ( 1 − 𝑇 ) ∈ ℂ )
28 27 3ad2ant3 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
29 simp1 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
30 28 29 mulcld ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
31 simp3 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → 𝑇 ∈ ℂ )
32 simp2 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
33 31 32 mulcld ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
34 30 33 32 addsubassd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐶 ‘ 𝑗 ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝐶 ‘ 𝑗 ) ) ) )
35 subdi ⊢ ( ( ( 1 − 𝑇 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) ) )
36 27 35 syl3an1 ⊢ ( ( 𝑇 ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) ) )
37 36 3coml ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) ) )
38 subdir ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) = ( ( 1 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
39 25 38 mp3an1 ⊢ ( ( 𝑇 ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) = ( ( 1 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
40 39 ancoms ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) = ( ( 1 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
41 40 3adant1 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) = ( ( 1 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
42 mulid2 ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ → ( 1 · ( 𝐶 ‘ 𝑗 ) ) = ( 𝐶 ‘ 𝑗 ) )
43 42 oveq1d ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ → ( ( 1 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
44 43 3ad2ant2 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
45 41 44 eqtrd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) = ( ( 𝐶 ‘ 𝑗 ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
46 45 oveq2d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 1 − 𝑇 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑗 ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) )
47 30 32 33 subsub2d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑗 ) − ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝐶 ‘ 𝑗 ) ) ) )
48 37 46 47 3eqtrd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) − ( 𝐶 ‘ 𝑗 ) ) ) )
49 34 48 eqtr4d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐶 ‘ 𝑗 ) ) = ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) )
50 49 oveq1d ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) ↑ 2 ) )
51 subcl ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
52 51 3adant3 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
53 28 52 sqmuld ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
54 50 53 eqtrd ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
55 24 54 sylan9eqr ⊢ ( ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
56 3 6 12 22 55 syl31anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
57 56 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
58 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
59 1re ⊢ 1 ∈ ℝ
60 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → ( 1 − 𝑇 ) ∈ ℝ )
61 59 8 60 sylancr ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ℝ )
62 61 resqcld ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( 1 − 𝑇 ) ↑ 2 ) ∈ ℝ )
63 62 recnd ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( 1 − 𝑇 ) ↑ 2 ) ∈ ℂ )
64 63 adantr ⊢ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( ( 1 − 𝑇 ) ↑ 2 ) ∈ ℂ )
65 64 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 1 − 𝑇 ) ↑ 2 ) ∈ ℂ )
66 2 3adant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
67 66 3adant2r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
68 5 3adant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
69 68 3adant2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
70 67 69 subcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
71 70 sqcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
72 71 3expa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
73 72 3adantl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
74 58 65 73 fsummulc2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( ( 1 − 𝑇 ) ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
75 57 74 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )