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 ) ) )