Metamath Proof Explorer

Theorem climsubmpt

Description: Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses climsubmpt.k 
|- F/ k ph
climsubmpt.z 
|- Z = ( ZZ>= ` M )
climsubmpt.m 
|- ( ph -> M e. ZZ )
climsubmpt.a 
|- ( ( ph /\ k e. Z ) -> A e. CC )
climsubmpt.b 
|- ( ( ph /\ k e. Z ) -> B e. CC )
climsubmpt.c 
|- ( ph -> ( k e. Z |-> A ) ~~> C )
climsubmpt.d 
|- ( ph -> ( k e. Z |-> B ) ~~> D )
Assertion climsubmpt 
|- ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( C - D ) )

Proof

Step Hyp Ref Expression
1 climsubmpt.k 
 |-  F/ k ph
2 climsubmpt.z 
 |-  Z = ( ZZ>= ` M )
3 climsubmpt.m 
 |-  ( ph -> M e. ZZ )
4 climsubmpt.a 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
5 climsubmpt.b 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
6 climsubmpt.c 
 |-  ( ph -> ( k e. Z |-> A ) ~~> C )
7 climsubmpt.d 
 |-  ( ph -> ( k e. Z |-> B ) ~~> D )
8 2 fvexi 
 |-  Z e. _V
9 8 mptex 
 |-  ( k e. Z |-> ( A - B ) ) e. _V
10 9 a1i 
 |-  ( ph -> ( k e. Z |-> ( A - B ) ) e. _V )
11 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
12 nfv 
 |-  F/ k j e. Z
13 1 12 nfan 
 |-  F/ k ( ph /\ j e. Z )
14 nfcv 
 |-  F/_ k j
15 14 nfcsb1 
 |-  F/_ k [_ j / k ]_ A
16 15 nfel1 
 |-  F/ k [_ j / k ]_ A e. CC
17 13 16 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC )
18 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
19 18 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
20 csbeq1a 
 |-  ( k = j -> A = [_ j / k ]_ A )
21 20 eleq1d 
 |-  ( k = j -> ( A e. CC <-> [_ j / k ]_ A e. CC ) )
22 19 21 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> A e. CC ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC ) ) )
23 17 22 4 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC )
24 eqid 
 |-  ( k e. Z |-> A ) = ( k e. Z |-> A )
25 14 15 20 24 fvmptf 
 |-  ( ( j e. Z /\ [_ j / k ]_ A e. CC ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
26 11 23 25 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
27 26 23 eqeltrd 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> A ) ` j ) e. CC )
28 14 nfcsb1 
 |-  F/_ k [_ j / k ]_ B
29 nfcv 
 |-  F/_ k CC
30 28 29 nfel 
 |-  F/ k [_ j / k ]_ B e. CC
31 13 30 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. CC )
32 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
33 32 eleq1d 
 |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
34 19 33 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> B e. CC ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. CC ) ) )
35 31 34 5 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ B e. CC )
36 eqid 
 |-  ( k e. Z |-> B ) = ( k e. Z |-> B )
37 14 28 32 36 fvmptf 
 |-  ( ( j e. Z /\ [_ j / k ]_ B e. CC ) -> ( ( k e. Z |-> B ) ` j ) = [_ j / k ]_ B )
38 11 35 37 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> B ) ` j ) = [_ j / k ]_ B )
39 38 35 eqeltrd 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> B ) ` j ) e. CC )
40 ovexd 
 |-  ( ( ph /\ j e. Z ) -> ( [_ j / k ]_ A - [_ j / k ]_ B ) e. _V )
41 nfcv 
 |-  F/_ k -
42 15 41 28 nfov 
 |-  F/_ k ( [_ j / k ]_ A - [_ j / k ]_ B )
43 20 32 oveq12d 
 |-  ( k = j -> ( A - B ) = ( [_ j / k ]_ A - [_ j / k ]_ B ) )
44 eqid 
 |-  ( k e. Z |-> ( A - B ) ) = ( k e. Z |-> ( A - B ) )
45 14 42 43 44 fvmptf 
 |-  ( ( j e. Z /\ ( [_ j / k ]_ A - [_ j / k ]_ B ) e. _V ) -> ( ( k e. Z |-> ( A - B ) ) ` j ) = ( [_ j / k ]_ A - [_ j / k ]_ B ) )
46 11 40 45 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> ( A - B ) ) ` j ) = ( [_ j / k ]_ A - [_ j / k ]_ B ) )
47 26 38 oveq12d 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( k e. Z |-> A ) ` j ) - ( ( k e. Z |-> B ) ` j ) ) = ( [_ j / k ]_ A - [_ j / k ]_ B ) )
48 46 47 eqtr4d 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> ( A - B ) ) ` j ) = ( ( ( k e. Z |-> A ) ` j ) - ( ( k e. Z |-> B ) ` j ) ) )
49 2 3 6 10 7 27 39 48 climsub 
 |-  ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( C - D ) )