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

Theorem ax5seg 23906
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
StepHypRef Expression
1 simpr3r 1022 . . . . . . . . . . 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 >. )
2 simpl13 1037 . . . . . . . . . . . 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
) )
3 simpl22 1039 . . . . . . . . . . . 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
) )
4 simpl31 1041 . . . . . . . . . . . 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
) )
5 simpl33 1043 . . . . . . . . . . . 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
) )
6 brcgr 23868 . . . . . . . . . . . 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 ) ) )
72, 3, 4, 5, 6syl22anc 1188 . . . . . . . . . . 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 ) ) )
81, 7mpbid 203 . . . . . . . . . 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 ) )
9 simpl11 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 ) ) )  /\  (
( ( 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 )
10 simp12 991 . . . . . . . . . . . . . . . 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 ) ) )  ->  A  e.  ( EE `  N
) )
11 simp13 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 ) ) )  ->  B  e.  ( EE `  N
) )
12 simp21 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 ) ) )  ->  C  e.  ( EE `  N
) )
1310, 11, 123jca 1137 . . . . . . . . . . . . . . 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 ) ) )  ->  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
)  /\  C  e.  ( EE `  N ) ) )
14 simp23 995 . . . . . . . . . . . . . . . 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
) )
15 simp31 996 . . . . . . . . . . . . . . . 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
) )
16 simp32 997 . . . . . . . . . . . . . . . 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
) )
1714, 15, 163jca 1137 . . . . . . . . . . . . . . 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 ) ) )
1813, 17jca 520 . . . . . . . . . . . . . 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 ) ) ) )
1918adantr 453 . . . . . . . . . . . . 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 ) ) ) )
20 simp1rl 1025 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
2120adantl 454 . . . . . . . . . . . . 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 )
22 simpr1l 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 >. ) ) )  ->  (
t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )
23 simprrl 743 . . . . . . . . . . . . . . . 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
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) )
24233ad2ant1 981 . . . . . . . . . . . . . . 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
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) )
2524adantl 454 . . . . . . . . . . . . . 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
) ( B `  i )  =  ( ( ( 1  -  t )  x.  ( A `  i )
)  +  ( t  x.  ( C `  i ) ) ) )
26 simprrr 744 . . . . . . . . . . . . . . . 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 ) ) ) )
27263ad2ant1 981 . . . . . . . . . . . . . . 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 ) ) ) )
2827adantl 454 . . . . . . . . . . . . . 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 ) ) ) )
2925, 28jca 520 . . . . . . . . . . . . 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 )
) ) ) )
30 simpr2l 1019 . . . . . . . . . . . . 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 >. )
31 simpr2r 1020 . . . . . . . . . . . . 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 >. )
32 ax5seglem6 23902 . . . . . . . . . . . . 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 )
339, 19, 21, 22, 29, 30, 31, 32syl232anc 1214 . . . . . . . . . . . 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 )
3433oveq2d 5773 . . . . . . . . . . 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 ) )
3513adantr 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  e.  ( EE `  N )  /\  B  e.  ( EE `  N
)  /\  C  e.  ( EE `  N ) ) )
3617adantr 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 >. ) ) )  ->  ( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N
)  /\  G  e.  ( EE `  N ) ) )
37 ax5seglem3 23899 . . . . . . . . . . . . . 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 ) )
389, 35, 36, 22, 29, 30, 31, 37syl322anc 1215 . . . . . . . . . . . . 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 ) )
3933, 38oveq12d 5775 . . . . . . . . . . . 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 ) ) )
40 simpr3l 1021 . . . . . . . . . . . . 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 >. )
41 simpl12 1036 . . . . . . . . . . . . . 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
) )
42 simpl23 1040 . . . . . . . . . . . . . 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
) )
43 brcgr 23868 . . . . . . . . . . . . . 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 ) ) )
4441, 3, 42, 5, 43syl22anc 1188 . . . . . . . . . . . . 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 ) ) )
4540, 44mpbid 203 . . . . . . . . . . . 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 ) )
4639, 45oveq12d 5775 . . . . . . . . . . 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 ) ) )
4734, 46oveq12d 5775 . . . . . . . . . 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 ) ) ) )
488, 47oveq12d 5775 . . . . . . . . 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 ) ) ) ) )
4910, 11jca 520 . . . . . . . . . . . 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
) ) )
50 simp22 994 . . . . . . . . . . . 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
) )
5149, 12, 50jca32 523 . . . . . . . . . . 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
) ) ) )
5251adantr 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 >. ) ) )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  D  e.  ( EE `  N
) ) ) )
53 simp1ll 1023 . . . . . . . . . . 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
) )
5453adantl 454 . . . . . . . . . 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
) )
55 ax5seglem9 23905 . . . . . . . . . 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 ) ) ) ) )
569, 52, 54, 25, 55syl22anc 1188 . . . . . . . . 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 ) ) ) ) )
57 3simpc 959 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( EE
`  N )  /\  G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) )  ->  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) )
58573ad2ant3 983 . . . . . . . . . . . 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
) ) )
5914, 15, 58jca31 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 ) ) )  ->  (
( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N ) )  /\  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) ) )
6059adantr 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 >. ) ) )  ->  (
( E  e.  ( EE `  N )  /\  F  e.  ( EE `  N ) )  /\  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) ) )
61 simp1lr 1024 . . . . . . . . . . 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
) )
6261adantl 454 . . . . . . . . . 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
) )
63 ax5seglem9 23905 . . . . . . . . . 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 ) ) ) ) )
649, 60, 62, 28, 63syl22anc 1188 . . . . . . . . 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 ) ) ) ) )
6548, 56, 643eqtr4d 2298 . . . . . . . 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 >. ) ) )  ->  (
t  x.  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 ) )  =  ( s  x.  sum_ j  e.  ( 1 ... N ) ( ( ( G `  j )  -  ( H `  j )
) ^ 2 ) ) )
6633oveq1d 5772 . . . . . . . 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 >. ) ) )  ->  (
t  x.  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 ) )  =  ( s  x.  sum_ j  e.  ( 1 ... N ) ( ( ( G `  j )  -  ( H `  j )
) ^ 2 ) ) )
6765, 66eqtr4d 2291 . . . . . . 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  x.  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 ) )  =  ( t  x.  sum_ j  e.  ( 1 ... N ) ( ( ( G `  j )  -  ( H `  j )
) ^ 2 ) ) )
68 fzfid 10966 . . . . . . . . . . 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 ) ) )  ->  (
1 ... N )  e. 
Fin )
69 simpl21 1038 . . . . . . . . . . . . . 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 ) ) )  /\  j  e.  ( 1 ... N
) )  ->  C  e.  ( EE `  N
) )
70 fveere 23869 . . . . . . . . . . . . . 14  |-  ( ( C  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( C `  j )  e.  RR )
7169, 70sylancom 651 . . . . . . . . . . . . 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 `  j )  e.  RR )
72 simpl22 1039 . . . . . . . . . . . . . 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 ) ) )  /\  j  e.  ( 1 ... N
) )  ->  D  e.  ( EE `  N
) )
73 fveere 23869 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( D `  j )  e.  RR )
7472, 73sylancom 651 . . . . . . . . . . . . 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 `  j )  e.  RR )
7571, 74resubcld 9144 . . . . . . . . . . . 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
)  -  ( D `
 j ) )  e.  RR )
7675resqcld 11202 . . . . . . . . . . 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 )
) ^ 2 )  e.  RR )
7768, 76fsumrecl 12137 . . . . . . . . . 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 ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 )  e.  RR )
7877recnd 8794 . . . . . . . . 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.  CC )
7978adantr 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 >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( C `  j )  -  ( D `  j ) ) ^
2 )  e.  CC )
80 simpl32 1042 . . . . . . . . . . . . . 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 ) ) )  /\  j  e.  ( 1 ... N
) )  ->  G  e.  ( EE `  N
) )
81 fveere 23869 . . . . . . . . . . . . . 14  |-  ( ( G  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( G `  j )  e.  RR )
8280, 81sylancom 651 . . . . . . . . . . . . 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 `  j )  e.  RR )
83 simpl33 1043 . . . . . . . . . . . . . 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 ) ) )  /\  j  e.  ( 1 ... N
) )  ->  H  e.  ( EE `  N
) )
84 fveere 23869 . . . . . . . . . . . . . 14  |-  ( ( H  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( H `  j )  e.  RR )
8583, 84sylancom 651 . . . . . . . . . . . . 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 `  j )  e.  RR )
8682, 85resubcld 9144 . . . . . . . . . . . 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
)  -  ( H `
 j ) )  e.  RR )
8786resqcld 11202 . . . . . . . . . . 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 )
) ^ 2 )  e.  RR )
8868, 87fsumrecl 12137 . . . . . . . . . 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 ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 )  e.  RR )
8988recnd 8794 . . . . . . . . 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.  CC )
9089adantr 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 >. ) ) )  ->  sum_ j  e.  ( 1 ... N
) ( ( ( G `  j )  -  ( H `  j ) ) ^
2 )  e.  CC )
91 0re 8771 . . . . . . . . . . . . . 14  |-  0  e.  RR
92 1re 8770 . . . . . . . . . . . . . 14  |-  1  e.  RR
9391, 92elicc2i 10647 . . . . . . . . . . . . 13  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
9493simp1bi 975 . . . . . . . . . . . 12  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
9594recnd 8794 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  CC )
9695ad2antrr 709 . . . . . . . . . 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