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

Theorem axeuclidlem 24662
Description: Lemma for axeuclid 24663. 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 988 . . 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 989 . . 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 24601 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( A `  k )  e.  RR )
43expcom 424 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( A  e.  ( EE `  N )  ->  ( A `  k )  e.  RR ) )
5 fveere 24601 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( B `  k )  e.  RR )
65expcom 424 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( B  e.  ( EE `  N )  ->  ( B `  k )  e.  RR ) )
74, 6anim12d 546 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  ->  ( ( A `  k )  e.  RR  /\  ( B `
 k )  e.  RR ) ) )
8 fveere 24601 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( C `  k )  e.  RR )
98expcom 424 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( C  e.  ( EE `  N )  ->  ( C `  k )  e.  RR ) )
10 fveere 24601 . . . . . . . . . . . . 13  |-  ( ( T  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( T `  k )  e.  RR )
1110expcom 424 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  ( T  e.  ( EE `  N )  ->  ( T `  k )  e.  RR ) )
129, 11anim12d 546 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  (
( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N ) )  ->  ( ( C `  k )  e.  RR  /\  ( T `
 k )  e.  RR ) ) )
137, 12anim12d 546 . . . . . . . . . 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 419 . . . . . . . . 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 0re 8854 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
16 1re 8853 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
17 iccssre 10747 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  ( 0 [,] 1
)  C_  RR )
1815, 16, 17mp2an 653 . . . . . . . . . . . . . . . 16  |-  ( 0 [,] 1 )  C_  RR
1918sseli 3189 . . . . . . . . . . . . . . 15  |-  ( P  e.  ( 0 [,] 1 )  ->  P  e.  RR )
20193ad2ant1 976 . . . . . . . . . . . . . 14  |-  ( ( P  e.  ( 0 [,] 1 )  /\  Q  e.  ( 0 [,] 1 )  /\  P  =/=  0 )  ->  P  e.  RR )
2120adantl 452 . . . . . . . . . . . . 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 )
22 peano2rem 9129 . . . . . . . . . . . . 13  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
2321, 22syl 15 . . . . . . . . . . . 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 )
24 simplll 734 . . . . . . . . . . . 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 )
2523, 24remulcld 8879 . . . . . . . . . . 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 )
26 simpllr 735 . . . . . . . . . . 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 )
2725, 26readdcld 8878 . . . . . . . . . 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 )
28 simpr3 963 . . . . . . . . . 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 )
2927, 21, 28redivcld 9604 . . . . . . . . 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 )
3014, 29sylan 457 . . . . . . . 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 )
3130an32s 779 . . . . . . 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 )
3231ralrimiva 2639 . . . . . 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 )
33 eleenn 24596 . . . . . . . 8  |-  ( A  e.  ( EE `  N )  ->  N  e.  NN )
3433ad3antrrr 710 . . . . . . 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 )
35 mptelee 24595 . . . . . . 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 ) )
3634, 35syl 15 . . . . . 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 ) )
3732, 36mpbird 223 . . . . 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 ) )
38373adant3 975 . . . 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
) )
39 simplrl 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 ) )  -> 
( C `  k
)  e.  RR )
4025, 39readdcld 8878 . . . . . . . . . 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 )
4140, 21, 28redivcld 9604 . . . . . . . . 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 )
4214, 41sylan 457 . . . . . . . 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 )
4342an32s 779 . . . . . . 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 )
4443ralrimiva 2639 . . . . . 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 )
45 mptelee 24595 . . . . . . 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 ) )
4634, 45syl 15 . . . . . 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 ) )
4744, 46mpbird 223 . . . . 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 ) )
48473adant3 975 . . . 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
) )
49 fveecn 24602 . . . . . . . . . . . 12  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
5049expcom 424 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( A  e.  ( EE `  N )  ->  ( A `  i )  e.  CC ) )
51 fveecn 24602 . . . . . . . . . . . 12  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
5251expcom 424 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( B  e.  ( EE `  N )  ->  ( B `  i )  e.  CC ) )
5350, 52anim12d 546 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... N )  ->  (
( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N ) )  ->  ( ( A `  i )  e.  CC  /\  ( B `
 i )  e.  CC ) ) )
54 fveecn 24602 . . . . . . . . . . . 12  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
5554expcom 424 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( C  e.  ( EE `  N )  ->  ( C `  i )  e.  CC ) )
56 fveecn 24602 . . . . . . . . . . . 12  |-  ( ( T  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( T `  i )  e.  CC )
5756expcom 424 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... N )  ->  ( T  e.  ( EE `  N )  ->  ( T `  i )  e.  CC ) )
5855, 57anim12d 546 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... N )  ->  (
( C  e.  ( EE `  N )  /\  T  e.  ( EE `  N ) )  ->  ( ( C `  i )  e.  CC  /\  ( T `
 i )  e.  CC ) ) )
5953, 58anim12d 546 . . . . . . . . 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 ) ) ) )
6059impcom 419 . . . . . . . 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 ) ) )
61 eqcom 2298 . . . . . . . . . . . . . 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 ) )
62 ax-1cn 8811 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
63 simpr2 962 . . . . . . . . . . . . . . . . . . . 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 ) )
6418sseli 3189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Q  e.  ( 0 [,] 1 )  ->  Q  e.  RR )
6564recnd 8877 . . . . . . . . . . . . . . . . . . . 20  |-  ( Q  e.  ( 0 [,] 1 )  ->  Q  e.  CC )
6663, 65syl 15 . . . . . . . . . . . . . . . . . . 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 )
67 subcl 9067 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  Q  e.  CC )  ->  ( 1  -  Q
)  e.  CC )
6862, 66, 67sylancr 644 . . . . . . . . . . . . . . . . . 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 )
69 simpr1 961 . . . . . . . . . . . . . . . . . . . . 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 ) )
7019recnd 8877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ( 0 [,] 1 )  ->  P  e.  CC )
7169, 70syl 15 . . . . . . . . . . . . . . . . . . . 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 )
72 subcl 9067 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e.  CC  /\  1  e.  CC )  ->  ( P  -  1 )  e.  CC )
7371, 62, 72sylancl 643 . . . . . . . . . . . . . . . . . . 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 )
74 simplll 734 . . . . . . . . . . . . . . . . . . 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 )
7573, 74mulcld 8871 . . . . . . . . . . . . . . . . . 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 )
7668, 75mulcld 8871 . . . . . . . . . . . . . . . . 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 )
7766, 75mulcld 8871 . . . . . . . . . . . . . . . . 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 )
7876, 77addcld 8870 . . . . . . . . . . . . . . . 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 )
79 simpllr 735 . . . . . . . . . . . . . . . . . 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 )
8068, 79mulcld 8871 . . . . . . . . . . . . . . . . 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 )
81 simplrl 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 ) )  -> 
( C `  i
)  e.  CC )
8266, 81mulcld 8871 . . . . . . . . . . . . . . . . 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 )
8380, 82addcld 8870 . . . . . . . . . . . . . . . 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 )
8478, 83addcld 8870 . . . . . . . . . . . . . . 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 )
85 simplrr 737 . . . . . . . . . . . . . . 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 )
86 simpr3 963 . . . . . . . . . . . . . . 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 )
8784, 71, 85, 86divmuld 9574 . . . . . . . . . . . . . 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 )
) ) ) ) )
8861, 87syl5bb 248 . . . . . . . . . . . . 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 )
) ) ) ) )
89 negsubdi2 9122 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  CC )  -> 
-u ( 1  -  P )  =  ( P  -  1 ) )
9062, 71, 89sylancr 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 ) )  ->  -u ( 1  -  P
)  =  ( P  -  1 ) )
9190oveq1d 5889 . . . . . . . . . . . . . . . . . 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 ) ) )
92 subcl 9067 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  CC )  ->  ( 1  -  P
)  e.  CC )
9362, 71, 92sylancr 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 ) )  -> 
( 1  -  P
)  e.  CC )
9493, 74mulneg1d 9248 . . . . . . . . . . . . . . . . . 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 ) ) )
95 npcan 9076 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  CC  /\  Q  e.  CC )  ->  ( ( 1  -  Q )  +  Q
)  =  1 )
9662, 66, 95sylancr 644 . . . . . . . . . . . . . . . . . . . 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 )
9796oveq1d 5889 . . . . . . . . . . . . . . . . . . 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
) ) ) )
9868, 66, 75adddird 8876 . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
9975mulid2d 8869 . . . . . . . . . . . . . . . . . . 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 ) ) )
10097, 98, 993eqtr3rd 2337 . . . . . . . . . . . . . . . . . 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 )
) ) ) )
10191, 94, 1003eqtr3d 2336 . . . . . . . . . . . . . . . . 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 )
) ) ) )
102101oveq2d 5890 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
10393, 74mulcld 8871 . . . . . . . . . . . . . . . . 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 )
10483, 103negsubd 9179 . . . . . . . . . . . . . . . 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 ) ) ) )
10583, 78addcomd 9030 . . . . . . . . . . . . . . . 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 )
) ) ) )
106102, 104, 1053eqtr3d 2336 . . . . . . . . . . . . . . 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 )
) ) ) )
107106eqeq1d 2304 . . . . . . . . . . . . . 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 )
) ) )
108 eqcom 2298 . . . . . . . . . . . . . 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 )
) ) ) )
109107, 108syl6bb 252 . . . . . . . . . . . . 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 ) ) ) ) ) )
11088, 109bitr4d 247 . . . . . . . . . . . 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 ) ) ) )
11176, 77, 80, 82add4d 9051 . . . . . . . . . . . . . . . 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 )
) ) ) )
11268, 75, 79adddid 8875 . . . . . . . . . . . . . . . . 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
) ) ) )
11366, 75, 81adddid 8875 . . . . . . . . . . . . . . . . 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 ) ) ) )
114112, 113oveq12d 5892 . . . . . . . . . . . . . . . 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 )
) ) ) )
115111, 114eqtr4d 2331 . . . . . . . . . . . . . . 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 ) ) ) ) )
116115oveq1d 5889 . . . . . . . . . . . . . 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 ) )
11775, 79addcld 8870 . . . . . . . . . . . . . . . 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 )
11868, 117mulcld 8871 . . . . . . . . . . . . . . 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 )
11975, 81addcld 8870 . . . . . . . . . . . . . . . 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 )
12066, 119mulcld 8871 . . . . . . . . . . . . . . 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 )
121118, 120, 71, 86divdird 9590 . . . . . . . . . . . . . 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 ) ) )
12268, 117, 71, 86divassd 9587 . . . . . . . . . . . . . . 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 ) ) )
12366, 119, 71, 86divassd 9587 . . . . . . . . . . . . . . 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 ) ) )
124122, 123oveq12d 5892 . . . . . . . . . . . . . 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
) ) ) )
125116, 121, 1243eqtrd 2332 . . . . . . . . . . . . 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
) ) ) )
126125eqeq2d 2307 . . . . . . . . . . . 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
) ) ) ) )
12771, 85mulcld 8871 . . . . . . . . . . . . 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 )
12883, 103, 127subaddd 9191 . . . . . . . . . . . 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 ) ) ) ) )
129110, 126, 1283bitr3rd 275 . . . . . . . . . . 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
) ) ) ) )
130129biimpd 198 . . . . . . . . . 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 ) ) ) ) )
131 npncan2 9090 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  CC  /\  P  e.  CC )  ->  ( ( 1  -  P )  +  ( P  -  1 ) )  =  0 )
13262, 71, 131sylancr 644 . . . . . . . . . . . . . . . 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 )
133132oveq1d 5889 . . . . . . . . . . . . . . 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 ) ) )
13493, 73, 74adddird 8876 . . . . . . . . . . . . . . 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
) ) ) )
135 mul02 9006 . . . . . . . . . . . . . . . 16  |-  ( ( A `  i )  e.  CC  ->  (
0  x.  ( A `
 i ) )  =  0 )
136135ad3antrrr 710 . . . . . . . . . . . . . . 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 )
137133, 134, 1363eqtr3d 2336 . . . . . . . . . . . . . 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 )
138137oveq1d 5889 . . . . . . . . . . . . 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 ) ) )
139103, 75, 79addassd 8873 . . . . . . . . . . . . 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
) ) ) )
14079addid2d 9029 . . . . . . . . . . . . 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 ) )
141138, 139, 1403eqtr3rd 2337 . . . . . . . . . . . 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
) ) ) )
142117, 71, 86divcan2d 9554 . . . . . . . . . . . . 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 ) ) )
143142oveq2d 5890 . . . . . . . . . . . 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
) ) ) )
144141, 143eqtr4d 2331 . . . . . . . . . . 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
) ) ) )
145137oveq1d 5889 . . . . . . . . . . . . 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 ) ) )
146103, 75, 81addassd 8873 . . . . . . . . . . . . 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
) ) ) )
14781addid2d 9029 . . . . . . . . . . . . 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 ) )
148145, 146, 1473eqtr3rd 2337 . . . . . . . . . . . 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
) ) ) )
149119, 71, 86divcan2d 9554 . . . . . . . . . . . . 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 ) ) )
150149oveq2d 5890 . . . . . . . . . . . 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
) ) ) )
151148, 150eqtr4d 2331 . . . . . . . . . . 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
) ) ) )
152144, 151jca 518 . . . . . . . . . 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 ) ) ) ) )
153130, 152jctild 527 . . . . . . . . 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 ) ) ) ) ) )
154 df-3an 936 . . . . . . . . 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 ) ) ) ) )
155153, 154syl6ibr 218 . . . . . . . 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 ) ) ) ) ) )
15660, 155sylan 457 . . . . . . 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 ) ) ) ) ) )
157156an32s 779 . . . . . 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 ) ) ) ) ) )
158157ralimdva 2634 . . . . 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 ) ) ) ) ) )
1591583impia 1148 . . . 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 ) ) ) ) )
160 fveq1 5540 . . . . . . . 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 ) )
161 fveq2 5541 . . . . . . . . . . . 12  |-  ( k  =  i  ->  ( A `  k )  =  ( A `  i ) )
162161oveq2d 5890 . . . . . . . . . . 11  |-  ( k  =  i  ->  (
( P  -  1 )  x.  ( A `
 k ) )  =  ( ( P  -  1 )  x.  ( A `  i
) ) )
163 fveq2 5541 . . . . . . . . . . 11  |-  ( k  =  i  ->  ( B `  k )  =  ( B `  i ) )
164162, 163oveq12d 5892 . . . . . . . . . 10  |-  ( k  =  i  ->  (
( ( P  - 
1 )  x.  ( A `  k )
)  +  ( B `
 k ) )  =  ( ( ( P  -  1 )  x.  ( A `  i ) )  +  ( B `  i
) ) )
165164oveq1d 5889 . . . . . . . . 9  |-  ( k  =  i  ->  (
( ( ( P  -  1 )  x.  ( A `  k
) )  +  ( B `  k ) )  /  P )  =  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P ) )
166 eqid 2296 . . . . . . . . 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 ) )
167 ovex 5899 . . . . . . . . 9  |-  ( ( ( ( P  - 
1 )  x.  ( A `  i )
)  +  ( B `
 i ) )  /  P )  e. 
_V
168165, 166, 167fvmpt 5618 . . . . . . . 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 ) )
169160, 168sylan9eq 2348 . . . . . . 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 ) )
170 oveq2 5882 . . . . . . . . . 10  |-  ( ( x `  i )  =  ( ( ( ( P  -  1 )  x.  ( A `
 i ) )  +  ( B `  i ) )  /  P )  ->  ( P  x.  ( x `  i ) )  =  ( P  x.  (
( ( (