Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax5seg Unicode version

Theorem ax5seg 25781
Description: The five segment axiom. Take two triangles  A D C and  E H G, a point  B on  A C, and a point  F on  E G. If all corresponding line segments except for  C D and  G H are congruent, then so are  C D and  G H. Axiom A5 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 12-Jun-2013.)
Assertion
Ref Expression
ax5seg  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  (
( ( A  =/= 
B  /\  B  Btwn  <. A ,  C >.  /\  F  Btwn  <. E ,  G >. )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  <. C ,  D >.Cgr <. G ,  H >. ) )

Proof of Theorem ax5seg
Dummy variables  i 
j  t  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 11267 . . . . . . . . . 10  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  (
1 ... N )  e. 
Fin )
2 simpl21 1035 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  C  e.  ( EE `  N
) )
3 fveere 25744 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( C `  j )  e.  RR )
42, 3sylancom 649 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  ( C `  j )  e.  RR )
5 simpl22 1036 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  D  e.  ( EE `  N
) )
6 fveere 25744 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( D `  j )  e.  RR )
75, 6sylancom 649 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  ( D `  j )  e.  RR )
84, 7resubcld 9421 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  (
( C `  j
)  -  ( D `
 j ) )  e.  RR )
98resqcld 11504 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  (
( ( C `  j )  -  ( D `  j )
) ^ 2 )  e.  RR )
101, 9fsumrecl 12483 . . . . . . . . 9  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 )  e.  RR )
1110recnd 9070 . . . . . . . 8  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 )  e.  CC )
1211adantr 452 . . . . . . 7  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 )  e.  CC )
13 simpl32 1039 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  G  e.  ( EE `  N
) )
14 fveere 25744 . . . . . . . . . . . . 13  |-  ( ( G  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( G `  j )  e.  RR )
1513, 14sylancom 649 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  ( G `  j )  e.  RR )
16 simpl33 1040 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  H  e.  ( EE `  N
) )
17 fveere 25744 . . . . . . . . . . . . 13  |-  ( ( H  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( H `  j )  e.  RR )
1816, 17sylancom 649 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  ( H `  j )  e.  RR )
1915, 18resubcld 9421 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  (
( G `  j
)  -  ( H `
 j ) )  e.  RR )
2019resqcld 11504 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  j  e.  ( 1 ... N
) )  ->  (
( ( G `  j )  -  ( H `  j )
) ^ 2 )  e.  RR )
211, 20fsumrecl 12483 . . . . . . . . 9  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 )  e.  RR )
2221recnd 9070 . . . . . . . 8  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 )  e.  CC )
2322adantr 452 . . . . . . 7  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 )  e.  CC )
24 0re 9047 . . . . . . . . . . . . 13  |-  0  e.  RR
25 1re 9046 . . . . . . . . . . . . 13  |-  1  e.  RR
2624, 25elicc2i 10932 . . . . . . . . . . . 12  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
2726simp1bi 972 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
2827recnd 9070 . . . . . . . . . 10  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  CC )
2928ad2antrr 707 . . . . . . . . 9  |-  ( ( ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  ->  t  e.  CC )
30293ad2ant1 978 . . . . . . . 8  |-  ( ( ( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  t  e.  CC )
3130adantl 453 . . . . . . 7  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  t  e.  CC )
32 simpl11 1032 . . . . . . . 8  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  N  e.  NN )
33 simp12 988 . . . . . . . . . 10  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  A  e.  ( EE `  N
) )
34 simp13 989 . . . . . . . . . 10  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  B  e.  ( EE `  N
) )
35 simp21 990 . . . . . . . . . 10  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  C  e.  ( EE `  N
) )
3633, 34, 353jca 1134 . . . . . . . . 9  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
)  /\  C  e.  ( EE `  N ) ) )
3736adantr 452 . . . . . . . 8  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
)  /\  C  e.  ( EE `  N ) ) )
38 simprrl 741 . . . . . . . . . 10  |-  ( ( ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  ->  A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) )
39383ad2ant1 978 . . . . . . . . 9  |-  ( ( ( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) )
4039adantl 453 . . . . . . . 8  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) )
41 simp1rl 1022 . . . . . . . . 9  |-  ( ( ( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  A  =/=  B )
4241adantl 453 . . . . . . . 8  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  A  =/=  B )
43 ax5seglem4 25775 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) ) )  /\  A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A  =/=  B )  ->  t  =/=  0 )
4432, 37, 40, 42, 43syl211anc 1190 . . . . . . 7  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  t  =/=  0 )
45 simpr3r 1019 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  <. B ,  D >.Cgr <. F ,  H >. )
46 simpl13 1034 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  B  e.  ( EE `  N
) )
47 simpl22 1036 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  D  e.  ( EE `  N
) )
48 simpl31 1038 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  F  e.  ( EE `  N
) )
49 simpl33 1040 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  H  e.  ( EE `  N
) )
50 brcgr 25743 . . . . . . . . . . . 12  |-  ( ( ( B  e.  ( EE `  N )  /\  D  e.  ( EE `  N ) )  /\  ( F  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) )  -> 
( <. B ,  D >.Cgr
<. F ,  H >.  <->  sum_ j  e.  ( 1 ... N ) ( ( ( B `  j )  -  ( D `  j )
) ^ 2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( F `
 j )  -  ( H `  j ) ) ^ 2 ) ) )
5146, 47, 48, 49, 50syl22anc 1185 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  ( <. B ,  D >.Cgr <. F ,  H >.  <->  sum_ j  e.  ( 1 ... N ) ( ( ( B `  j )  -  ( D `  j )
) ^ 2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( F `
 j )  -  ( H `  j ) ) ^ 2 ) ) )
5245, 51mpbid 202 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( B `  j )  -  ( D `  j ) ) ^
2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( F `  j )  -  ( H `  j )
) ^ 2 ) )
53 simp23 992 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  E  e.  ( EE `  N
) )
54 simp31 993 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  F  e.  ( EE `  N
) )
55 simp32 994 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  G  e.  ( EE `  N
) )
5653, 54, 553jca 1134 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  e.  ( EE `  N ) ) )
5736, 56jca 519 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  e.  ( EE `  N ) ) ) )
5857adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  e.  ( EE `  N ) ) ) )
59 simpr1l 1014 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )
60 simprrr 742 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  ->  A. i  e.  ( 1 ... N
) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i )
)  +  ( s  x.  ( G `  i ) ) ) )
61603ad2ant1 978 . . . . . . . . . . . . . . 15  |-  ( ( ( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  A. i  e.  ( 1 ... N
) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i )
)  +  ( s  x.  ( G `  i ) ) ) )
6261adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  A. i  e.  ( 1 ... N
) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i )
)  +  ( s  x.  ( G `  i ) ) ) )
6340, 62jca 519 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) )
64 simpr2l 1016 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  <. A ,  B >.Cgr <. E ,  F >. )
65 simpr2r 1017 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  <. B ,  C >.Cgr <. F ,  G >. )
66 ax5seglem6 25777 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN  /\  ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  e.  ( EE `  N ) ) ) )  /\  ( A  =/=  B  /\  ( 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 ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\  <. B ,  C >.Cgr
<. F ,  G >. ) )  ->  t  =  s )
6732, 58, 42, 59, 63, 64, 65, 66syl232anc 1211 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  t  =  s )
6867oveq2d 6056 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
1  -  t )  =  ( 1  -  s ) )
6956adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  e.  ( EE `  N ) ) )
70 ax5seglem3 25774 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  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 ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\  <. B ,  C >.Cgr
<. F ,  G >. ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( C `  j ) ) ^
2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( E `  j )  -  ( G `  j )
) ^ 2 ) )
7132, 37, 69, 59, 63, 64, 65, 70syl322anc 1212 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( C `  j ) ) ^
2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( E `  j )  -  ( G `  j )
) ^ 2 ) )
7267, 71oveq12d 6058 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
t  x.  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( C `  j ) ) ^
2 ) )  =  ( s  x.  sum_ j  e.  ( 1 ... N ) ( ( ( E `  j )  -  ( G `  j )
) ^ 2 ) ) )
73 simpr3l 1018 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  <. A ,  D >.Cgr <. E ,  H >. )
74 simpl12 1033 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  A  e.  ( EE `  N
) )
75 simpl23 1037 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  E  e.  ( EE `  N
) )
76 brcgr 25743 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ( EE `  N )  /\  D  e.  ( EE `  N ) )  /\  ( E  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) )  -> 
( <. A ,  D >.Cgr
<. E ,  H >.  <->  sum_ j  e.  ( 1 ... N ) ( ( ( A `  j )  -  ( D `  j )
) ^ 2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( E `
 j )  -  ( H `  j ) ) ^ 2 ) ) )
7774, 47, 75, 49, 76syl22anc 1185 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  ( <. A ,  D >.Cgr <. E ,  H >.  <->  sum_ j  e.  ( 1 ... N ) ( ( ( A `  j )  -  ( D `  j )
) ^ 2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( E `
 j )  -  ( H `  j ) ) ^ 2 ) ) )
7873, 77mpbid 202 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( D `  j ) ) ^
2 )  =  sum_ j  e.  ( 1 ... N ) ( ( ( E `  j )  -  ( H `  j )
) ^ 2 ) )
7972, 78oveq12d 6058 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
( t  x.  sum_ j  e.  ( 1 ... N ) ( ( ( A `  j )  -  ( C `  j )
) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( D `  j ) ) ^
2 ) )  =  ( ( s  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( E `
 j )  -  ( G `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( E `  j )  -  ( H `  j ) ) ^
2 ) ) )
8068, 79oveq12d 6058 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
( 1  -  t
)  x.  ( ( t  x.  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( C `  j ) ) ^
2 ) )  -  sum_ j  e.  ( 1 ... N ) ( ( ( A `  j )  -  ( D `  j )
) ^ 2 ) ) )  =  ( ( 1  -  s
)  x.  ( ( s  x.  sum_ j  e.  ( 1 ... N
) ( ( ( E `  j )  -  ( G `  j ) ) ^
2 ) )  -  sum_ j  e.  ( 1 ... N ) ( ( ( E `  j )  -  ( H `  j )
) ^ 2 ) ) ) )
8152, 80oveq12d 6058 . . . . . . . . 9  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  ( sum_ j  e.  ( 1 ... N ) ( ( ( B `  j )  -  ( D `  j )
) ^ 2 )  +  ( ( 1  -  t )  x.  ( ( t  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( A `
 j )  -  ( C `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( D `  j ) ) ^
2 ) ) ) )  =  ( sum_ j  e.  ( 1 ... N ) ( ( ( F `  j )  -  ( H `  j )
) ^ 2 )  +  ( ( 1  -  s )  x.  ( ( s  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( E `
 j )  -  ( G `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( E `  j )  -  ( H `  j ) ) ^
2 ) ) ) ) )
8233, 34jca 519 . . . . . . . . . . . 12  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) ) )
83 simp22 991 . . . . . . . . . . . 12  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  D  e.  ( EE `  N
) )
8482, 35, 83jca32 522 . . . . . . . . . . 11  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  D  e.  ( EE `  N
) ) ) )
8584adantr 452 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  D  e.  ( EE `  N
) ) ) )
86 simp1ll 1020 . . . . . . . . . . 11  |-  ( ( ( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  t  e.  ( 0 [,] 1
) )
8786adantl 453 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  t  e.  ( 0 [,] 1
) )
88 ax5seglem9 25780 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  D  e.  ( EE `  N
) ) ) )  /\  ( t  e.  ( 0 [,] 1
)  /\  A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) ) )  ->  (
t  x.  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 ) )  =  ( sum_ j  e.  ( 1 ... N ) ( ( ( B `
 j )  -  ( D `  j ) ) ^ 2 )  +  ( ( 1  -  t )  x.  ( ( t  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( A `
 j )  -  ( C `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( D `  j ) ) ^
2 ) ) ) ) )
8932, 85, 87, 40, 88syl22anc 1185 . . . . . . . . 9  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
t  x.  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 ) )  =  ( sum_ j  e.  ( 1 ... N ) ( ( ( B `
 j )  -  ( D `  j ) ) ^ 2 )  +  ( ( 1  -  t )  x.  ( ( t  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( A `
 j )  -  ( C `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( A `  j )  -  ( D `  j ) ) ^
2 ) ) ) ) )
90 3simpc 956 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( EE
`  N )  /\  G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) )  ->  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) )
91903ad2ant3 980 . . . . . . . . . . . 12  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) )
9253, 54, 91jca31 521 . . . . . . . . . . 11  |-  ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  ->  (
( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N ) )  /\  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) ) )
9392adantr 452 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N ) )  /\  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) ) )
94 simp1lr 1021 . . . . . . . . . . 11  |-  ( ( ( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) )  ->  s  e.  ( 0 [,] 1
) )
9594adantl 453 . . . . . . . . . 10  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  s  e.  ( 0 [,] 1
) )
96 ax5seglem9 25780 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( ( E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) )  /\  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) ) )  /\  ( s  e.  ( 0 [,] 1
)  /\  A. i  e.  ( 1 ... N
) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i )
)  +  ( s  x.  ( G `  i ) ) ) ) )  ->  (
s  x.  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 ) )  =  ( sum_ j  e.  ( 1 ... N ) ( ( ( F `
 j )  -  ( H `  j ) ) ^ 2 )  +  ( ( 1  -  s )  x.  ( ( s  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( E `
 j )  -  ( G `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( E `  j )  -  ( H `  j ) ) ^
2 ) ) ) ) )
9732, 93, 95, 62, 96syl22anc 1185 . . . . . . . . 9  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  /\  ( <. A ,  D >.Cgr <. E ,  H >.  /\  <. B ,  D >.Cgr
<. F ,  H >. ) ) )  ->  (
s  x.  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 ) )  =  ( sum_ j  e.  ( 1 ... N ) ( ( ( F `
 j )  -  ( H `  j ) ) ^ 2 )  +  ( ( 1  -  s )  x.  ( ( s  x. 
sum_ j  e.  ( 1 ... N ) ( ( ( E `
 j )  -  ( G `  j ) ) ^ 2 ) )  -  sum_ j  e.  ( 1 ... N
) ( ( ( E `  j )  -  ( H `  j ) ) ^
2 ) ) ) ) )
9881, 89, 973eqtr4d 2446 . . . . . . . 8  |-  ( ( ( ( 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 )  /\  G  e.  ( EE `  N
)  /\  H  e.  ( EE `  N ) ) )  /\  (
( ( t  e.  ( 0 [,] 1
)  /\  s  e.  ( 0 [,] 1
) )  /\  ( A  =/=  B  /\  ( A. i  e.  (
1 ... N ) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i ) )  +  ( t  x.  ( C `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( F `  i )  =  ( ( ( 1  -  s )  x.  ( E `  i ) )  +  ( s  x.  ( G `  i )
) ) ) ) )  /\  ( <. A ,  B >.Cgr <. E ,  F >.  /\ 
<. B