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

Metamath Proof Explorer

Theorem climsubc1mpt

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

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

Proof

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