sublimc

Description: Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Step	Hyp	Ref	Expression
1		sublimc.f	$⊢ F = (x \in A ⟼ B)$
2		sublimc.2	$⊢ G = (x \in A ⟼ C)$
3		sublimc.3	$⊢ H = (x \in A ⟼ B - C)$
4		sublimc.4	$⊢ (φ \land x \in A) \to B \in ℂ$
5		sublimc.5	$⊢ (φ \land x \in A) \to C \in ℂ$
6		sublimc.6	$⊢ φ \to E \in (F {lim}_{ℂ} D)$
7		sublimc.7	$⊢ φ \to I \in (G {lim}_{ℂ} D)$
8		eqid	$⊢ (x \in A ⟼ - C) = (x \in A ⟼ - C)$
9		eqid	$⊢ (x \in A ⟼ B + (- C)) = (x \in A ⟼ B + (- C))$
10	5	negcld	$⊢ (φ \land x \in A) \to - C \in ℂ$
11	2 8 5 7	neglimc	$⊢ φ \to - I \in ((x \in A ⟼ - C) {lim}_{ℂ} D)$
12	1 8 9 4 10 6 11	addlimc	$⊢ φ \to E + -I \in ((x \in A ⟼ B + (- C)) {lim}_{ℂ} D)$
13		limccl	$⊢ F {lim}_{ℂ} D \subseteq ℂ$
14	13 6	sselid	$⊢ φ \to E \in ℂ$
15		limccl	$⊢ G {lim}_{ℂ} D \subseteq ℂ$
16	15 7	sselid	$⊢ φ \to I \in ℂ$
17	14 16	negsubd	$⊢ φ \to E + -I = E - I$
18	17	eqcomd	$⊢ φ \to E - I = E + -I$
19	4 5	negsubd	$⊢ (φ \land x \in A) \to B + (- C) = B - C$
20	19	eqcomd	$⊢ (φ \land x \in A) \to B - C = B + (- C)$
21	20	mpteq2dva	$⊢ φ \to (x \in A ⟼ B - C) = (x \in A ⟼ B + (- C))$
22	3 21	eqtrid	$⊢ φ \to H = (x \in A ⟼ B + (- C))$
23	22	oveq1d	$⊢ φ \to H {lim}_{ℂ} D = (x \in A ⟼ B + (- C)) {lim}_{ℂ} D$
24	12 18 23	3eltr4d	$⊢ φ \to E - I \in (H {lim}_{ℂ} D)$

Metamath Proof Explorer