Metamath Proof Explorer

Theorem ax5seglem8

Description: Lemma for ax5seg . Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 . (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem8 
|- ( ( ( A e. CC /\ T e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( 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 oveq2 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( 1 - T ) x. A ) = ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) )
2 1 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( 1 - T ) x. A ) + ( T x. C ) ) = ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) )
3 2 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( ( 1 - T ) x. A ) + ( T x. C ) ) - D ) = ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) )
4 3 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( ( ( 1 - T ) x. A ) + ( T x. C ) ) - D ) ^ 2 ) = ( ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) ^ 2 ) )
5 oveq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A - C ) = ( if ( A e. CC , A , 0 ) - C ) )
6 5 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( A - C ) ^ 2 ) = ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) )
7 6 oveq2d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( T x. ( ( A - C ) ^ 2 ) ) = ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) )
8 oveq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A - D ) = ( if ( A e. CC , A , 0 ) - D ) )
9 8 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( A - D ) ^ 2 ) = ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) )
10 7 9 oveq12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( T x. ( ( A - C ) ^ 2 ) ) - ( ( A - D ) ^ 2 ) ) = ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) )
11 10 oveq2d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( 1 - T ) x. ( ( T x. ( ( A - C ) ^ 2 ) ) - ( ( A - D ) ^ 2 ) ) ) = ( ( 1 - T ) x. ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) )
12 4 11 oveq12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( ( ( ( 1 - T ) x. A ) + ( T x. C ) ) - D ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( A - C ) ^ 2 ) ) - ( ( A - D ) ^ 2 ) ) ) ) = ( ( ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) )
13 12 eqeq2d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( 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 ) ) ) ) <-> ( T x. ( ( C - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) ) )
14 oveq1 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( T x. ( ( C - D ) ^ 2 ) ) = ( if ( T e. CC , T , 0 ) x. ( ( C - D ) ^ 2 ) ) )
15 oveq2 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( 1 - T ) = ( 1 - if ( T e. CC , T , 0 ) ) )
16 15 oveq1d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) = ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) )
17 oveq1 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( T x. C ) = ( if ( T e. CC , T , 0 ) x. C ) )
18 16 17 oveq12d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) = ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) )
19 18 oveq1d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) = ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) )
20 19 oveq1d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) ^ 2 ) = ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) ^ 2 ) )
21 oveq1 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) = ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) )
22 21 oveq1d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) = ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) )
23 15 22 oveq12d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( 1 - T ) x. ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) = ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) )
24 20 23 oveq12d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) )
25 14 24 eqeq12d 
 |-  ( T = if ( T e. CC , T , 0 ) -> ( ( T x. ( ( C - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - T ) x. if ( A e. CC , A , 0 ) ) + ( T x. C ) ) - D ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) <-> ( if ( T e. CC , T , 0 ) x. ( ( C - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) ) )
26 oveq1 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( C - D ) = ( if ( C e. CC , C , 0 ) - D ) )
27 26 oveq1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( C - D ) ^ 2 ) = ( ( if ( C e. CC , C , 0 ) - D ) ^ 2 ) )
28 27 oveq2d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( if ( T e. CC , T , 0 ) x. ( ( C - D ) ^ 2 ) ) = ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - D ) ^ 2 ) ) )
29 oveq2 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( if ( T e. CC , T , 0 ) x. C ) = ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) )
30 29 oveq2d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) = ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) )
31 30 oveq1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) = ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) )
32 31 oveq1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) ^ 2 ) = ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) ^ 2 ) )
33 oveq2 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( if ( A e. CC , A , 0 ) - C ) = ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) )
34 33 oveq1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) = ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) )
35 34 oveq2d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) = ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) )
36 35 oveq1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) = ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) )
37 36 oveq2d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) = ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) )
38 32 37 oveq12d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) )
39 28 38 eqeq12d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( if ( T e. CC , T , 0 ) x. ( ( C - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. C ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - C ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) <-> ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) ) )
40 oveq2 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( if ( C e. CC , C , 0 ) - D ) = ( if ( C e. CC , C , 0 ) - if ( D e. CC , D , 0 ) ) )
41 40 oveq1d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( if ( C e. CC , C , 0 ) - D ) ^ 2 ) = ( ( if ( C e. CC , C , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) )
42 41 oveq2d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - D ) ^ 2 ) ) = ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) )
43 oveq2 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) = ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - if ( D e. CC , D , 0 ) ) )
44 43 oveq1d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) ^ 2 ) = ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - if ( D e. CC , D , 0 ) ) ^ 2 ) )
45 oveq2 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( if ( A e. CC , A , 0 ) - D ) = ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) )
46 45 oveq1d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) = ( ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) )
47 46 oveq2d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) = ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) )
48 47 oveq2d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) = ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) ) )
49 44 48 oveq12d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - if ( D e. CC , D , 0 ) ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) ) ) )
50 42 49 eqeq12d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - D ) ^ 2 ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - D ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - D ) ^ 2 ) ) ) ) <-> ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - if ( D e. CC , D , 0 ) ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) ) ) ) )
51 0cn 
 |-  0 e. CC
52 51 elimel 
 |-  if ( A e. CC , A , 0 ) e. CC
53 51 elimel 
 |-  if ( T e. CC , T , 0 ) e. CC
54 51 elimel 
 |-  if ( C e. CC , C , 0 ) e. CC
55 51 elimel 
 |-  if ( D e. CC , D , 0 ) e. CC
56 52 53 54 55 ax5seglem7 
 |-  ( if ( T e. CC , T , 0 ) x. ( ( if ( C e. CC , C , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) = ( ( ( ( ( ( 1 - if ( T e. CC , T , 0 ) ) x. if ( A e. CC , A , 0 ) ) + ( if ( T e. CC , T , 0 ) x. if ( C e. CC , C , 0 ) ) ) - if ( D e. CC , D , 0 ) ) ^ 2 ) + ( ( 1 - if ( T e. CC , T , 0 ) ) x. ( ( if ( T e. CC , T , 0 ) x. ( ( if ( A e. CC , A , 0 ) - if ( C e. CC , C , 0 ) ) ^ 2 ) ) - ( ( if ( A e. CC , A , 0 ) - if ( D e. CC , D , 0 ) ) ^ 2 ) ) ) )
57 13 25 39 50 56 dedth4h 
 |-  ( ( ( A e. CC /\ T e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( 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 ) ) ) ) )