Metamath Proof Explorer

Theorem clim2div

Description: The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017)

Ref Expression
Hypotheses clim2div.1 
|- Z = ( ZZ>= ` M )
clim2div.2 
|- ( ph -> N e. Z )
clim2div.3 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
clim2div.4 
|- ( ph -> seq M ( x. , F ) ~~> A )
clim2div.5 
|- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )
Assertion clim2div 
|- ( ph -> seq ( N + 1 ) ( x. , F ) ~~> ( A / ( seq M ( x. , F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 clim2div.1 
 |-  Z = ( ZZ>= ` M )
2 clim2div.2 
 |-  ( ph -> N e. Z )
3 clim2div.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4 clim2div.4 
 |-  ( ph -> seq M ( x. , F ) ~~> A )
5 clim2div.5 
 |-  ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )
6 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
7 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
8 7 1 eleq2s 
 |-  ( N e. Z -> N e. ZZ )
9 2 8 syl 
 |-  ( ph -> N e. ZZ )
10 9 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 11 1 eleq2s 
 |-  ( N e. Z -> M e. ZZ )
13 2 12 syl 
 |-  ( ph -> M e. ZZ )
14 1 13 3 prodf 
 |-  ( ph -> seq M ( x. , F ) : Z --> CC )
15 14 2 ffvelrnd 
 |-  ( ph -> ( seq M ( x. , F ) ` N ) e. CC )
16 15 5 reccld 
 |-  ( ph -> ( 1 / ( seq M ( x. , F ) ` N ) ) e. CC )
17 seqex 
 |-  seq ( N + 1 ) ( x. , F ) e. _V
18 17 a1i 
 |-  ( ph -> seq ( N + 1 ) ( x. , F ) e. _V )
19 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
20 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
21 19 20 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
22 21 1 eleqtrrdi 
 |-  ( ph -> ( N + 1 ) e. Z )
23 1 uztrn2 
 |-  ( ( ( N + 1 ) e. Z /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. Z )
24 22 23 sylan 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. Z )
25 14 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( x. , F ) ` j ) e. CC )
26 24 25 syldan 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` j ) e. CC )
27 mulcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
28 27 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
29 mulass 
 |-  ( ( k e. CC /\ x e. CC /\ y e. CC ) -> ( ( k x. x ) x. y ) = ( k x. ( x x. y ) ) )
30 29 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> ( ( k x. x ) x. y ) = ( k x. ( x x. y ) ) )
31 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. ( ZZ>= ` ( N + 1 ) ) )
32 19 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ( ZZ>= ` M ) )
33 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
34 33 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
35 34 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
36 35 adantlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
37 28 30 31 32 36 seqsplit 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` j ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` j ) ) )
38 37 eqcomd 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` j ) ) = ( seq M ( x. , F ) ` j ) )
39 15 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` N ) e. CC )
40 1 uztrn2 
 |-  ( ( ( N + 1 ) e. Z /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
41 22 40 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
42 41 3 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` k ) e. CC )
43 6 10 42 prodf 
 |-  ( ph -> seq ( N + 1 ) ( x. , F ) : ( ZZ>= ` ( N + 1 ) ) --> CC )
44 43 ffvelrnda 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , F ) ` j ) e. CC )
45 5 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` N ) =/= 0 )
46 26 39 44 45 divmuld 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( seq M ( x. , F ) ` j ) / ( seq M ( x. , F ) ` N ) ) = ( seq ( N + 1 ) ( x. , F ) ` j ) <-> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` j ) ) = ( seq M ( x. , F ) ` j ) ) )
47 38 46 mpbird 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( seq M ( x. , F ) ` j ) / ( seq M ( x. , F ) ` N ) ) = ( seq ( N + 1 ) ( x. , F ) ` j ) )
48 26 39 45 divrec2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( seq M ( x. , F ) ` j ) / ( seq M ( x. , F ) ` N ) ) = ( ( 1 / ( seq M ( x. , F ) ` N ) ) x. ( seq M ( x. , F ) ` j ) ) )
49 47 48 eqtr3d 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , F ) ` j ) = ( ( 1 / ( seq M ( x. , F ) ` N ) ) x. ( seq M ( x. , F ) ` j ) ) )
50 6 10 4 16 18 26 49 climmulc2 
 |-  ( ph -> seq ( N + 1 ) ( x. , F ) ~~> ( ( 1 / ( seq M ( x. , F ) ` N ) ) x. A ) )
51 climcl 
 |-  ( seq M ( x. , F ) ~~> A -> A e. CC )
52 4 51 syl 
 |-  ( ph -> A e. CC )
53 52 15 5 divrec2d 
 |-  ( ph -> ( A / ( seq M ( x. , F ) ` N ) ) = ( ( 1 / ( seq M ( x. , F ) ` N ) ) x. A ) )
54 50 53 breqtrrd 
 |-  ( ph -> seq ( N + 1 ) ( x. , F ) ~~> ( A / ( seq M ( x. , F ) ` N ) ) )