Step |
Hyp |
Ref |
Expression |
1 |
|
fzfid |
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( 1 ... N ) e. Fin ) |
2 |
|
simpl21 |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR ) |
4 |
2 3
|
sylancom |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( D e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR ) |
7 |
5 6
|
sylancom |
|- ( ( ( ( N e. NN /\ 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 ) |
8 |
4 7
|
resubcld |
|- ( ( ( ( N e. NN /\ 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 ) |
9 |
8
|
resqcld |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. RR ) |
10 |
1 9
|
fsumrecl |
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. RR ) |
11 |
10
|
recnd |
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. CC ) |
12 |
11
|
adantr |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( G e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( G ` j ) e. RR ) |
15 |
13 14
|
sylancom |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( ( ( N e. NN /\ 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 |
|- ( ( H e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( H ` j ) e. RR ) |
18 |
16 17
|
sylancom |
|- ( ( ( ( N e. NN /\ 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 ) |
19 |
15 18
|
resubcld |
|- ( ( ( ( N e. NN /\ 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 ) |
20 |
19
|
resqcld |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. RR ) |
21 |
1 20
|
fsumrecl |
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. RR ) |
22 |
21
|
recnd |
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. CC ) |
23 |
22
|
adantr |
|- ( ( ( ( N e. NN /\ 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 |
|
elicc01 |
|- ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) ) |
25 |
24
|
simp1bi |
|- ( t e. ( 0 [,] 1 ) -> t e. RR ) |
26 |
25
|
recnd |
|- ( t e. ( 0 [,] 1 ) -> t e. CC ) |
27 |
26
|
ad2antrr |
|- ( ( ( 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 ) |
28 |
27
|
3ad2ant1 |
|- ( ( ( ( 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 ) |
29 |
28
|
adantl |
|- ( ( ( ( N e. NN /\ 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 ) |
30 |
|
simpl11 |
|- ( ( ( ( N e. NN /\ 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 ) |
31 |
|
simp12 |
|- ( ( ( N e. NN /\ 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 ) ) |
32 |
|
simp13 |
|- ( ( ( N e. NN /\ 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 ) ) |
33 |
|
simp21 |
|- ( ( ( N e. NN /\ 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 ) ) |
34 |
31 32 33
|
3jca |
|- ( ( ( N e. NN /\ 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 ) ) ) |
35 |
34
|
adantr |
|- ( ( ( ( N e. NN /\ 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 ) ) ) |
36 |
|
simprrl |
|- ( ( ( 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 ) ) ) ) |
37 |
36
|
3ad2ant1 |
|- ( ( ( ( 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 ) ) ) ) |
38 |
37
|
adantl |
|- ( ( ( ( N e. NN /\ 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 ) ) ) ) |
39 |
|
simp1rl |
|- ( ( ( ( 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 ) |
40 |
39
|
adantl |
|- ( ( ( ( N e. NN /\ 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 ) |
41 |
|
ax5seglem4 |
|- ( ( ( 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 ) |
42 |
30 35 38 40 41
|
syl211anc |
|- ( ( ( ( N e. NN /\ 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 ) |
43 |
|
simpr3r |
|- ( ( ( ( N e. NN /\ 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 >. ) |
44 |
|
simpl13 |
|- ( ( ( ( N e. NN /\ 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 ) ) |
45 |
|
simpl22 |
|- ( ( ( ( N e. NN /\ 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 ) ) |
46 |
|
simpl31 |
|- ( ( ( ( N e. NN /\ 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 ) ) |
47 |
|
simpl33 |
|- ( ( ( ( N e. NN /\ 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 ) ) |
48 |
|
brcgr |
|- ( ( ( 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 ) ) ) |
49 |
44 45 46 47 48
|
syl22anc |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) |
50 |
43 49
|
mpbid |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) |
51 |
|
simp23 |
|- ( ( ( N e. NN /\ 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 ) ) |
52 |
|
simp31 |
|- ( ( ( N e. NN /\ 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 ) ) |
53 |
|
simp32 |
|- ( ( ( N e. NN /\ 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 ) ) |
54 |
51 52 53
|
3jca |
|- ( ( ( N e. NN /\ 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 ) ) ) |
55 |
34 54
|
jca |
|- ( ( ( N e. NN /\ 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 ) ) ) ) |
56 |
55
|
adantr |
|- ( ( ( ( N e. NN /\ 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 ) ) ) ) |
57 |
|
simpr1l |
|- ( ( ( ( N e. NN /\ 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 ) ) ) |
58 |
|
simprrr |
|- ( ( ( 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 ) ) ) ) |
59 |
58
|
3ad2ant1 |
|- ( ( ( ( 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 ) ) ) ) |
60 |
59
|
adantl |
|- ( ( ( ( N e. NN /\ 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 ) ) ) ) |
61 |
38 60
|
jca |
|- ( ( ( ( N e. NN /\ 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 ) ) ) ) ) |
62 |
|
simpr2l |
|- ( ( ( ( N e. NN /\ 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 >. ) |
63 |
|
simpr2r |
|- ( ( ( ( N e. NN /\ 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 >. ) |
64 |
|
ax5seglem6 |
|- ( ( ( 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 ) |
65 |
30 56 40 57 61 62 63 64
|
syl232anc |
|- ( ( ( ( N e. NN /\ 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 ) |
66 |
65
|
oveq2d |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) |
67 |
54
|
adantr |
|- ( ( ( ( N e. NN /\ 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 ) ) ) |
68 |
|
ax5seglem3 |
|- ( ( ( 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 ) ) |
69 |
30 35 67 57 61 62 63 68
|
syl322anc |
|- ( ( ( ( N e. NN /\ 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 ) ) |
70 |
65 69
|
oveq12d |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) |
71 |
|
simpr3l |
|- ( ( ( ( N e. NN /\ 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 >. ) |
72 |
|
simpl12 |
|- ( ( ( ( N e. NN /\ 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 ) ) |
73 |
|
simpl23 |
|- ( ( ( ( N e. NN /\ 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 ) ) |
74 |
|
brcgr |
|- ( ( ( 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 ) ) ) |
75 |
72 45 73 47 74
|
syl22anc |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) |
76 |
71 75
|
mpbid |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) |
77 |
70 76
|
oveq12d |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) |
78 |
66 77
|
oveq12d |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) ) |
79 |
50 78
|
oveq12d |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) ) ) |
80 |
31 32
|
jca |
|- ( ( ( N e. NN /\ 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 ) ) ) |
81 |
|
simp22 |
|- ( ( ( N e. NN /\ 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 ) ) |
82 |
80 33 81
|
jca32 |
|- ( ( ( N e. NN /\ 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 ) ) ) ) |
83 |
82
|
adantr |
|- ( ( ( ( N e. NN /\ 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 ) ) ) ) |
84 |
|
simp1ll |
|- ( ( ( ( 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 ) ) |
85 |
84
|
adantl |
|- ( ( ( ( N e. NN /\ 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 ) ) |
86 |
|
ax5seglem9 |
|- ( ( ( 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 ) ) ) ) ) |
87 |
30 83 85 38 86
|
syl22anc |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) ) ) |
88 |
|
3simpc |
|- ( ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) -> ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) |
89 |
88
|
3ad2ant3 |
|- ( ( ( N e. NN /\ 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 ) ) ) |
90 |
51 52 89
|
jca31 |
|- ( ( ( N e. NN /\ 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 ) ) ) ) |
91 |
90
|
adantr |
|- ( ( ( ( N e. NN /\ 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 ) ) ) ) |
92 |
|
simp1lr |
|- ( ( ( ( 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 ) ) |
93 |
92
|
adantl |
|- ( ( ( ( N e. NN /\ 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 ) ) |
94 |
|
ax5seglem9 |
|- ( ( ( 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 ) ) ) ) ) |
95 |
30 91 93 60 94
|
syl22anc |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) ) ) |
96 |
79 87 95
|
3eqtr4d |
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ 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 ) ) ) |
97 |
65
|
oveq1d |
|- ( ( ( ( N e. NN /\ 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 ) ) ) |
98 |
96 97
|
eqtr4d |
|- ( ( ( ( N e. NN /\ 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 ) ) ) |
99 |
12 23 29 42 98
|
mulcanad |
|- ( ( ( ( N e. NN /\ 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 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) |
100 |
99
|
3exp2 |
|- ( ( ( N e. NN /\ 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 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) ) ) ) |
101 |
100
|
expd |
|- ( ( ( N e. NN /\ 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 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) ) ) ) ) |
102 |
101
|
rexlimdvv |
|- ( ( ( N e. NN /\ 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. t e. ( 0 [,] 1 ) E. 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 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) ) ) ) |
103 |
102
|
3impd |
|- ( ( ( N e. NN /\ 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. t e. ( 0 [,] 1 ) E. 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 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) ) |
104 |
|
brbtwn |
|- ( ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B Btwn <. A , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) ) |
105 |
32 31 33 104
|
syl3anc |
|- ( ( ( N e. NN /\ 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 Btwn <. A , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) ) |
106 |
|
brbtwn |
|- ( ( F e. ( EE ` N ) /\ E e. ( EE ` N ) /\ G e. ( EE ` N ) ) -> ( F Btwn <. E , G >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) |
107 |
52 51 53 106
|
syl3anc |
|- ( ( ( N e. NN /\ 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 Btwn <. E , G >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) |
108 |
105 107
|
anbi12d |
|- ( ( ( N e. NN /\ 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 Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) |
109 |
|
reeanv |
|- ( E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) |
110 |
108 109
|
bitr4di |
|- ( ( ( N e. NN /\ 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 Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) ) ) |
111 |
110
|
anbi2d |
|- ( ( ( N e. NN /\ 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 /\ E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) ) ) ) |
112 |
|
3anass |
|- ( ( A =/= B /\ B Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> ( A =/= B /\ ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) ) ) |
113 |
|
r19.42v |
|- ( E. 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 /\ E. 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 ) ) ) ) ) ) |
114 |
113
|
rexbii |
|- ( E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) ) <-> E. t e. ( 0 [,] 1 ) ( A =/= B /\ E. 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 ) ) ) ) ) ) |
115 |
|
r19.42v |
|- ( E. t e. ( 0 [,] 1 ) ( A =/= B /\ E. 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 /\ E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) ) ) |
116 |
114 115
|
bitri |
|- ( E. t e. ( 0 [,] 1 ) E. 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 /\ E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) ) ) |
117 |
111 112 116
|
3bitr4g |
|- ( ( ( N e. NN /\ 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 >. ) <-> E. t e. ( 0 [,] 1 ) E. 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 ) ) ) ) ) ) ) |
118 |
117
|
3anbi1d |
|- ( ( ( N e. NN /\ 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 >. ) ) <-> ( E. t e. ( 0 [,] 1 ) E. 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 >. ) ) ) ) |
119 |
|
simp33 |
|- ( ( ( N e. NN /\ 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 ) ) ) -> H e. ( EE ` N ) ) |
120 |
|
brcgr |
|- ( ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. G , H >. <-> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) ) |
121 |
33 81 53 119 120
|
syl22anc |
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. G , H >. <-> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) ) |
122 |
103 118 121
|
3imtr4d |
|- ( ( ( N e. NN /\ 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 >. ) ) |