Metamath Proof Explorer

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