Metamath Proof Explorer

Theorem ax5seglem9

Description: Lemma for ax5seg . Take the calculation in ax5seglem8 and turn it into a series of measurements. (Contributed by Scott Fenton, 12-Jun-2013) (Revised by Mario Carneiro, 22-May-2014)

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

Proof

Step Hyp Ref Expression
1 simprll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
2 1 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
4 2 3 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
5 elicc01 ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1 ) )
6 5 simp1bi ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℝ )
7 6 recnd ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℂ )
8 7 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → 𝑇 ∈ ℂ )
9 8 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑇 ∈ ℂ )
10 simprrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
11 10 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
12 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
13 11 12 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
14 simprrr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
15 14 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
16 fveecn ⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ℂ )
17 15 16 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ℂ )
18 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑗 ) )
19 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑗 ) )
20 19 oveq2d ⊢ ( 𝑖 = 𝑗 → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) )
21 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) )
22 21 oveq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) = ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) )
23 20 22 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
24 18 23 eqeq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) )
25 24 rspccva ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
26 25 adantll ⊢ ( ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
27 26 adantll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) )
28 ax5seglem8 ⊢ ( ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℂ ) ) → ( 𝑇 · ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
29 oveq1 ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) = ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐷 ‘ 𝑗 ) ) )
30 29 oveq1d ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) = ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) )
31 30 oveq1d ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
32 31 eqcomd ⊢ ( ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) → ( ( ( ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) = ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
33 28 32 sylan9eq ⊢ ( ( ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℂ ) ) ∧ ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) → ( 𝑇 · ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
34 33 3impa ⊢ ( ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℂ ) ∧ ( 𝐵 ‘ 𝑗 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑗 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑗 ) ) ) ) → ( 𝑇 · ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
35 4 9 13 17 27 34 syl221anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 · ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
36 35 sumeq2dv ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
37 fzfid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
38 13 17 subcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ∈ ℂ )
39 38 sqcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
40 37 8 39 fsummulc2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) )
41 4 13 subcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
42 41 sqcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
43 37 8 42 fsummulc2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
44 43 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) )
45 9 42 mulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) ∈ ℂ )
46 4 17 subcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ∈ ℂ )
47 46 sqcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
48 37 45 47 fsumsub ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) )
49 44 48 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) )
50 49 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 1 − 𝑇 ) · ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) = ( ( 1 − 𝑇 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) )
51 ax-1cn ⊢ 1 ∈ ℂ
52 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
53 51 8 52 sylancr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 1 − 𝑇 ) ∈ ℂ )
54 45 47 subcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ∈ ℂ )
55 37 53 54 fsummulc2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 1 − 𝑇 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) )
56 50 55 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( ( 1 − 𝑇 ) · ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) )
57 56 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
58 simprlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
59 58 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
60 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ℂ )
61 59 60 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ℂ )
62 61 17 subcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ∈ ℂ )
63 62 sqcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
64 51 9 52 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑇 ) ∈ ℂ )
65 64 54 mulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ∈ ℂ )
66 37 63 65 fsumadd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
67 57 66 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )
68 36 40 67 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) − Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐷 ‘ 𝑗 ) ) ↑ 2 ) ) ) ) )