Step |
Hyp |
Ref |
Expression |
1 |
|
prodfdiv.1 |
|- ( ph -> N e. ( ZZ>= ` M ) ) |
2 |
|
prodfdiv.2 |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC ) |
3 |
|
prodfdiv.3 |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC ) |
4 |
|
prodfdiv.4 |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) =/= 0 ) |
5 |
|
prodfdiv.5 |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) ) |
6 |
|
fveq2 |
|- ( n = k -> ( G ` n ) = ( G ` k ) ) |
7 |
6
|
oveq2d |
|- ( n = k -> ( 1 / ( G ` n ) ) = ( 1 / ( G ` k ) ) ) |
8 |
|
eqid |
|- ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) = ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) |
9 |
|
ovex |
|- ( 1 / ( G ` k ) ) e. _V |
10 |
7 8 9
|
fvmpt |
|- ( k e. ( M ... N ) -> ( ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ` k ) = ( 1 / ( G ` k ) ) ) |
11 |
10
|
adantl |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ` k ) = ( 1 / ( G ` k ) ) ) |
12 |
1 3 4 11
|
prodfrec |
|- ( ph -> ( seq M ( x. , ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ) ` N ) = ( 1 / ( seq M ( x. , G ) ` N ) ) ) |
13 |
12
|
oveq2d |
|- ( ph -> ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ) ` N ) ) = ( ( seq M ( x. , F ) ` N ) x. ( 1 / ( seq M ( x. , G ) ` N ) ) ) ) |
14 |
|
eleq1w |
|- ( k = n -> ( k e. ( M ... N ) <-> n e. ( M ... N ) ) ) |
15 |
14
|
anbi2d |
|- ( k = n -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ n e. ( M ... N ) ) ) ) |
16 |
|
fveq2 |
|- ( k = n -> ( G ` k ) = ( G ` n ) ) |
17 |
16
|
eleq1d |
|- ( k = n -> ( ( G ` k ) e. CC <-> ( G ` n ) e. CC ) ) |
18 |
15 17
|
imbi12d |
|- ( k = n -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC ) <-> ( ( ph /\ n e. ( M ... N ) ) -> ( G ` n ) e. CC ) ) ) |
19 |
18 3
|
chvarvv |
|- ( ( ph /\ n e. ( M ... N ) ) -> ( G ` n ) e. CC ) |
20 |
16
|
neeq1d |
|- ( k = n -> ( ( G ` k ) =/= 0 <-> ( G ` n ) =/= 0 ) ) |
21 |
15 20
|
imbi12d |
|- ( k = n -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) =/= 0 ) <-> ( ( ph /\ n e. ( M ... N ) ) -> ( G ` n ) =/= 0 ) ) ) |
22 |
21 4
|
chvarvv |
|- ( ( ph /\ n e. ( M ... N ) ) -> ( G ` n ) =/= 0 ) |
23 |
19 22
|
reccld |
|- ( ( ph /\ n e. ( M ... N ) ) -> ( 1 / ( G ` n ) ) e. CC ) |
24 |
23
|
fmpttd |
|- ( ph -> ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) : ( M ... N ) --> CC ) |
25 |
24
|
ffvelrnda |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ` k ) e. CC ) |
26 |
2 3 4
|
divrecd |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( ( F ` k ) / ( G ` k ) ) = ( ( F ` k ) x. ( 1 / ( G ` k ) ) ) ) |
27 |
11
|
oveq2d |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( ( F ` k ) x. ( ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ` k ) ) = ( ( F ` k ) x. ( 1 / ( G ` k ) ) ) ) |
28 |
26 5 27
|
3eqtr4d |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) x. ( ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ` k ) ) ) |
29 |
1 2 25 28
|
prodfmul |
|- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , ( n e. ( M ... N ) |-> ( 1 / ( G ` n ) ) ) ) ` N ) ) ) |
30 |
|
mulcl |
|- ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC ) |
31 |
30
|
adantl |
|- ( ( ph /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC ) |
32 |
1 2 31
|
seqcl |
|- ( ph -> ( seq M ( x. , F ) ` N ) e. CC ) |
33 |
1 3 31
|
seqcl |
|- ( ph -> ( seq M ( x. , G ) ` N ) e. CC ) |
34 |
1 3 4
|
prodfn0 |
|- ( ph -> ( seq M ( x. , G ) ` N ) =/= 0 ) |
35 |
32 33 34
|
divrecd |
|- ( ph -> ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) = ( ( seq M ( x. , F ) ` N ) x. ( 1 / ( seq M ( x. , G ) ` N ) ) ) ) |
36 |
13 29 35
|
3eqtr4d |
|- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) ) |