climsubmpt

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

	Ref	Expression
Hypotheses	climsubmpt.k	$⊢ Ⅎ k φ$
	climsubmpt.z	$⊢ Z = ℤ_{\geq M}$
	climsubmpt.m	$⊢ φ \to M \in ℤ$
	climsubmpt.a	$⊢ (φ \land k \in Z) \to A \in ℂ$
	climsubmpt.b	$⊢ (φ \land k \in Z) \to B \in ℂ$
	climsubmpt.c	$⊢ φ \to (k \in Z ⟼ A) ⇝ C$
	climsubmpt.d	$⊢ φ \to (k \in Z ⟼ B) ⇝ D$
Assertion	climsubmpt	$⊢ φ \to (k \in Z ⟼ A - B) ⇝ (C - D)$

Proof

Step	Hyp	Ref	Expression
1		climsubmpt.k	$⊢ Ⅎ k φ$
2		climsubmpt.z	$⊢ Z = ℤ_{\geq M}$
3		climsubmpt.m	$⊢ φ \to M \in ℤ$
4		climsubmpt.a	$⊢ (φ \land k \in Z) \to A \in ℂ$
5		climsubmpt.b	$⊢ (φ \land k \in Z) \to B \in ℂ$
6		climsubmpt.c	$⊢ φ \to (k \in Z ⟼ A) ⇝ C$
7		climsubmpt.d	$⊢ φ \to (k \in Z ⟼ B) ⇝ D$
8	2	fvexi	$⊢ Z \in V$
9	8	mptex	$⊢ (k \in Z ⟼ A - B) \in V$
10	9	a1i	$⊢ φ \to (k \in Z ⟼ A - B) \in V$
11		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
12		nfv	$⊢ Ⅎ k j \in Z$
13	1 12	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
14		nfcv	$⊢ \underline{Ⅎ} k j$
15	14	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ A$
16	15	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ A \in ℂ$
17	13 16	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ A \in ℂ)$
18		eleq1w	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
19	18	anbi2d	$⊢ k = j \to ((φ \land k \in Z) \leftrightarrow (φ \land j \in Z))$
20		csbeq1a	$⊢ k = j \to A = ⦋ j / k ⦌ A$
21	20	eleq1d	$⊢ k = j \to (A \in ℂ \leftrightarrow ⦋ j / k ⦌ A \in ℂ)$
22	19 21	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to A \in ℂ) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ A \in ℂ))$
23	17 22 4	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ A \in ℂ$
24		eqid	$⊢ (k \in Z ⟼ A) = (k \in Z ⟼ A)$
25	14 15 20 24	fvmptf	$⊢ (j \in Z \land ⦋ j / k ⦌ A \in ℂ) \to (k \in Z ⟼ A) (j) = ⦋ j / k ⦌ A$
26	11 23 25	syl2anc	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A) (j) = ⦋ j / k ⦌ A$
27	26 23	eqeltrd	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A) (j) \in ℂ$
28	14	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
29		nfcv	$⊢ \underline{Ⅎ} k ℂ$
30	28 29	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℂ$
31	13 30	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ B \in ℂ)$
32		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
33	32	eleq1d	$⊢ k = j \to (B \in ℂ \leftrightarrow ⦋ j / k ⦌ B \in ℂ)$
34	19 33	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to B \in ℂ) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ B \in ℂ))$
35	31 34 5	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ B \in ℂ$
36		eqid	$⊢ (k \in Z ⟼ B) = (k \in Z ⟼ B)$
37	14 28 32 36	fvmptf	$⊢ (j \in Z \land ⦋ j / k ⦌ B \in ℂ) \to (k \in Z ⟼ B) (j) = ⦋ j / k ⦌ B$
38	11 35 37	syl2anc	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ B) (j) = ⦋ j / k ⦌ B$
39	38 35	eqeltrd	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ B) (j) \in ℂ$
40		ovexd	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ A - ⦋ j / k ⦌ B \in V$
41		nfcv	$⊢ \underline{Ⅎ} k -$
42	15 41 28	nfov	$⊢ \underline{Ⅎ} k (⦋ j / k ⦌ A - ⦋ j / k ⦌ B)$
43	20 32	oveq12d	$⊢ k = j \to A - B = ⦋ j / k ⦌ A - ⦋ j / k ⦌ B$
44		eqid	$⊢ (k \in Z ⟼ A - B) = (k \in Z ⟼ A - B)$
45	14 42 43 44	fvmptf	$⊢ (j \in Z \land ⦋ j / k ⦌ A - ⦋ j / k ⦌ B \in V) \to (k \in Z ⟼ A - B) (j) = ⦋ j / k ⦌ A - ⦋ j / k ⦌ B$
46	11 40 45	syl2anc	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A - B) (j) = ⦋ j / k ⦌ A - ⦋ j / k ⦌ B$
47	26 38	oveq12d	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A) (j) - (k \in Z ⟼ B) (j) = ⦋ j / k ⦌ A - ⦋ j / k ⦌ B$
48	46 47	eqtr4d	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A - B) (j) = (k \in Z ⟼ A) (j) - (k \in Z ⟼ B) (j)$
49	2 3 6 10 7 27 39 48	climsub	$⊢ φ \to (k \in Z ⟼ A - B) ⇝ (C - D)$

Metamath Proof Explorer

Theorem climsubmpt

Proof