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		mullid	⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ℂ → ( 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 ) ) )