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	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ⇝ ( 𝐶 − 𝐷 ) )