Theorem ax5seglem7

Description: Lemma for ax5seg . An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013)

	Ref	Expression
Hypotheses	ax5seglem7.1	⊢ 𝐴 ∈ ℂ
	ax5seglem7.2	⊢ 𝑇 ∈ ℂ
	ax5seglem7.3	⊢ 𝐶 ∈ ℂ
	ax5seglem7.4	⊢ 𝐷 ∈ ℂ
Assertion	ax5seglem7	⊢ ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax5seglem7.1	⊢ 𝐴 ∈ ℂ
2		ax5seglem7.2	⊢ 𝑇 ∈ ℂ
3		ax5seglem7.3	⊢ 𝐶 ∈ ℂ
4		ax5seglem7.4	⊢ 𝐷 ∈ ℂ
5	3 4	binom2subi	⊢ ( ( 𝐶 − 𝐷 ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) )
6	5	oveq2i	⊢ ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( 𝑇 · ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) )
7	3	sqcli	⊢ ( 𝐶 ↑ 2 ) ∈ ℂ
8		2cn	⊢ 2 ∈ ℂ
9	3 4	mulcli	⊢ ( 𝐶 · 𝐷 ) ∈ ℂ
10	8 9	mulcli	⊢ ( 2 · ( 𝐶 · 𝐷 ) ) ∈ ℂ
11	7 10	subcli	⊢ ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) ∈ ℂ
12	4	sqcli	⊢ ( 𝐷 ↑ 2 ) ∈ ℂ
13	2 11 12	adddii	⊢ ( 𝑇 · ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) ) = ( ( 𝑇 · ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
14	2 7 10	subdii	⊢ ( 𝑇 · ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) ) = ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) )
15	14	oveq1i	⊢ ( ( 𝑇 · ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
16	6 13 15	3eqtri	⊢ ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
17		ax-1cn	⊢ 1 ∈ ℂ
18	17 2	subcli	⊢ ( 1 − 𝑇 ) ∈ ℂ
19	18 1	mulcli	⊢ ( ( 1 − 𝑇 ) · 𝐴 ) ∈ ℂ
20	19	sqcli	⊢ ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) ∈ ℂ
21	2 3	mulcli	⊢ ( 𝑇 · 𝐶 ) ∈ ℂ
22	21 4	subcli	⊢ ( ( 𝑇 · 𝐶 ) − 𝐷 ) ∈ ℂ
23	19 22	mulcli	⊢ ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ∈ ℂ
24	8 23	mulcli	⊢ ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ∈ ℂ
25	20 24	addcli	⊢ ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) ∈ ℂ
26	21	sqcli	⊢ ( ( 𝑇 · 𝐶 ) ↑ 2 ) ∈ ℂ
27	26 12	addcli	⊢ ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ
28	25 27	addcli	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℂ
29	21 4	mulcli	⊢ ( ( 𝑇 · 𝐶 ) · 𝐷 ) ∈ ℂ
30	8 29	mulcli	⊢ ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ∈ ℂ
31	2 7	mulcli	⊢ ( 𝑇 · ( 𝐶 ↑ 2 ) ) ∈ ℂ
32	2 12	mulcli	⊢ ( 𝑇 · ( 𝐷 ↑ 2 ) ) ∈ ℂ
33	31 32	addcli	⊢ ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ∈ ℂ
34		subadd23	⊢ ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℂ ∧ ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ∈ ℂ ∧ ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ∈ ℂ ) → ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ) )
35	28 30 33 34	mp3an	⊢ ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) )
36	35	oveq1i	⊢ ( ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) = ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
37	19 22	binom2i	⊢ ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ↑ 2 ) = ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) − 𝐷 ) ↑ 2 ) )
38	19 21 4	addsubassi	⊢ ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) = ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( ( 𝑇 · 𝐶 ) − 𝐷 ) )
39	38	oveq1i	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) = ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ↑ 2 )
40	25 27 30	addsubassi	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) = ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) )
41	21 4	binom2subi	⊢ ( ( ( 𝑇 · 𝐶 ) − 𝐷 ) ↑ 2 ) = ( ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) )
42	26 12 30	addsubi	⊢ ( ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) = ( ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) )
43	41 42	eqtr4i	⊢ ( ( ( 𝑇 · 𝐶 ) − 𝐷 ) ↑ 2 ) = ( ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) )
44	43	oveq2i	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) )
45	40 44	eqtr4i	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) = ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) − 𝐷 ) ↑ 2 ) )
46	37 39 45	3eqtr4i	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) )
47	1 3	binom2subi	⊢ ( ( 𝐴 − 𝐶 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) )
48	47	oveq2i	⊢ ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) = ( 𝑇 · ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) )
49	1	sqcli	⊢ ( 𝐴 ↑ 2 ) ∈ ℂ
50	1 3	mulcli	⊢ ( 𝐴 · 𝐶 ) ∈ ℂ
51	8 50	mulcli	⊢ ( 2 · ( 𝐴 · 𝐶 ) ) ∈ ℂ
52	49 51	subcli	⊢ ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ
53	2 52 7	adddii	⊢ ( 𝑇 · ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) ) = ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) + ( 𝑇 · ( 𝐶 ↑ 2 ) ) )
54	48 53	eqtri	⊢ ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) = ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) + ( 𝑇 · ( 𝐶 ↑ 2 ) ) )
55	1 4	binom2subi	⊢ ( ( 𝐴 − 𝐷 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) )
56	54 55	oveq12i	⊢ ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) = ( ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) + ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) )
57	2 52	mulcli	⊢ ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ∈ ℂ
58	1 4	mulcli	⊢ ( 𝐴 · 𝐷 ) ∈ ℂ
59	8 58	mulcli	⊢ ( 2 · ( 𝐴 · 𝐷 ) ) ∈ ℂ
60	49 59	subcli	⊢ ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ∈ ℂ
61	57 31 60 12	addsub4i	⊢ ( ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) + ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) )
62	56 61	eqtri	⊢ ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) = ( ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) )
63	62	oveq2i	⊢ ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) = ( ( 1 − 𝑇 ) · ( ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) )
64	57 60	subcli	⊢ ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ∈ ℂ
65	31 12	subcli	⊢ ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ∈ ℂ
66	18 64 65	adddii	⊢ ( ( 1 − 𝑇 ) · ( ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) )
67	17 2 65	subdiri	⊢ ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) = ( ( 1 · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) )
68	65	mullidi	⊢ ( 1 · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) = ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) )
69	2 31 12	subdii	⊢ ( 𝑇 · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) = ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
70	68 69	oveq12i	⊢ ( ( 1 · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) − ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) )
71	2 31	mulcli	⊢ ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ∈ ℂ
72		subsub3	⊢ ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ∈ ℂ ∧ ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ∈ ℂ ∧ ( 𝑇 · ( 𝐷 ↑ 2 ) ) ∈ ℂ ) → ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) − ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) )
73	65 71 32 72	mp3an	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) − ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) )
74	31 32 12	addsubi	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝐷 ↑ 2 ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
75	74	oveq1i	⊢ ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝐷 ↑ 2 ) ) − ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) = ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) )
76		subsub4	⊢ ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ∈ ℂ ∧ ( 𝐷 ↑ 2 ) ∈ ℂ ∧ ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ∈ ℂ ) → ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝐷 ↑ 2 ) ) − ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
77	33 12 71 76	mp3an	⊢ ( ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝐷 ↑ 2 ) ) − ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) )
78	73 75 77	3eqtr2i	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) − ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) )
79	67 70 78	3eqtri	⊢ ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) )
80	79	oveq2i	⊢ ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
81	18 64	mulcli	⊢ ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ∈ ℂ
82	12 71	addcli	⊢ ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ∈ ℂ
83		addsub12	⊢ ( ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ∈ ℂ ∧ ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ∈ ℂ ) → ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) )
84	81 33 82 83	mp3an	⊢ ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
85	80 84	eqtri	⊢ ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
86	63 66 85	3eqtri	⊢ ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
87	46 86	oveq12i	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) )
88	28 30	subcli	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ∈ ℂ
89	81 82	subcli	⊢ ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ∈ ℂ
90	88 33 89	addassi	⊢ ( ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) = ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) )
91	87 90	eqtr4i	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) + ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
92	33 30	subcli	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ∈ ℂ
93	28 89 92	add32i	⊢ ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ) = ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
94	36 91 93	3eqtr4i	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) )
95		subsub2	⊢ ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ∈ ℂ ) → ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) )
96	28 82 81 95	mp3an	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) )
97	25 26 12	addassi	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) + ( 𝐷 ↑ 2 ) ) = ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
98	25 26	addcomi	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) = ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) )
99	2 3	sqmuli	⊢ ( ( 𝑇 · 𝐶 ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · ( 𝐶 ↑ 2 ) )
100	2	sqvali	⊢ ( 𝑇 ↑ 2 ) = ( 𝑇 · 𝑇 )
101	100	oveq1i	⊢ ( ( 𝑇 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) = ( ( 𝑇 · 𝑇 ) · ( 𝐶 ↑ 2 ) )
102	2 2 7	mulassi	⊢ ( ( 𝑇 · 𝑇 ) · ( 𝐶 ↑ 2 ) ) = ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) )
103	99 101 102	3eqtri	⊢ ( ( 𝑇 · 𝐶 ) ↑ 2 ) = ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) )
104	18 1	sqmuli	⊢ ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) = ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( 𝐴 ↑ 2 ) )
105	18	sqvali	⊢ ( ( 1 − 𝑇 ) ↑ 2 ) = ( ( 1 − 𝑇 ) · ( 1 − 𝑇 ) )
106	105	oveq1i	⊢ ( ( ( 1 − 𝑇 ) ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( ( ( 1 − 𝑇 ) · ( 1 − 𝑇 ) ) · ( 𝐴 ↑ 2 ) )
107	18 18 49	mulassi	⊢ ( ( ( 1 − 𝑇 ) · ( 1 − 𝑇 ) ) · ( 𝐴 ↑ 2 ) ) = ( ( 1 − 𝑇 ) · ( ( 1 − 𝑇 ) · ( 𝐴 ↑ 2 ) ) )
108	17 2 49	subdiri	⊢ ( ( 1 − 𝑇 ) · ( 𝐴 ↑ 2 ) ) = ( ( 1 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) )
109	49	mullidi	⊢ ( 1 · ( 𝐴 ↑ 2 ) ) = ( 𝐴 ↑ 2 )
110	109	oveq1i	⊢ ( ( 1 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) )
111	108 110	eqtri	⊢ ( ( 1 − 𝑇 ) · ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) )
112	111	oveq2i	⊢ ( ( 1 − 𝑇 ) · ( ( 1 − 𝑇 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( 1 − 𝑇 ) · ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) )
113	107 112	eqtri	⊢ ( ( ( 1 − 𝑇 ) · ( 1 − 𝑇 ) ) · ( 𝐴 ↑ 2 ) ) = ( ( 1 − 𝑇 ) · ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) )
114	104 106 113	3eqtri	⊢ ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) = ( ( 1 − 𝑇 ) · ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) )
115	8 19 22	mul12i	⊢ ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) = ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) )
116	8 22	mulcli	⊢ ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ∈ ℂ
117	18 1 116	mulassi	⊢ ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) = ( ( 1 − 𝑇 ) · ( 𝐴 · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) )
118	1 8	mulcomi	⊢ ( 𝐴 · 2 ) = ( 2 · 𝐴 )
119	118	oveq1i	⊢ ( ( 𝐴 · 2 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) = ( ( 2 · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) )
120	1 8 22	mulassi	⊢ ( ( 𝐴 · 2 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) = ( 𝐴 · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) )
121	119 120	eqtr3i	⊢ ( ( 2 · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) = ( 𝐴 · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) )
122	8 1	mulcli	⊢ ( 2 · 𝐴 ) ∈ ℂ
123	122 21 4	subdii	⊢ ( ( 2 · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝑇 · 𝐶 ) ) − ( ( 2 · 𝐴 ) · 𝐷 ) )
124	122 2 3	mul12i	⊢ ( ( 2 · 𝐴 ) · ( 𝑇 · 𝐶 ) ) = ( 𝑇 · ( ( 2 · 𝐴 ) · 𝐶 ) )
125	8 1 3	mulassi	⊢ ( ( 2 · 𝐴 ) · 𝐶 ) = ( 2 · ( 𝐴 · 𝐶 ) )
126	125	oveq2i	⊢ ( 𝑇 · ( ( 2 · 𝐴 ) · 𝐶 ) ) = ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) )
127	124 126	eqtri	⊢ ( ( 2 · 𝐴 ) · ( 𝑇 · 𝐶 ) ) = ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) )
128	8 1 4	mulassi	⊢ ( ( 2 · 𝐴 ) · 𝐷 ) = ( 2 · ( 𝐴 · 𝐷 ) )
129	127 128	oveq12i	⊢ ( ( ( 2 · 𝐴 ) · ( 𝑇 · 𝐶 ) ) − ( ( 2 · 𝐴 ) · 𝐷 ) ) = ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) )
130	123 129	eqtri	⊢ ( ( 2 · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) = ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) )
131	121 130	eqtr3i	⊢ ( 𝐴 · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) = ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) )
132	131	oveq2i	⊢ ( ( 1 − 𝑇 ) · ( 𝐴 · ( 2 · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) = ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) )
133	115 117 132	3eqtri	⊢ ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) = ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) )
134	114 133	oveq12i	⊢ ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) = ( ( ( 1 − 𝑇 ) · ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) )
135	2 49	mulcli	⊢ ( 𝑇 · ( 𝐴 ↑ 2 ) ) ∈ ℂ
136	49 135	subcli	⊢ ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) ∈ ℂ
137	2 51	mulcli	⊢ ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ
138	137 59	subcli	⊢ ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ∈ ℂ
139	18 136 138	adddii	⊢ ( ( 1 − 𝑇 ) · ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) = ( ( ( 1 − 𝑇 ) · ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) )
140	2 49 51	subdii	⊢ ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) = ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) )
141	140	oveq2i	⊢ ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) )
142	140 57	eqeltrri	⊢ ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ∈ ℂ
143		sub32	⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ∈ ℂ ∧ ( 2 · ( 𝐴 · 𝐷 ) ) ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) )
144	49 142 59 143	mp3an	⊢ ( ( ( 𝐴 ↑ 2 ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) )
145	141 144	eqtr4i	⊢ ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) )
146		subsub	⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 𝑇 · ( 𝐴 ↑ 2 ) ) ∈ ℂ ∧ ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) )
147	49 135 137 146	mp3an	⊢ ( ( 𝐴 ↑ 2 ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) )
148	147	oveq1i	⊢ ( ( ( 𝐴 ↑ 2 ) − ( ( 𝑇 · ( 𝐴 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) )
149	136 137 59	addsubassi	⊢ ( ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) )
150	145 148 149	3eqtrri	⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) )
151	150	oveq2i	⊢ ( ( 1 − 𝑇 ) · ( ( ( 𝐴 ↑ 2 ) − ( 𝑇 · ( 𝐴 ↑ 2 ) ) ) + ( ( 𝑇 · ( 2 · ( 𝐴 · 𝐶 ) ) ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) = ( ( 1 − 𝑇 ) · ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) )
152	134 139 151	3eqtr2i	⊢ ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) = ( ( 1 − 𝑇 ) · ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) )
153	57 60	negsubdi2i	⊢ - ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) )
154	153	oveq2i	⊢ ( ( 1 − 𝑇 ) · - ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) = ( ( 1 − 𝑇 ) · ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) − ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) ) )
155	18 64	mulneg2i	⊢ ( ( 1 − 𝑇 ) · - ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) = - ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) )
156	152 154 155	3eqtr2i	⊢ ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) = - ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) )
157	103 156	oveq12i	⊢ ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) ) = ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) + - ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) )
158	71 81	negsubi	⊢ ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) + - ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) = ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) )
159	98 157 158	3eqtri	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) = ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) )
160	159	oveq2i	⊢ ( ( 𝐷 ↑ 2 ) + ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) ) = ( ( 𝐷 ↑ 2 ) + ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) )
161	25 26	addcli	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) ∈ ℂ
162	161 12	addcomi	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) + ( 𝐷 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) + ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) )
163	12 71 81	addsubassi	⊢ ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) = ( ( 𝐷 ↑ 2 ) + ( ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) )
164	160 162 163	3eqtr4i	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( 𝑇 · 𝐶 ) ↑ 2 ) ) + ( 𝐷 ↑ 2 ) ) = ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) )
165	97 164	eqtr3i	⊢ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) )
166	82 81	subcli	⊢ ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) ∈ ℂ
167	28 166	subeq0i	⊢ ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) ) = 0 ↔ ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) )
168	165 167	mpbir	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) − ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) ) ) = 0
169	96 168	eqtr3i	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) = 0
170	2 3 4	mulassi	⊢ ( ( 𝑇 · 𝐶 ) · 𝐷 ) = ( 𝑇 · ( 𝐶 · 𝐷 ) )
171	170	oveq2i	⊢ ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) = ( 2 · ( 𝑇 · ( 𝐶 · 𝐷 ) ) )
172	8 2 9	mul12i	⊢ ( 2 · ( 𝑇 · ( 𝐶 · 𝐷 ) ) ) = ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) )
173	171 172	eqtri	⊢ ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) = ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) )
174	173	oveq2i	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) )
175	2 10	mulcli	⊢ ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ∈ ℂ
176	31 32 175	addsubi	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
177	174 176	eqtri	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
178	169 177	oveq12i	⊢ ( ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) ↑ 2 ) + ( 2 · ( ( ( 1 − 𝑇 ) · 𝐴 ) · ( ( 𝑇 · 𝐶 ) − 𝐷 ) ) ) ) + ( ( ( 𝑇 · 𝐶 ) ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) + ( ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐶 ) ) ) ) − ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐷 ) ) ) ) ) − ( ( 𝐷 ↑ 2 ) + ( 𝑇 · ( 𝑇 · ( 𝐶 ↑ 2 ) ) ) ) ) ) + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) − ( 2 · ( ( 𝑇 · 𝐶 ) · 𝐷 ) ) ) ) = ( 0 + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) )
179	31 175	subcli	⊢ ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) ∈ ℂ
180	179 32	addcli	⊢ ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ∈ ℂ
181	180	addlidi	⊢ ( 0 + ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
182	94 178 181	3eqtri	⊢ ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( 𝑇 · ( 𝐶 ↑ 2 ) ) − ( 𝑇 · ( 2 · ( 𝐶 · 𝐷 ) ) ) ) + ( 𝑇 · ( 𝐷 ↑ 2 ) ) )
183	16 182	eqtr4i	⊢ ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) )