Metamath Proof Explorer

Theorem clim2prod

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

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

Proof

Step Hyp Ref Expression
1 clim2prod.1 
 |-  Z = ( ZZ>= ` M )
2 clim2prod.2 
 |-  ( ph -> N e. Z )
3 clim2prod.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4 clim2prod.4 
 |-  ( ph -> seq ( N + 1 ) ( x. , F ) ~~> A )
5 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
6 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
7 1 6 eqsstri 
 |-  Z C_ ZZ
8 7 2 sselid 
 |-  ( ph -> N e. ZZ )
9 8 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
10 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 10 11 syl 
 |-  ( ph -> M e. ZZ )
13 1 12 3 prodf 
 |-  ( ph -> seq M ( x. , F ) : Z --> CC )
14 13 2 ffvelcdmd 
 |-  ( ph -> ( seq M ( x. , F ) ` N ) e. CC )
15 seqex 
 |-  seq M ( x. , F ) e. _V
16 15 a1i 
 |-  ( ph -> seq M ( x. , F ) e. _V )
17 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
18 uzss 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` M ) )
19 10 17 18 3syl 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` M ) )
20 19 1 sseqtrrdi 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ Z )
21 20 sselda 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
22 21 3 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` k ) e. CC )
23 5 9 22 prodf 
 |-  ( ph -> seq ( N + 1 ) ( x. , F ) : ( ZZ>= ` ( N + 1 ) ) --> CC )
24 23 ffvelcdmda 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , F ) ` k ) e. CC )
25 fveq2 
 |-  ( x = ( N + 1 ) -> ( seq M ( x. , F ) ` x ) = ( seq M ( x. , F ) ` ( N + 1 ) ) )
26 fveq2 
 |-  ( x = ( N + 1 ) -> ( seq ( N + 1 ) ( x. , F ) ` x ) = ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) )
27 26 oveq2d 
 |-  ( x = ( N + 1 ) -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) ) )
28 25 27 eqeq12d 
 |-  ( x = ( N + 1 ) -> ( ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) <-> ( seq M ( x. , F ) ` ( N + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) ) ) )
29 28 imbi2d 
 |-  ( x = ( N + 1 ) -> ( ( ph -> ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) ) <-> ( ph -> ( seq M ( x. , F ) ` ( N + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) ) ) ) )
30 fveq2 
 |-  ( x = n -> ( seq M ( x. , F ) ` x ) = ( seq M ( x. , F ) ` n ) )
31 fveq2 
 |-  ( x = n -> ( seq ( N + 1 ) ( x. , F ) ` x ) = ( seq ( N + 1 ) ( x. , F ) ` n ) )
32 31 oveq2d 
 |-  ( x = n -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) )
33 30 32 eqeq12d 
 |-  ( x = n -> ( ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) <-> ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) )
34 33 imbi2d 
 |-  ( x = n -> ( ( ph -> ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) ) <-> ( ph -> ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) ) )
35 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq M ( x. , F ) ` x ) = ( seq M ( x. , F ) ` ( n + 1 ) ) )
36 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq ( N + 1 ) ( x. , F ) ` x ) = ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) )
37 36 oveq2d 
 |-  ( x = ( n + 1 ) -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) )
38 35 37 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) <-> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) ) )
39 38 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) ) <-> ( ph -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) ) ) )
40 fveq2 
 |-  ( x = k -> ( seq M ( x. , F ) ` x ) = ( seq M ( x. , F ) ` k ) )
41 fveq2 
 |-  ( x = k -> ( seq ( N + 1 ) ( x. , F ) ` x ) = ( seq ( N + 1 ) ( x. , F ) ` k ) )
42 41 oveq2d 
 |-  ( x = k -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` k ) ) )
43 40 42 eqeq12d 
 |-  ( x = k -> ( ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) <-> ( seq M ( x. , F ) ` k ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` k ) ) ) )
44 43 imbi2d 
 |-  ( x = k -> ( ( ph -> ( seq M ( x. , F ) ` x ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` x ) ) ) <-> ( ph -> ( seq M ( x. , F ) ` k ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` k ) ) ) ) )
45 10 adantr 
 |-  ( ( ph /\ ( N + 1 ) e. ZZ ) -> N e. ( ZZ>= ` M ) )
46 seqp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( seq M ( x. , F ) ` ( N + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( F ` ( N + 1 ) ) ) )
47 45 46 syl 
 |-  ( ( ph /\ ( N + 1 ) e. ZZ ) -> ( seq M ( x. , F ) ` ( N + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( F ` ( N + 1 ) ) ) )
48 seq1 
 |-  ( ( N + 1 ) e. ZZ -> ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) = ( F ` ( N + 1 ) ) )
49 48 adantl 
 |-  ( ( ph /\ ( N + 1 ) e. ZZ ) -> ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) = ( F ` ( N + 1 ) ) )
50 49 oveq2d 
 |-  ( ( ph /\ ( N + 1 ) e. ZZ ) -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) ) = ( ( seq M ( x. , F ) ` N ) x. ( F ` ( N + 1 ) ) ) )
51 47 50 eqtr4d 
 |-  ( ( ph /\ ( N + 1 ) e. ZZ ) -> ( seq M ( x. , F ) ` ( N + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) ) )
52 51 expcom 
 |-  ( ( N + 1 ) e. ZZ -> ( ph -> ( seq M ( x. , F ) ` ( N + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( N + 1 ) ) ) ) )
53 19 sselda 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> n e. ( ZZ>= ` M ) )
54 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
55 53 54 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
56 55 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
57 oveq1 
 |-  ( ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) -> ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) = ( ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) x. ( F ` ( n + 1 ) ) ) )
58 57 adantl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) = ( ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) x. ( F ` ( n + 1 ) ) ) )
59 14 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` N ) e. CC )
60 23 ffvelcdmda 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , F ) ` n ) e. CC )
61 peano2uz 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. ( ZZ>= ` M ) )
62 61 1 eleqtrrdi 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. Z )
63 53 62 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( n + 1 ) e. Z )
64 3 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
65 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
66 65 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. CC <-> ( F ` ( n + 1 ) ) e. CC ) )
67 66 rspcv 
 |-  ( ( n + 1 ) e. Z -> ( A. k e. Z ( F ` k ) e. CC -> ( F ` ( n + 1 ) ) e. CC ) )
68 64 67 mpan9 
 |-  ( ( ph /\ ( n + 1 ) e. Z ) -> ( F ` ( n + 1 ) ) e. CC )
69 63 68 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` ( n + 1 ) ) e. CC )
70 59 60 69 mulassd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) x. ( F ` ( n + 1 ) ) ) = ( ( seq M ( x. , F ) ` N ) x. ( ( seq ( N + 1 ) ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
71 70 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) x. ( F ` ( n + 1 ) ) ) = ( ( seq M ( x. , F ) ` N ) x. ( ( seq ( N + 1 ) ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
72 seqp1 
 |-  ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) = ( ( seq ( N + 1 ) ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
73 72 adantl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) = ( ( seq ( N + 1 ) ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
74 73 oveq2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) = ( ( seq M ( x. , F ) ` N ) x. ( ( seq ( N + 1 ) ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
75 74 adantr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) = ( ( seq M ( x. , F ) ` N ) x. ( ( seq ( N + 1 ) ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
76 71 75 eqtr4d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) x. ( F ` ( n + 1 ) ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) )
77 56 58 76 3eqtrd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) )
78 77 exp31 
 |-  ( ph -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) ) ) )
79 78 com12 
 |-  ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( ph -> ( ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) ) ) )
80 79 a2d 
 |-  ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( ( ph -> ( seq M ( x. , F ) ` n ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` n ) ) ) -> ( ph -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` ( n + 1 ) ) ) ) ) )
81 29 34 39 44 52 80 uzind4 
 |-  ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( ph -> ( seq M ( x. , F ) ` k ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` k ) ) ) )
82 81 impcom 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( x. , F ) ` k ) = ( ( seq M ( x. , F ) ` N ) x. ( seq ( N + 1 ) ( x. , F ) ` k ) ) )
83 5 9 4 14 16 24 82 climmulc2 
 |-  ( ph -> seq M ( x. , F ) ~~> ( ( seq M ( x. , F ) ` N ) x. A ) )