Metamath Proof Explorer

Theorem climneg

Description: Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climneg.1 
|- F/ k ph
climneg.2 
|- F/_ k F
climneg.3 
|- Z = ( ZZ>= ` M )
climneg.4 
|- ( ph -> M e. ZZ )
climneg.5 
|- ( ph -> F ~~> A )
climneg.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
Assertion climneg 
|- ( ph -> ( k e. Z |-> -u ( F ` k ) ) ~~> -u A )

Proof

Step Hyp Ref Expression
1 climneg.1 
 |-  F/ k ph
2 climneg.2 
 |-  F/_ k F
3 climneg.3 
 |-  Z = ( ZZ>= ` M )
4 climneg.4 
 |-  ( ph -> M e. ZZ )
5 climneg.5 
 |-  ( ph -> F ~~> A )
6 climneg.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 nfmpt1 
 |-  F/_ k ( k e. Z |-> -u 1 )
8 nfmpt1 
 |-  F/_ k ( k e. Z |-> -u ( F ` k ) )
9 3 fvexi 
 |-  Z e. _V
10 9 mptex 
 |-  ( k e. Z |-> -u 1 ) e. _V
11 10 a1i 
 |-  ( ph -> ( k e. Z |-> -u 1 ) e. _V )
12 1cnd 
 |-  ( ph -> 1 e. CC )
13 12 negcld 
 |-  ( ph -> -u 1 e. CC )
14 eqidd 
 |-  ( j e. Z -> ( k e. Z |-> -u 1 ) = ( k e. Z |-> -u 1 ) )
15 eqidd 
 |-  ( ( j e. Z /\ k = j ) -> -u 1 = -u 1 )
16 id 
 |-  ( j e. Z -> j e. Z )
17 1cnd 
 |-  ( j e. Z -> 1 e. CC )
18 17 negcld 
 |-  ( j e. Z -> -u 1 e. CC )
19 14 15 16 18 fvmptd 
 |-  ( j e. Z -> ( ( k e. Z |-> -u 1 ) ` j ) = -u 1 )
20 19 adantl 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> -u 1 ) ` j ) = -u 1 )
21 3 4 11 13 20 climconst 
 |-  ( ph -> ( k e. Z |-> -u 1 ) ~~> -u 1 )
22 9 mptex 
 |-  ( k e. Z |-> -u ( F ` k ) ) e. _V
23 22 a1i 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) e. _V )
24 neg1cn 
 |-  -u 1 e. CC
25 eqid 
 |-  ( k e. Z |-> -u 1 ) = ( k e. Z |-> -u 1 )
26 25 fvmpt2 
 |-  ( ( k e. Z /\ -u 1 e. CC ) -> ( ( k e. Z |-> -u 1 ) ` k ) = -u 1 )
27 24 26 mpan2 
 |-  ( k e. Z -> ( ( k e. Z |-> -u 1 ) ` k ) = -u 1 )
28 27 24 eqeltrdi 
 |-  ( k e. Z -> ( ( k e. Z |-> -u 1 ) ` k ) e. CC )
29 28 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> -u 1 ) ` k ) e. CC )
30 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
31 6 negcld 
 |-  ( ( ph /\ k e. Z ) -> -u ( F ` k ) e. CC )
32 eqid 
 |-  ( k e. Z |-> -u ( F ` k ) ) = ( k e. Z |-> -u ( F ` k ) )
33 32 fvmpt2 
 |-  ( ( k e. Z /\ -u ( F ` k ) e. CC ) -> ( ( k e. Z |-> -u ( F ` k ) ) ` k ) = -u ( F ` k ) )
34 30 31 33 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> -u ( F ` k ) ) ` k ) = -u ( F ` k ) )
35 6 mulm1d 
 |-  ( ( ph /\ k e. Z ) -> ( -u 1 x. ( F ` k ) ) = -u ( F ` k ) )
36 27 eqcomd 
 |-  ( k e. Z -> -u 1 = ( ( k e. Z |-> -u 1 ) ` k ) )
37 36 adantl 
 |-  ( ( ph /\ k e. Z ) -> -u 1 = ( ( k e. Z |-> -u 1 ) ` k ) )
38 37 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( -u 1 x. ( F ` k ) ) = ( ( ( k e. Z |-> -u 1 ) ` k ) x. ( F ` k ) ) )
39 34 35 38 3eqtr2d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> -u ( F ` k ) ) ` k ) = ( ( ( k e. Z |-> -u 1 ) ` k ) x. ( F ` k ) ) )
40 1 7 2 8 3 4 21 23 5 29 6 39 climmulf 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) ~~> ( -u 1 x. A ) )
41 climcl 
 |-  ( F ~~> A -> A e. CC )
42 5 41 syl 
 |-  ( ph -> A e. CC )
43 42 mulm1d 
 |-  ( ph -> ( -u 1 x. A ) = -u A )
44 40 43 breqtrd 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) ~~> -u A )