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 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
rlimadd.4 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑉 )
rlimadd.5 ( 𝜑 → ( 𝑥𝐴𝐵 ) ⇝𝑟 𝐷 )
rlimadd.6 ( 𝜑 → ( 𝑥𝐴𝐶 ) ⇝𝑟 𝐸 )
Assertion rlimsub ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ⇝𝑟 ( 𝐷𝐸 ) )

Proof

Step Hyp Ref Expression
1 rlimadd.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 rlimadd.4 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑉 )
3 rlimadd.5 ( 𝜑 → ( 𝑥𝐴𝐵 ) ⇝𝑟 𝐷 )
4 rlimadd.6 ( 𝜑 → ( 𝑥𝐴𝐶 ) ⇝𝑟 𝐸 )
5 1 3 rlimmptrcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
6 2 4 rlimmptrcl ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
7 rlimcl ( ( 𝑥𝐴𝐵 ) ⇝𝑟 𝐷𝐷 ∈ ℂ )
8 3 7 syl ( 𝜑𝐷 ∈ ℂ )
9 rlimcl ( ( 𝑥𝐴𝐶 ) ⇝𝑟 𝐸𝐸 ∈ ℂ )
10 4 9 syl ( 𝜑𝐸 ∈ ℂ )
11 subf − : ( ℂ × ℂ ) ⟶ ℂ
12 11 a1i ( 𝜑 → − : ( ℂ × ℂ ) ⟶ ℂ )
13 simpr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
14 8 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
15 10 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐸 ∈ ℂ )
16 subcn2 ( ( 𝑦 ∈ ℝ+𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ℝ+𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢𝐷 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢𝑣 ) − ( 𝐷𝐸 ) ) ) < 𝑦 ) )
17 13 14 15 16 syl3anc ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ℝ+𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢𝐷 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢𝑣 ) − ( 𝐷𝐸 ) ) ) < 𝑦 ) )
18 5 6 8 10 3 4 12 17 rlimcn2 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ⇝𝑟 ( 𝐷𝐸 ) )