MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax5seg Structured version   Unicode version

Theorem ax5seg 23007
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 11779 . . . . . . . . . 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 1059 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( C `  j )  e.  RR )
42, 3sylancom 660 . . . . . . . . . . . 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 1060 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( D `  j )  e.  RR )
75, 6sylancom 660 . . . . . . . . . . . 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 9764 . . . . . . . . . . 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 12018 . . . . . . . . . 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 13195 . . . . . . . . 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 9400 . . . . . . . 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 462 . . . . . . 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 1063 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13  |-  ( ( G  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( G `  j )  e.  RR )
1513, 14sylancom 660 . . . . . . . . . . . 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 1064 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13  |-  ( ( H  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( H `  j )  e.  RR )
1816, 17sylancom 660 . . . . . . . . . . . 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 9764 . . . . . . . . . . 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 12018 . . . . . . . . . 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 13195 . . . . . . . . 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 9400 . . . . . . . 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 462 . . . . . . 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 9374 . . . . . . . . . . . . 13  |-  0  e.  RR
25 1re 9373 . . . . . . . . . . . . 13  |-  1  e.  RR
2624, 25elicc2i 11349 . . . . . . . . . . . 12  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
2726simp1bi 996 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
2827recnd 9400 . . . . . . . . . 10  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  CC )
2928ad2antrr 718 . . . . . . . . 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 1002 . . . . . . . 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 463 . . . . . . 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 1056 . . . . . . . 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 1012 . . . . . . . . . 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 1013 . . . . . . . . . 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 1014 . . . . . . . . . 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 1161 . . . . . . . . 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 462 . . . . . . . 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 756 . . . . . . . . . 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 1002 . . . . . . . . 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 463 . . . . . . . 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 1046 . . . . . . . . 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 463 . . . . . . . 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 23001 . . . . . . . 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 1217 . . . . . . 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 1043 . . . . . . . . . . 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 1058 . . . . . . . . . . . 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 1060 . . . . . . . . . . . 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 1062 . . . . . . . . . . . 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 1064 . . . . . . . . . . . 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 22969 . . . . . . . . . . . 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 1212 . . . . . . . . . . 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 210 . . . . . . . . . 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 1016 . . . . . . . . . . . . . . . 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 1017 . . . . . . . . . . . . . . . 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 1018 . . . . . . . . . . . . . . . 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 1161 . . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 1038 . . . . . . . . . . . . 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 757 . . . . . . . . . . . . . . . 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 1002 . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . 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 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 ) ) )  /\  (
( ( 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 1041 . . . . . . . . . . . . 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 23003 . . . . . . . . . . . . 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 1238 . . . . . . . . . . . 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 6096 . . . . . . . . . . 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 462 . . . . . . . . . . . . . 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 23000 . . . . . . . . . . . . . 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 1239 . . . . . . . . . . . . 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 6098 . . . . . . . . . . . 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 1042 . . . . . . . . . . . . 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 1057 . . . . . . . . . . . . . 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 1061 . . . . . . . . . . . . . 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 22969 . . . . . . . . . . . . . 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 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 >. ) ) )  ->  ( <. 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 210 . . . . . . . . . . . 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 6098 . . . . . . . . . . 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 6098 . . . . . . . . . 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 6098 . . . . . . . . 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 529 . . . . . . . . . . . 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 1015 . . . . . . . . . . . 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 532 . . . . . . . . . . 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 462 . . . . . . . . . 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 1044 . . . . . . . . . . 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 463 . . . . . . . . . 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 23006 . . . . . . . . . 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 1212 . . . . . . . . 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 980 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( EE
`  N )  /\  G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) )  ->  ( G  e.  ( EE `  N )  /\  H  e.  ( EE `  N
) ) )
91903ad2ant3 1004 . . . . . . . . . . . 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 531 . . . . . . . . . . 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 462 . . . . . . . . . 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 1045 . . . . . . . . . . 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 463 . . . . . . . . . 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 23006 . . . . . . . . . 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 1212 . . . . . . . . 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 2475 . . . . . . . 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 ,