Metamath Proof Explorer

Theorem sublimc

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

Ref Expression
Hypotheses sublimc.f ⊢ F = x ∈ A ⟼ B
sublimc.2 ⊢ G = x ∈ A ⟼ C
sublimc.3 ⊢ H = x ∈ A ⟼ B − C
sublimc.4 ⊢ φ ∧ x ∈ A → B ∈ ℂ
sublimc.5 ⊢ φ ∧ x ∈ A → C ∈ ℂ
sublimc.6 ⊢ φ → E ∈ F lim ℂ D
sublimc.7 ⊢ φ → I ∈ G lim ℂ D
Assertion sublimc ⊢ φ → E − I ∈ H lim ℂ D

Proof

Step Hyp Ref Expression
1 sublimc.f ⊢ F = x ∈ A ⟼ B
2 sublimc.2 ⊢ G = x ∈ A ⟼ C
3 sublimc.3 ⊢ H = x ∈ A ⟼ B − C
4 sublimc.4 ⊢ φ ∧ x ∈ A → B ∈ ℂ
5 sublimc.5 ⊢ φ ∧ x ∈ A → C ∈ ℂ
6 sublimc.6 ⊢ φ → E ∈ F lim ℂ D
7 sublimc.7 ⊢ φ → I ∈ G lim ℂ D
8 eqid ⊢ x ∈ A ⟼ − C = x ∈ A ⟼ − C
9 eqid ⊢ x ∈ A ⟼ B + − C = x ∈ A ⟼ B + − C
10 5 negcld ⊢ φ ∧ x ∈ A → − C ∈ ℂ
11 2 8 5 7 neglimc ⊢ φ → − I ∈ x ∈ A ⟼ − C lim ℂ D
12 1 8 9 4 10 6 11 addlimc ⊢ φ → E + -I ∈ x ∈ A ⟼ B + − C lim ℂ D
13 limccl ⊢ F lim ℂ D ⊆ ℂ
14 13 6 sselid ⊢ φ → E ∈ ℂ
15 limccl ⊢ G lim ℂ D ⊆ ℂ
16 15 7 sselid ⊢ φ → I ∈ ℂ
17 14 16 negsubd ⊢ φ → E + -I = E − I
18 17 eqcomd ⊢ φ → E − I = E + -I
19 4 5 negsubd ⊢ φ ∧ x ∈ A → B + − C = B − C
20 19 eqcomd ⊢ φ ∧ x ∈ A → B − C = B + − C
21 20 mpteq2dva ⊢ φ → x ∈ A ⟼ B − C = x ∈ A ⟼ B + − C
22 3 21 syl5eq ⊢ φ → H = x ∈ A ⟼ B + − C
23 22 oveq1d ⊢ φ → H lim ℂ D = x ∈ A ⟼ B + − C lim ℂ D
24 12 18 23 3eltr4d ⊢ φ → E − I ∈ H lim ℂ D