Metamath Proof Explorer

Theorem ax5seglem3

Description: Lemma for ax5seg . Combine congruences for points on a line. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem3 
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
3 2 simp1bi 
 |-  ( T e. ( 0 [,] 1 ) -> T e. RR )
4 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
5 1 3 4 sylancr 
 |-  ( T e. ( 0 [,] 1 ) -> ( 1 - T ) e. RR )
6 5 ad2antrr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> ( 1 - T ) e. RR )
7 6 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 - T ) e. RR )
8 fzfid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( 1 ... N ) e. Fin )
9 ax5seglem3a 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) e. RR /\ ( ( D ` j ) - ( F ` j ) ) e. RR ) )
10 9 simpld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. RR )
11 10 resqcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. RR )
12 8 11 fsumrecl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. RR )
13 10 sqge0d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> 0 <_ ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) )
14 8 11 13 fsumge0 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> 0 <_ sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) )
15 12 14 resqrtcld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) e. RR )
16 15 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) e. RR )
17 7 16 remulcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) e. RR )
18 elicc01 
 |-  ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
19 18 simp1bi 
 |-  ( S e. ( 0 [,] 1 ) -> S e. RR )
20 resubcl 
 |-  ( ( 1 e. RR /\ S e. RR ) -> ( 1 - S ) e. RR )
21 1 19 20 sylancr 
 |-  ( S e. ( 0 [,] 1 ) -> ( 1 - S ) e. RR )
22 21 ad2antlr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> ( 1 - S ) e. RR )
23 22 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 - S ) e. RR )
24 9 simprd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( D ` j ) - ( F ` j ) ) e. RR )
25 24 resqcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) e. RR )
26 8 25 fsumrecl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) e. RR )
27 24 sqge0d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> 0 <_ ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
28 8 25 27 fsumge0 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> 0 <_ sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
29 26 28 resqrtcld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) e. RR )
30 29 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) e. RR )
31 23 30 remulcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) e. RR )
32 2 simp3bi 
 |-  ( T e. ( 0 [,] 1 ) -> T <_ 1 )
33 subge0 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 0 <_ ( 1 - T ) <-> T <_ 1 ) )
34 1 3 33 sylancr 
 |-  ( T e. ( 0 [,] 1 ) -> ( 0 <_ ( 1 - T ) <-> T <_ 1 ) )
35 32 34 mpbird 
 |-  ( T e. ( 0 [,] 1 ) -> 0 <_ ( 1 - T ) )
36 35 ad2antrr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> 0 <_ ( 1 - T ) )
37 36 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( 1 - T ) )
38 12 14 sqrtge0d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> 0 <_ ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
39 38 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
40 7 16 37 39 mulge0d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) )
41 18 simp3bi 
 |-  ( S e. ( 0 [,] 1 ) -> S <_ 1 )
42 subge0 
 |-  ( ( 1 e. RR /\ S e. RR ) -> ( 0 <_ ( 1 - S ) <-> S <_ 1 ) )
43 1 19 42 sylancr 
 |-  ( S e. ( 0 [,] 1 ) -> ( 0 <_ ( 1 - S ) <-> S <_ 1 ) )
44 41 43 mpbird 
 |-  ( S e. ( 0 [,] 1 ) -> 0 <_ ( 1 - S ) )
45 44 ad2antlr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> 0 <_ ( 1 - S ) )
46 45 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( 1 - S ) )
47 26 28 sqrtge0d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> 0 <_ ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
48 47 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
49 23 30 46 48 mulge0d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
50 resqrtth 
 |-  ( ( sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. RR /\ 0 <_ sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) )
51 12 14 50 syl2anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) )
52 51 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) )
53 52 oveq2d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
54 ax-1cn 
 |-  1 e. CC
55 3 recnd 
 |-  ( T e. ( 0 [,] 1 ) -> T e. CC )
56 55 ad2antrr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> T e. CC )
57 56 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> T e. CC )
58 subcl 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
59 54 57 58 sylancr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 - T ) e. CC )
60 15 recnd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) e. CC )
61 60 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) e. CC )
62 59 61 sqmuld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) ) )
63 resqrtth 
 |-  ( ( sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) e. RR /\ 0 <_ sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
64 26 28 63 syl2anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
65 64 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
66 65 oveq2d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - S ) ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) ) = ( ( ( 1 - S ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
67 19 recnd 
 |-  ( S e. ( 0 [,] 1 ) -> S e. CC )
68 67 ad2antlr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> S e. CC )
69 68 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> S e. CC )
70 subcl 
 |-  ( ( 1 e. CC /\ S e. CC ) -> ( 1 - S ) e. CC )
71 54 69 70 sylancr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 - S ) e. CC )
72 29 recnd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) e. CC )
73 72 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) e. CC )
74 71 73 sqmuld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( ( 1 - S ) ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) ) )
75 simp3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. B , C >. Cgr <. E , F >. )
76 simp122 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> B e. ( EE ` N ) )
77 simp123 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> C e. ( EE ` N ) )
78 simp132 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> E e. ( EE ` N ) )
79 simp133 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> F e. ( EE ` N ) )
80 brcgr 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. E , F >. <-> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( F ` j ) ) ^ 2 ) ) )
81 76 77 78 79 80 syl22anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( <. B , C >. Cgr <. E , F >. <-> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( F ` j ) ) ^ 2 ) ) )
82 75 81 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( F ` j ) ) ^ 2 ) )
83 simp11 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> N e. NN )
84 simp121 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A e. ( EE ` N ) )
85 simp2ll 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> T e. ( 0 [,] 1 ) )
86 simp2rl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) )
87 ax5seglem2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
88 83 84 77 85 86 87 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
89 simp131 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> D e. ( EE ` N ) )
90 simp2lr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> S e. ( 0 [,] 1 ) )
91 simp2rr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) )
92 ax5seglem2 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( S e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( F ` j ) ) ^ 2 ) = ( ( ( 1 - S ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
93 83 89 79 90 91 92 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( F ` j ) ) ^ 2 ) = ( ( ( 1 - S ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
94 82 88 93 3eqtr3d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( ( ( 1 - S ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
95 66 74 94 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
96 53 62 95 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ^ 2 ) )
97 17 31 40 49 96 sq11d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
98 3 ad2antrr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> T e. RR )
99 98 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> T e. RR )
100 99 16 remulcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) e. RR )
101 19 ad2antlr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> S e. RR )
102 101 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> S e. RR )
103 102 30 remulcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) e. RR )
104 2 simp2bi 
 |-  ( T e. ( 0 [,] 1 ) -> 0 <_ T )
105 104 ad2antrr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> 0 <_ T )
106 105 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ T )
107 99 16 106 39 mulge0d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) )
108 18 simp2bi 
 |-  ( S e. ( 0 [,] 1 ) -> 0 <_ S )
109 108 ad2antlr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> 0 <_ S )
110 109 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ S )
111 102 30 110 48 mulge0d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> 0 <_ ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
112 51 oveq2d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( T ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
113 112 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
114 57 61 sqmuld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( T ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ^ 2 ) ) )
115 65 oveq2d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( S ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
116 69 73 sqmuld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( S ^ 2 ) x. ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ^ 2 ) ) )
117 simp3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , B >. Cgr <. D , E >. )
118 brcgr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) ) )
119 84 76 89 78 118 syl22anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( <. A , B >. Cgr <. D , E >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) ) )
120 117 119 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) )
121 ax5seglem1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
122 83 84 77 85 86 121 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
123 ax5seglem1 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( S e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
124 83 89 79 90 91 123 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
125 120 122 124 3eqtr3d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
126 115 116 125 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
127 113 114 126 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) ^ 2 ) = ( ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ^ 2 ) )
128 100 103 107 111 127 sq11d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
129 97 128 oveq12d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) + ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) ) = ( ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) + ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ) )
130 59 57 61 adddird 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) + T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( ( ( 1 - T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) + ( T x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) ) )
131 71 69 73 adddird 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - S ) + S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( ( ( 1 - S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) + ( S x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) ) )
132 129 130 131 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) + T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( ( ( 1 - S ) + S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
133 npcan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( ( 1 - T ) + T ) = 1 )
134 54 55 133 sylancr 
 |-  ( T e. ( 0 [,] 1 ) -> ( ( 1 - T ) + T ) = 1 )
135 134 adantr 
 |-  ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) -> ( ( 1 - T ) + T ) = 1 )
136 135 oveq1d 
 |-  ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) + T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) )
137 136 adantr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> ( ( ( 1 - T ) + T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) )
138 137 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) + T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) )
139 60 mullidd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
140 139 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
141 138 140 eqtrd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - T ) + T ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
142 npcan 
 |-  ( ( 1 e. CC /\ S e. CC ) -> ( ( 1 - S ) + S ) = 1 )
143 54 67 142 sylancr 
 |-  ( S e. ( 0 [,] 1 ) -> ( ( 1 - S ) + S ) = 1 )
144 143 oveq1d 
 |-  ( S e. ( 0 [,] 1 ) -> ( ( ( 1 - S ) + S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
145 144 ad2antlr 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> ( ( ( 1 - S ) + S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
146 145 3ad2ant2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - S ) + S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) )
147 72 mullidd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
148 147 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
149 146 148 eqtrd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( ( 1 - S ) + S ) x. ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
150 132 141 149 3eqtr3d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
151 sqrt11 
 |-  ( ( ( sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. RR /\ 0 <_ sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) /\ ( sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) e. RR /\ 0 <_ sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
152 12 14 26 28 151 syl22anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
153 152 3ad2ant1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( sqrt ` sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
154 150 153 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )