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 
|- A e. CC
ax5seglem7.2 
|- T e. CC
ax5seglem7.3 
|- C e. CC
ax5seglem7.4 
|- D e. CC
Assertion ax5seglem7 
|- ( T x. ( ( C - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - T ) x. A ) + ( T x. C ) ) - D ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( A - C ) ^ 2 ) ) - ( ( A - D ) ^ 2 ) ) ) )

Proof

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