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

Metamath Proof Explorer

Theorem climsubc2mpt

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

Ref Expression
Hypotheses climsubc2mpt.k ⊢ Ⅎ k φ
climsubc2mpt.z ⊢ Z = ℤ ≥ M
climsubc2mpt.m ⊢ φ → M ∈ ℤ
climsubc2mpt.a ⊢ φ ∧ k ∈ Z → A ∈ ℂ
climsubc2mpt.c ⊢ φ → k ∈ Z ⟼ A ⇝ C
climsubc2mpt.b ⊢ φ → B ∈ ℂ
Assertion climsubc2mpt ⊢ φ → k ∈ Z ⟼ A − B ⇝ C − B

Proof

Step Hyp Ref Expression
1 climsubc2mpt.k ⊢ Ⅎ k φ
2 climsubc2mpt.z ⊢ Z = ℤ ≥ M
3 climsubc2mpt.m ⊢ φ → M ∈ ℤ
4 climsubc2mpt.a ⊢ φ ∧ k ∈ Z → A ∈ ℂ
5 climsubc2mpt.c ⊢ φ → k ∈ Z ⟼ A ⇝ C
6 climsubc2mpt.b ⊢ φ → B ∈ ℂ
7 6 adantr ⊢ φ ∧ k ∈ Z → B ∈ ℂ
8 3 2 6 climconstmpt ⊢ φ → k ∈ Z ⟼ B ⇝ B
9 1 2 3 4 7 5 8 climsubmpt ⊢ φ → k ∈ Z ⟼ A − B ⇝ C − B