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 𝑘 𝜑
climsubmpt.z 𝑍 = ( ℤ𝑀 )
climsubmpt.m ( 𝜑𝑀 ∈ ℤ )
climsubmpt.a ( ( 𝜑𝑘𝑍 ) → 𝐴 ∈ ℂ )
climsubmpt.b ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℂ )
climsubmpt.c ( 𝜑 → ( 𝑘𝑍𝐴 ) ⇝ 𝐶 )
climsubmpt.d ( 𝜑 → ( 𝑘𝑍𝐵 ) ⇝ 𝐷 )
Assertion climsubmpt ( 𝜑 → ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ⇝ ( 𝐶𝐷 ) )

Proof

Step Hyp Ref Expression
1 climsubmpt.k 𝑘 𝜑
2 climsubmpt.z 𝑍 = ( ℤ𝑀 )
3 climsubmpt.m ( 𝜑𝑀 ∈ ℤ )
4 climsubmpt.a ( ( 𝜑𝑘𝑍 ) → 𝐴 ∈ ℂ )
5 climsubmpt.b ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℂ )
6 climsubmpt.c ( 𝜑 → ( 𝑘𝑍𝐴 ) ⇝ 𝐶 )
7 climsubmpt.d ( 𝜑 → ( 𝑘𝑍𝐵 ) ⇝ 𝐷 )
8 2 fvexi 𝑍 ∈ V
9 8 mptex ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ∈ V
10 9 a1i ( 𝜑 → ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ∈ V )
11 simpr ( ( 𝜑𝑗𝑍 ) → 𝑗𝑍 )
12 nfv 𝑘 𝑗𝑍
13 1 12 nfan 𝑘 ( 𝜑𝑗𝑍 )
14 nfcv 𝑘 𝑗
15 14 nfcsb1 𝑘 𝑗 / 𝑘 𝐴
16 15 nfel1 𝑘 𝑗 / 𝑘 𝐴 ∈ ℂ
17 13 16 nfim 𝑘 ( ( 𝜑𝑗𝑍 ) → 𝑗 / 𝑘 𝐴 ∈ ℂ )
18 eleq1w ( 𝑘 = 𝑗 → ( 𝑘𝑍𝑗𝑍 ) )
19 18 anbi2d ( 𝑘 = 𝑗 → ( ( 𝜑𝑘𝑍 ) ↔ ( 𝜑𝑗𝑍 ) ) )
20 csbeq1a ( 𝑘 = 𝑗𝐴 = 𝑗 / 𝑘 𝐴 )
21 20 eleq1d ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ 𝑗 / 𝑘 𝐴 ∈ ℂ ) )
22 19 21 imbi12d ( 𝑘 = 𝑗 → ( ( ( 𝜑𝑘𝑍 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑𝑗𝑍 ) → 𝑗 / 𝑘 𝐴 ∈ ℂ ) ) )
23 17 22 4 chvarfv ( ( 𝜑𝑗𝑍 ) → 𝑗 / 𝑘 𝐴 ∈ ℂ )
24 eqid ( 𝑘𝑍𝐴 ) = ( 𝑘𝑍𝐴 )
25 14 15 20 24 fvmptf ( ( 𝑗𝑍 𝑗 / 𝑘 𝐴 ∈ ℂ ) → ( ( 𝑘𝑍𝐴 ) ‘ 𝑗 ) = 𝑗 / 𝑘 𝐴 )
26 11 23 25 syl2anc ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍𝐴 ) ‘ 𝑗 ) = 𝑗 / 𝑘 𝐴 )
27 26 23 eqeltrd ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍𝐴 ) ‘ 𝑗 ) ∈ ℂ )
28 14 nfcsb1 𝑘 𝑗 / 𝑘 𝐵
29 nfcv 𝑘
30 28 29 nfel 𝑘 𝑗 / 𝑘 𝐵 ∈ ℂ
31 13 30 nfim 𝑘 ( ( 𝜑𝑗𝑍 ) → 𝑗 / 𝑘 𝐵 ∈ ℂ )
32 csbeq1a ( 𝑘 = 𝑗𝐵 = 𝑗 / 𝑘 𝐵 )
33 32 eleq1d ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ 𝑗 / 𝑘 𝐵 ∈ ℂ ) )
34 19 33 imbi12d ( 𝑘 = 𝑗 → ( ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑𝑗𝑍 ) → 𝑗 / 𝑘 𝐵 ∈ ℂ ) ) )
35 31 34 5 chvarfv ( ( 𝜑𝑗𝑍 ) → 𝑗 / 𝑘 𝐵 ∈ ℂ )
36 eqid ( 𝑘𝑍𝐵 ) = ( 𝑘𝑍𝐵 )
37 14 28 32 36 fvmptf ( ( 𝑗𝑍 𝑗 / 𝑘 𝐵 ∈ ℂ ) → ( ( 𝑘𝑍𝐵 ) ‘ 𝑗 ) = 𝑗 / 𝑘 𝐵 )
38 11 35 37 syl2anc ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍𝐵 ) ‘ 𝑗 ) = 𝑗 / 𝑘 𝐵 )
39 38 35 eqeltrd ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍𝐵 ) ‘ 𝑗 ) ∈ ℂ )
40 ovexd ( ( 𝜑𝑗𝑍 ) → ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 ) ∈ V )
41 nfcv 𝑘
42 15 41 28 nfov 𝑘 ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 )
43 20 32 oveq12d ( 𝑘 = 𝑗 → ( 𝐴𝐵 ) = ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 ) )
44 eqid ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) = ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) )
45 14 42 43 44 fvmptf ( ( 𝑗𝑍 ∧ ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 ) ∈ V ) → ( ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ‘ 𝑗 ) = ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 ) )
46 11 40 45 syl2anc ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ‘ 𝑗 ) = ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 ) )
47 26 38 oveq12d ( ( 𝜑𝑗𝑍 ) → ( ( ( 𝑘𝑍𝐴 ) ‘ 𝑗 ) − ( ( 𝑘𝑍𝐵 ) ‘ 𝑗 ) ) = ( 𝑗 / 𝑘 𝐴 𝑗 / 𝑘 𝐵 ) )
48 46 47 eqtr4d ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ‘ 𝑗 ) = ( ( ( 𝑘𝑍𝐴 ) ‘ 𝑗 ) − ( ( 𝑘𝑍𝐵 ) ‘ 𝑗 ) ) )
49 2 3 6 10 7 27 39 48 climsub ( 𝜑 → ( 𝑘𝑍 ↦ ( 𝐴𝐵 ) ) ⇝ ( 𝐶𝐷 ) )