Metamath Proof Explorer

Theorem prodfdiv

Description: The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018)

Ref Expression
Hypotheses prodfdiv.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
prodfdiv.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
prodfdiv.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
prodfdiv.4 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) =/= 0 )
prodfdiv.5 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )
Assertion prodfdiv 
|- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) )

Proof

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 ffvelcdmda 
 |-  ( ( 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 ) ) )