This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimsub

Description: Limit of the difference of two converging functions. Proposition 12-2.1(b) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses rlimadd.3 ⊢ φ ∧ x ∈ A → B ∈ V
rlimadd.4 ⊢ φ ∧ x ∈ A → C ∈ V
rlimadd.5 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
rlimadd.6 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
Assertion rlimsub ⊢ φ → x ∈ A ⟼ B − C ⇝ℝ D − E

Proof

Step Hyp Ref Expression
1 rlimadd.3 ⊢ φ ∧ x ∈ A → B ∈ V
2 rlimadd.4 ⊢ φ ∧ x ∈ A → C ∈ V
3 rlimadd.5 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
4 rlimadd.6 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
5 1 3 rlimmptrcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
6 2 4 rlimmptrcl ⊢ φ ∧ x ∈ A → C ∈ ℂ
7 rlimcl ⊢ x ∈ A ⟼ B ⇝ℝ D → D ∈ ℂ
8 3 7 syl ⊢ φ → D ∈ ℂ
9 rlimcl ⊢ x ∈ A ⟼ C ⇝ℝ E → E ∈ ℂ
10 4 9 syl ⊢ φ → E ∈ ℂ
11 subf ⊢ − : ℂ × ℂ ⟶ ℂ
12 11 a1i ⊢ φ → − : ℂ × ℂ ⟶ ℂ
13 simpr ⊢ φ ∧ y ∈ ℝ + → y ∈ ℝ +
14 8 adantr ⊢ φ ∧ y ∈ ℝ + → D ∈ ℂ
15 10 adantr ⊢ φ ∧ y ∈ ℝ + → E ∈ ℂ
16 subcn2 ⊢ y ∈ ℝ + ∧ D ∈ ℂ ∧ E ∈ ℂ → ∃ z ∈ ℝ + ∃ w ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − D < z ∧ v − E < w → u - v - D − E < y
17 13 14 15 16 syl3anc ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ ℝ + ∃ w ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − D < z ∧ v − E < w → u - v - D − E < y
18 5 6 8 10 3 4 12 17 rlimcn2 ⊢ φ → x ∈ A ⟼ B − C ⇝ℝ D − E