Metamath Proof Explorer

Theorem axsegconlem10

Description: Lemma for axsegcon . Show that the scaling constant from axsegconlem7 produces the betweenness condition for A , B and F . (Contributed by Scott Fenton, 21-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
axsegconlem7.2 
|- T = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
axsegconlem8.3 
|- F = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) )
Assertion axsegconlem10 
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( F ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 
 |-  S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
2 axsegconlem7.2 
 |-  T = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
3 axsegconlem8.3 
 |-  F = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) )
4 2 axsegconlem4 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( sqrt ` T ) e. RR )
5 4 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` T ) e. RR )
6 simpl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
7 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
8 6 7 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
9 5 8 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( A ` i ) ) e. RR )
10 9 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( A ` i ) ) e. CC )
11 1 axsegconlem4 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR )
12 11 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. RR )
13 12 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` S ) e. RR )
14 1 2 3 axsegconlem8 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
15 fveere 
 |-  ( ( F e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. RR )
16 14 15 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. RR )
17 13 16 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( F ` i ) ) e. RR )
18 17 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( F ` i ) ) e. CC )
19 readdcl 
 |-  ( ( ( sqrt ` S ) e. RR /\ ( sqrt ` T ) e. RR ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
20 12 4 19 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
21 20 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
22 21 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. CC )
23 0red 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 e. RR )
24 12 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sqrt ` S ) e. RR )
25 1 axsegconlem6 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) )
26 25 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 < ( sqrt ` S ) )
27 2 axsegconlem5 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> 0 <_ ( sqrt ` T ) )
28 27 adantl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 <_ ( sqrt ` T ) )
29 addge01 
 |-  ( ( ( sqrt ` S ) e. RR /\ ( sqrt ` T ) e. RR ) -> ( 0 <_ ( sqrt ` T ) <-> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
30 12 4 29 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( 0 <_ ( sqrt ` T ) <-> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
31 28 30 mpbid 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) )
32 23 24 20 26 31 ltletrd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 < ( ( sqrt ` S ) + ( sqrt ` T ) ) )
33 32 gt0ne0d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) =/= 0 )
34 33 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) =/= 0 )
35 10 18 22 34 divdird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( ( ( ( sqrt ` T ) x. ( A ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) + ( ( ( sqrt ` S ) x. ( F ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) )
36 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
37 36 oveq2d 
 |-  ( k = i -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) = ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) )
38 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
39 38 oveq2d 
 |-  ( k = i -> ( ( sqrt ` T ) x. ( A ` k ) ) = ( ( sqrt ` T ) x. ( A ` i ) ) )
40 37 39 oveq12d 
 |-  ( k = i -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) = ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) )
41 40 oveq1d 
 |-  ( k = i -> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) = ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) )
42 ovex 
 |-  ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) e. _V
43 41 3 42 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( F ` i ) = ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) )
44 43 adantl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) = ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) )
45 44 oveq2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( F ` i ) ) = ( ( sqrt ` S ) x. ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) )
46 simpl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
47 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
48 46 47 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
49 21 48 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) e. RR )
50 49 9 resubcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) e. RR )
51 50 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) e. CC )
52 13 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` S ) e. CC )
53 25 gt0ne0d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) =/= 0 )
54 53 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` S ) =/= 0 )
55 51 52 54 divcan2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) = ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) )
56 45 55 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( F ` i ) ) = ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) )
57 56 oveq2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) = ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) ) )
58 49 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) e. CC )
59 10 58 pncan3d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) ) = ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) )
60 57 59 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) = ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) )
61 9 17 readdcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) e. RR )
62 61 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) e. CC )
63 48 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
64 62 63 22 34 divmul2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( B ` i ) <-> ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) = ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) ) )
65 60 64 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` T ) x. ( A ` i ) ) + ( ( sqrt ` S ) x. ( F ` i ) ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( B ` i ) )
66 4 recnd 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( sqrt ` T ) e. CC )
67 66 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` T ) e. CC )
68 8 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
69 67 68 22 34 div23d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( ( ( sqrt ` T ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( A ` i ) ) )
70 22 52 22 34 divsubdird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) )
71 12 recnd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. CC )
72 pncan2 
 |-  ( ( ( sqrt ` S ) e. CC /\ ( sqrt ` T ) e. CC ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) = ( sqrt ` T ) )
73 71 66 72 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) = ( sqrt ` T ) )
74 73 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) = ( sqrt ` T ) )
75 74 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( ( sqrt ` T ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
76 22 34 dividd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = 1 )
77 76 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) = ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) )
78 70 75 77 3eqtr3d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) )
79 78 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( A ` i ) ) = ( ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) x. ( A ` i ) ) )
80 69 79 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( A ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) x. ( A ` i ) ) )
81 16 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) e. CC )
82 52 81 22 34 div23d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) x. ( F ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( F ` i ) ) )
83 80 82 oveq12d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` T ) x. ( A ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) + ( ( ( sqrt ` S ) x. ( F ` i ) ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) = ( ( ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( F ` i ) ) ) )
84 35 65 83 3eqtr3d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) = ( ( ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( F ` i ) ) ) )
85 84 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( F ` i ) ) ) )