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

Theorem axeuclidlem 25901
Description: Lemma for axeuclid 25902. Handle the algebraic aspects of the theorem. (Contributed by Scott Fenton, 9-Sep-2013.)
Assertion
Ref Expression
axeuclidlem  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
)  /\  A. i  e.  ( 1 ... N
) ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  ->  E. x  e.  ( EE `  N
) E. y  e.  ( EE `  N
) E. r  e.  ( 0 [,] 1
) E. s  e.  ( 0 [,] 1
) E. u  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... N
) ( ( B `
 i )  =  ( ( ( 1  -  r )  x.  ( A `  i
) )  +  ( r  x.  ( x `
 i ) ) )  /\  ( C `
 i )  =  ( ( ( 1  -  s )  x.  ( A `  i
) )  +  ( s  x.  ( y `
 i ) ) )  /\  ( T `
 i )  =  ( ( ( 1  -  u )  x.  ( x `  i
) )  +  ( u  x.  ( y `
 i ) ) ) ) )
Distinct variable groups:    A, i,
r, s, u, x, y    B, i, r, s, u, x, y    C, i, r, s, u, x, y    i, N, r, s, u, x, y    P, i, r, s, u, x, y    Q, i, r, s, u, x, y    T, i, r, s, u, x, y

Proof of Theorem axeuclidlem
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 simp21 990 . . 3  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
)  /\  A. i  e.  ( 1 ... N
) ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  ->  P  e.  ( 0 [,] 1
) )
2 simp22 991 . . 3  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
)  /\  A. i  e.  ( 1 ... N
) ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  ->  Q  e.  ( 0 [,] 1
) )
3 fveere 25840 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( A `  k )  e.  RR )
43expcom 425 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( A  e.  ( EE `  N )  ->  ( A `  k )  e.  RR ) )
5 fveere 25840 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( B `  k )  e.  RR )
65expcom 425 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( B  e.  ( EE `  N )  ->  ( B `  k )  e.  RR ) )
74, 6anim12d 547 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  ->  ( ( A `  k )  e.  RR  /\  ( B `
 k )  e.  RR ) ) )
8 fveere 25840 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( C `  k )  e.  RR )
98expcom 425 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( C  e.  ( EE `  N )  ->  ( C `  k )  e.  RR ) )
10 fveere 25840 . . . . . . . . . . . . 13  |-  ( ( T  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( T `  k )  e.  RR )
1110expcom 425 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( T  e.  ( EE `  N )  ->  ( T `  k )  e.  RR ) )
129, 11anim12d 547 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  (
( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N ) )  ->  ( ( C `  k )  e.  RR  /\  ( T `
 k )  e.  RR ) ) )
137, 12anim12d 547 . . . . . . . . . 10  |-  ( k  e.  ( 1 ... N )  ->  (
( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  -> 
( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) ) ) )
1413impcom 420 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  k  e.  ( 1 ... N ) )  ->  ( ( ( A `  k )  e.  RR  /\  ( B `  k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) ) )
15 unitssre 11042 . . . . . . . . . . . . . . . 16  |-  ( 0 [,] 1 )  C_  RR
1615sseli 3344 . . . . . . . . . . . . . . 15  |-  ( P  e.  ( 0 [,] 1 )  ->  P  e.  RR )
17163ad2ant1 978 . . . . . . . . . . . . . 14  |-  ( ( P  e.  ( 0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0 )  ->  P  e.  RR )
1817adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  P  e.  RR )
19 peano2rem 9367 . . . . . . . . . . . . 13  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
2018, 19syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( P  -  1 )  e.  RR )
21 simplll 735 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( A `  k
)  e.  RR )
2220, 21remulcld 9116 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( P  - 
1 )  x.  ( A `  k )
)  e.  RR )
23 simpllr 736 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( B `  k
)  e.  RR )
2422, 23readdcld 9115 . . . . . . . . . 10  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  e.  RR )
25 simpr3 965 . . . . . . . . . 10  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  P  =/=  0 )
2624, 18, 25redivcld 9842 . . . . . . . . 9  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( B `  k
) )  /  P
)  e.  RR )
2714, 26sylan 458 . . . . . . . 8  |-  ( ( ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  k  e.  ( 1 ... N ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( B `  k
) )  /  P
)  e.  RR )
2827an32s 780 . . . . . . 7  |-  ( ( ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  /\  k  e.  ( 1 ... N
) )  ->  (
( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P )  e.  RR )
2928ralrimiva 2789 . . . . . 6  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  A. k  e.  ( 1 ... N
) ( ( ( ( P  -  1 )  x.  ( A `
 k ) )  +  ( B `  k ) )  /  P )  e.  RR )
30 eleenn 25835 . . . . . . . 8  |-  ( A  e.  ( EE `  N )  ->  N  e.  NN )
3130ad3antrrr 711 . . . . . . 7  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  N  e.  NN )
32 mptelee 25834 . . . . . . 7  |-  ( N  e.  NN  ->  (
( k  e.  ( 1 ... N ) 
|->  ( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( B `  k
) )  /  P
) )  e.  ( EE `  N )  <->  A. k  e.  (
1 ... N ) ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P )  e.  RR ) )
3331, 32syl 16 . . . . . 6  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  (
( k  e.  ( 1 ... N ) 
|->  ( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( B `  k
) )  /  P
) )  e.  ( EE `  N )  <->  A. k  e.  (
1 ... N ) ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P )  e.  RR ) )
3429, 33mpbird 224 . . . . 5  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  (
k  e.  ( 1 ... N )  |->  ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P ) )  e.  ( EE
`  N ) )
35343adant3 977 . . . 4  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
)  /\  A. i  e.  ( 1 ... N
) ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  ->  ( k  e.  ( 1 ... N
)  |->  ( ( ( ( P  -  1 )  x.  ( A `
 k ) )  +  ( B `  k ) )  /  P ) )  e.  ( EE `  N
) )
36 simplrl 737 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( C `  k
)  e.  RR )
3722, 36readdcld 9115 . . . . . . . . . 10  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( C `  k ) )  e.  RR )
3837, 18, 25redivcld 9842 . . . . . . . . 9  |-  ( ( ( ( ( A `
 k )  e.  RR  /\  ( B `
 k )  e.  RR )  /\  (
( C `  k
)  e.  RR  /\  ( T `  k )  e.  RR ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( C `  k
) )  /  P
)  e.  RR )
3914, 38sylan 458 . . . . . . . 8  |-  ( ( ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  k  e.  ( 1 ... N ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( C `  k
) )  /  P
)  e.  RR )
4039an32s 780 . . . . . . 7  |-  ( ( ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  /\  k  e.  ( 1 ... N
) )  ->  (
( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( C `  k ) )  /  P )  e.  RR )
4140ralrimiva 2789 . . . . . 6  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  A. k  e.  ( 1 ... N
) ( ( ( ( P  -  1 )  x.  ( A `
 k ) )  +  ( C `  k ) )  /  P )  e.  RR )
42 mptelee 25834 . . . . . . 7  |-  ( N  e.  NN  ->  (
( k  e.  ( 1 ... N ) 
|->  ( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( C `  k
) )  /  P
) )  e.  ( EE `  N )  <->  A. k  e.  (
1 ... N ) ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( C `  k ) )  /  P )  e.  RR ) )
4331, 42syl 16 . . . . . 6  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  (
( k  e.  ( 1 ... N ) 
|->  ( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( C `  k
) )  /  P
) )  e.  ( EE `  N )  <->  A. k  e.  (
1 ... N ) ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( C `  k ) )  /  P )  e.  RR ) )
4441, 43mpbird 224 . . . . 5  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  (
k  e.  ( 1 ... N )  |->  ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( C `  k ) )  /  P ) )  e.  ( EE
`  N ) )
45443adant3 977 . . . 4  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
)  /\  A. i  e.  ( 1 ... N
) ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  ->  ( k  e.  ( 1 ... N
)  |->  ( ( ( ( P  -  1 )  x.  ( A `
 k ) )  +  ( C `  k ) )  /  P ) )  e.  ( EE `  N
) )
46 fveecn 25841 . . . . . . . . . . . 12  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
4746expcom 425 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( A  e.  ( EE `  N )  ->  ( A `  i )  e.  CC ) )
48 fveecn 25841 . . . . . . . . . . . 12  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
4948expcom 425 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( B  e.  ( EE `  N )  ->  ( B `  i )  e.  CC ) )
5047, 49anim12d 547 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... N )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  ->  ( ( A `  i )  e.  CC  /\  ( B `
 i )  e.  CC ) ) )
51 fveecn 25841 . . . . . . . . . . . 12  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
5251expcom 425 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( C  e.  ( EE `  N )  ->  ( C `  i )  e.  CC ) )
53 fveecn 25841 . . . . . . . . . . . 12  |-  ( ( T  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( T `  i )  e.  CC )
5453expcom 425 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( T  e.  ( EE `  N )  ->  ( T `  i )  e.  CC ) )
5552, 54anim12d 547 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... N )  ->  (
( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N ) )  ->  ( ( C `  i )  e.  CC  /\  ( T `
 i )  e.  CC ) ) )
5650, 55anim12d 547 . . . . . . . . 9  |-  ( i  e.  ( 1 ... N )  ->  (
( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  -> 
( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) ) ) )
5756impcom 420 . . . . . . . 8  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  i  e.  ( 1 ... N ) )  ->  ( ( ( A `  i )  e.  CC  /\  ( B `  i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) ) )
58 eqcom 2438 . . . . . . . . . . . . . 14  |-  ( ( T `  i )  =  ( ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) )  /  P )  <->  ( (
( ( ( 1  -  Q )  x.  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i ) ) ) )  +  ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) ) )  /  P )  =  ( T `  i ) )
59 ax-1cn 9048 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
60 simpr2 964 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  Q  e.  ( 0 [,] 1 ) )
6115sseli 3344 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Q  e.  ( 0 [,] 1 )  ->  Q  e.  RR )
6261recnd 9114 . . . . . . . . . . . . . . . . . . . 20  |-  ( Q  e.  ( 0 [,] 1 )  ->  Q  e.  CC )
6360, 62syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  Q  e.  CC )
64 subcl 9305 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  Q  e.  CC )  ->  ( 1  -  Q
)  e.  CC )
6559, 63, 64sylancr 645 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( 1  -  Q
)  e.  CC )
66 simpr1 963 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  P  e.  ( 0 [,] 1 ) )
6716recnd 9114 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ( 0 [,] 1 )  ->  P  e.  CC )
6866, 67syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  P  e.  CC )
69 subcl 9305 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e.  CC  /\  1  e.  CC )  ->  ( P  -  1 )  e.  CC )
7068, 59, 69sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( P  -  1 )  e.  CC )
71 simplll 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( A `  i
)  e.  CC )
7270, 71mulcld 9108 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( P  - 
1 )  x.  ( A `  i )
)  e.  CC )
7365, 72mulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  e.  CC )
7463, 72mulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  e.  CC )
7573, 74addcld 9107 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  Q )  x.  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i ) ) ) )  e.  CC )
76 simpllr 736 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( B `  i
)  e.  CC )
7765, 76mulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  Q )  x.  ( B `  i )
)  e.  CC )
78 simplrl 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( C `  i
)  e.  CC )
7963, 78mulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( Q  x.  ( C `  i )
)  e.  CC )
8077, 79addcld 9107 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  Q )  x.  ( B `  i
) )  +  ( Q  x.  ( C `
 i ) ) )  e.  CC )
8175, 80addcld 9107 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  e.  CC )
82 simplrr 738 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( T `  i
)  e.  CC )
83 simpr3 965 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  P  =/=  0 )
8481, 68, 82, 83divmuld 9812 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) )  /  P )  =  ( T `  i )  <-> 
( P  x.  ( T `  i )
)  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) ) ) )
8558, 84syl5bb 249 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( T `  i )  =  ( ( ( ( ( 1  -  Q )  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  /  P )  <-> 
( P  x.  ( T `  i )
)  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) ) ) )
86 negsubdi2 9360 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  CC )  -> 
-u ( 1  -  P )  =  ( P  -  1 ) )
8759, 68, 86sylancr 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  -u ( 1  -  P
)  =  ( P  -  1 ) )
8887oveq1d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( -u ( 1  -  P )  x.  ( A `  i )
)  =  ( ( P  -  1 )  x.  ( A `  i ) ) )
89 subcl 9305 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  CC )  ->  ( 1  -  P
)  e.  CC )
9059, 68, 89sylancr 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( 1  -  P
)  e.  CC )
9190, 71mulneg1d 9486 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( -u ( 1  -  P )  x.  ( A `  i )
)  =  -u (
( 1  -  P
)  x.  ( A `
 i ) ) )
92 npcan 9314 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  CC  /\  Q  e.  CC )  ->  ( ( 1  -  Q )  +  Q
)  =  1 )
9359, 63, 92sylancr 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  Q )  +  Q
)  =  1 )
9493oveq1d 6096 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  Q )  +  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  =  ( 1  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )
9565, 63, 72adddird 9113 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  Q )  +  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  =  ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( ( P  - 
1 )  x.  ( A `  i )
) ) ) )
9672mulid2d 9106 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( 1  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  =  ( ( P  -  1 )  x.  ( A `  i ) ) )
9794, 95, 963eqtr3rd 2477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( P  - 
1 )  x.  ( A `  i )
)  =  ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( ( P  - 
1 )  x.  ( A `  i )
) ) ) )
9888, 91, 973eqtr3d 2476 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  ->  -u ( ( 1  -  P )  x.  ( A `  i )
)  =  ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( ( P  - 
1 )  x.  ( A `  i )
) ) ) )
9998oveq2d 6097 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) )  +  -u ( ( 1  -  P )  x.  ( A `  i )
) )  =  ( ( ( ( 1  -  Q )  x.  ( B `  i
) )  +  ( Q  x.  ( C `
 i ) ) )  +  ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( ( P  - 
1 )  x.  ( A `  i )
) ) ) ) )
10090, 71mulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  P )  x.  ( A `  i )
)  e.  CC )
10180, 100negsubd 9417 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) )  +  -u ( ( 1  -  P )  x.  ( A `  i )
) )  =  ( ( ( ( 1  -  Q )  x.  ( B `  i
) )  +  ( Q  x.  ( C `
 i ) ) )  -  ( ( 1  -  P )  x.  ( A `  i ) ) ) )
10280, 75addcomd 9268 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) )  +  ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) ) )  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) ) )
10399, 101, 1023eqtr3d 2476 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) )  -  (
( 1  -  P
)  x.  ( A `
 i ) ) )  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) ) )
104103eqeq1d 2444 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) )  -  (
( 1  -  P
)  x.  ( A `
 i ) ) )  =  ( P  x.  ( T `  i ) )  <->  ( (
( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) )  =  ( P  x.  ( T `  i )
) ) )
105 eqcom 2438 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 1  -  Q )  x.  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i ) ) ) )  +  ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) ) )  =  ( P  x.  ( T `  i )
)  <->  ( P  x.  ( T `  i ) )  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) ) ) )
106104, 105syl6bb 253 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) )  -  (
( 1  -  P
)  x.  ( A `
 i ) ) )  =  ( P  x.  ( T `  i ) )  <->  ( P  x.  ( T `  i
) )  =  ( ( ( ( 1  -  Q )  x.  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( Q  x.  ( ( P  -  1 )  x.  ( A `  i ) ) ) )  +  ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) ) ) ) )
10785, 106bitr4d 248 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( T `  i )  =  ( ( ( ( ( 1  -  Q )  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  /  P )  <-> 
( ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) )  -  (
( 1  -  P
)  x.  ( A `
 i ) ) )  =  ( P  x.  ( T `  i ) ) ) )
10873, 74, 77, 79add4d 9289 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( ( 1  -  Q )  x.  ( B `  i ) ) )  +  ( ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  ( C `  i )
) ) ) )
10965, 72, 76adddid 9112 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  Q )  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) ) )  =  ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( ( 1  -  Q )  x.  ( B `  i
) ) ) )
11063, 72, 78adddid 9112 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( Q  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) ) )  =  ( ( Q  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( C `  i ) ) ) )
111109, 110oveq12d 6099 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  Q )  x.  ( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) ) )  +  ( Q  x.  ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( C `  i ) ) ) )  =  ( ( ( ( 1  -  Q )  x.  (
( P  -  1 )  x.  ( A `
 i ) ) )  +  ( ( 1  -  Q )  x.  ( B `  i ) ) )  +  ( ( Q  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  ( C `  i )
) ) ) )
112108, 111eqtr4d 2471 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  =  ( ( ( 1  -  Q
)  x.  ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) ) )  +  ( Q  x.  ( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) ) ) ) )
113112oveq1d 6096 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( ( P  - 
1 )  x.  ( A `  i )
) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i
) )  +  ( Q  x.  ( C `
 i ) ) ) )  /  P
)  =  ( ( ( ( 1  -  Q )  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) ) )  +  ( Q  x.  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) ) ) )  /  P ) )
11472, 76addcld 9107 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) )  e.  CC )
11565, 114mulcld 9108 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  Q )  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) ) )  e.  CC )
11672, 78addcld 9107 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  e.  CC )
11763, 116mulcld 9108 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( Q  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) ) )  e.  CC )
118115, 117, 68, 83divdird 9828 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) )  +  ( Q  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) ) ) )  /  P
)  =  ( ( ( ( 1  -  Q )  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) ) )  /  P )  +  ( ( Q  x.  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) ) )  /  P ) ) )
11965, 114, 68, 83divassd 9825 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  Q )  x.  ( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) ) )  /  P
)  =  ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) ) )
12063, 116, 68, 83divassd 9825 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( Q  x.  ( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) ) )  /  P
)  =  ( Q  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( C `  i ) )  /  P ) ) )
121119, 120oveq12d 6099 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  Q )  x.  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) )  /  P )  +  ( ( Q  x.  (
( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) ) )  /  P ) )  =  ( ( ( 1  -  Q
)  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) )  +  ( Q  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) )  /  P
) ) ) )
122113, 118, 1213eqtrd 2472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( ( 1  -  Q
)  x.  ( ( P  -  1 )  x.  ( A `  i ) ) )  +  ( Q  x.  ( ( P  - 
1 )  x.  ( A `  i )
) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i
) )  +  ( Q  x.  ( C `
 i ) ) ) )  /  P
)  =  ( ( ( 1  -  Q
)  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) )  +  ( Q  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) )  /  P
) ) ) )
123122eqeq2d 2447 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( T `  i )  =  ( ( ( ( ( 1  -  Q )  x.  ( ( P  -  1 )  x.  ( A `  i
) ) )  +  ( Q  x.  (
( P  -  1 )  x.  ( A `
 i ) ) ) )  +  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  /  P )  <-> 
( T `  i
)  =  ( ( ( 1  -  Q
)  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) )  +  ( Q  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) )  /  P
) ) ) ) )
12468, 82mulcld 9108 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( P  x.  ( T `  i )
)  e.  CC )
12580, 100, 124subaddd 9429 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) )  -  (
( 1  -  P
)  x.  ( A `
 i ) ) )  =  ( P  x.  ( T `  i ) )  <->  ( (
( 1  -  P
)  x.  ( A `
 i ) )  +  ( P  x.  ( T `  i ) ) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) ) )
126107, 123, 1253bitr3rd 276 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) )  <-> 
( T `  i
)  =  ( ( ( 1  -  Q
)  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) )  +  ( Q  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) )  /  P
) ) ) ) )
127126biimpd 199 . . . . . . . . . 10  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) )  ->  ( T `  i )  =  ( ( ( 1  -  Q )  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) )  /  P ) )  +  ( Q  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( C `  i ) )  /  P ) ) ) ) )
128 npncan2 9328 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  CC  /\  P  e.  CC )  ->  ( ( 1  -  P )  +  ( P  -  1 ) )  =  0 )
12959, 68, 128sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( 1  -  P )  +  ( P  -  1 ) )  =  0 )
130129oveq1d 6096 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  P )  +  ( P  -  1 ) )  x.  ( A `  i )
)  =  ( 0  x.  ( A `  i ) ) )
13190, 70, 71adddird 9113 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  P )  +  ( P  -  1 ) )  x.  ( A `  i )
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( P  -  1 )  x.  ( A `  i
) ) ) )
132 mul02 9244 . . . . . . . . . . . . . . . 16  |-  ( ( A `  i )  e.  CC  ->  (
0  x.  ( A `
 i ) )  =  0 )
133132ad3antrrr 711 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( 0  x.  ( A `  i )
)  =  0 )
134130, 131, 1333eqtr3d 2476 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( ( P  -  1 )  x.  ( A `
 i ) ) )  =  0 )
135134oveq1d 6096 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( B `  i ) )  =  ( 0  +  ( B `  i ) ) )
136100, 72, 76addassd 9110 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( B `  i ) )  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) ) )
13776addid2d 9267 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( 0  +  ( B `  i ) )  =  ( B `
 i ) )
138135, 136, 1373eqtr3rd 2477 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( B `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) ) )
139114, 68, 83divcan2d 9792 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) )  /  P ) )  =  ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) ) )
140139oveq2d 6097 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) ) )  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) ) )
141138, 140eqtr4d 2471 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( B `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) ) ) )
142134oveq1d 6096 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( C `  i ) )  =  ( 0  +  ( C `  i ) ) )
143100, 72, 78addassd 9110 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( ( P  - 
1 )  x.  ( A `  i )
) )  +  ( C `  i ) )  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) ) ) )
14478addid2d 9267 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( 0  +  ( C `  i ) )  =  ( C `
 i ) )
145142, 143, 1443eqtr3rd 2477 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( C `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) ) ) )
146116, 68, 83divcan2d 9792 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) )  =  ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( C `  i ) ) )
147146oveq2d 6097 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) )  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) ) ) )
148145, 147eqtr4d 2471 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( C `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( C `  i
) )  /  P
) ) ) )
149141, 148jca 519 . . . . . . . . . 10  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( B `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i )
)  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) ) )  /\  ( C `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i )
)  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( C `  i ) )  /  P ) ) ) ) )
150127, 149jctild 528 . . . . . . . . 9  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) )  ->  ( ( ( B `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) )  /  P ) ) )  /\  ( C `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) ) )  /\  ( T `  i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) )  +  ( Q  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) ) ) ) )
151 df-3an 938 . . . . . . . . 9  |-  ( ( ( B `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) ) )  /\  ( C `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) )  /\  ( T `  i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) )  +  ( Q  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) ) )  <->  ( (
( B `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) ) )  /\  ( C `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) ) )  /\  ( T `  i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) )  +  ( Q  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) ) ) )
152150, 151syl6ibr 219 . . . . . . . 8  |-  ( ( ( ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC )  /\  (
( C `  i
)  e.  CC  /\  ( T `  i )  e.  CC ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) )  ->  ( ( B `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) ) )  /\  ( C `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) )  /\  ( T `
 i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) )  +  ( Q  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) ) ) ) )
15357, 152sylan 458 . . . . . . 7  |-  ( ( ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  i  e.  ( 1 ... N ) )  /\  ( P  e.  ( 0 [,] 1
)  /\  Q  e.  ( 0 [,] 1
)  /\  P  =/=  0 ) )  -> 
( ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) )  ->  ( ( B `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) ) )  /\  ( C `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) )  /\  ( T `
 i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) )  +  ( Q  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) ) ) ) )
154153an32s 780 . . . . . 6  |-  ( ( ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( T `
 i ) ) )  =  ( ( ( 1  -  Q
)  x.  ( B `
 i ) )  +  ( Q  x.  ( C `  i ) ) )  ->  (
( B `  i
)  =  ( ( ( 1  -  P
)  x.  ( A `
 i ) )  +  ( P  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) ) )  /\  ( C `  i )  =  ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) )  /\  ( T `  i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) )  +  ( Q  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( C `  i ) )  /  P ) ) ) ) ) )
155154ralimdva 2784 . . . . 5  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
) )  ->  ( A. i  e.  (
1 ... N ) ( ( ( 1  -  P )  x.  ( A `  i )
)  +  ( P  x.  ( T `  i ) ) )  =  ( ( ( 1  -  Q )  x.  ( B `  i ) )  +  ( Q  x.  ( C `  i )
) )  ->  A. i  e.  ( 1 ... N
) ( ( B `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) ) )  /\  ( C `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) )  /\  ( T `
 i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) )  +  ( Q  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) ) ) ) )
1561553impia 1150 . . . 4  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N
) ) )  /\  ( P  e.  (
0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0
)  /\  A. i  e.  ( 1 ... N
) ( ( ( 1  -  P )  x.  ( A `  i ) )  +  ( P  x.  ( T `  i )
) )  =  ( ( ( 1  -  Q )  x.  ( B `  i )
)  +  ( Q  x.  ( C `  i ) ) ) )  ->  A. i  e.  ( 1 ... N
) ( ( B `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) ) )  /\  ( C `
 i )  =  ( ( ( 1  -  P )  x.  ( A `  i
) )  +  ( P  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) )  /\  ( T `
 i )  =  ( ( ( 1  -  Q )  x.  ( ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) )  /  P
) )  +  ( Q  x.  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( C `
 i ) )  /  P ) ) ) ) )
157 fveq1 5727 . . . . . . . 8  |-  ( x  =  ( k  e.  ( 1 ... N
)  |->  ( ( ( ( P  -  1 )  x.  ( A `
 k ) )  +  ( B `  k ) )  /  P ) )  -> 
( x `  i
)  =  ( ( k  e.  ( 1 ... N )  |->  ( ( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P ) ) `  i ) )
158 fveq2 5728 . . . . . . . . . . . 12  |-  ( k  =  i  ->  ( A `  k )  =  ( A `  i ) )
159158oveq2d 6097 . . . . . . . . . . 11  |-  ( k  =  i  ->  (
( P  -  1 )  x.  ( A `
 k ) )  =  ( ( P  -  1 )  x.  ( A `  i
) ) )
160 fveq2 5728 . . . . . . . . . . 11  |-  ( k  =  i  ->  ( B `  k )  =  ( B `  i ) )
161159, 160oveq12d 6099 . . . . . . . . . 10  |-  ( k  =  i  ->  (
( ( P  - 
1 )  x.  ( A `  k )
)  +  ( B `
 k ) )  =  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) )
162161oveq1d 6096 . . . . . . . . 9  |-  ( k  =  i  ->  (
( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P )  =  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) )
163 eqid 2436 . . . . . . . . 9  |-  ( k  e.  ( 1 ... N )  |->  ( ( ( ( P  - 
1 )  x.  ( A `  k )
)  +  ( B `
 k ) )  /  P ) )  =  ( k  e.  ( 1 ... N
)  |->  ( ( ( ( P  -  1 )  x.  ( A `
 k ) )  +  ( B `  k ) )  /  P ) )
164 ovex 6106 . . . . . . . . 9  |-  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P )  e. 
_V
165162, 163, 164fvmpt 5806 . . . . . . . 8  |-  ( i  e.  ( 1 ... N )  ->  (
( k  e.  ( 1 ... N ) 
|->  ( ( ( ( P  -  1 )  x.  ( A `  k ) )  +  ( B `  k
) )  /  P
) ) `  i
)  =  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P ) )
166157, 165sylan9eq 2488 . . . . . . 7  |-  ( ( x  =  ( k  e.  ( 1 ... N )  |->  ( ( ( ( P  - 
1 )  x.  ( A `  k )
)  +  ( B `
 k ) )  /  P ) )  /\  i  e.  ( 1 ... N ) )  ->  ( x `  i )  =  ( ( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) )  /  P ) )
167 oveq2 6089 . . . . . . . . . 10  |-  ( ( x `  i )  =  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P )  ->  ( P  x.  ( x `  i ) )  =  ( P  x.  (
( ( ( P  -  1 )  x.  ( A `  i
) )  +  ( B `  i ) )  /  P ) ) )
168167oveq2d 6097 . . . . . . . . 9  |-  ( ( x `  i )  =  ( ( ( ( P  -  1 )