Metamath Proof Explorer

Theorem climsubc2

Description: Limit of a constant C minus each term of a sequence. (Contributed by NM, 24-Sep-2005) (Revised by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses climadd.1 ⊢ Z = ℤ ≥ M
climadd.2 ⊢ φ → M ∈ ℤ
climadd.4 ⊢ φ → F ⇝ A
climaddc1.5 ⊢ φ → C ∈ ℂ
climaddc1.6 ⊢ φ → G ∈ W
climaddc1.7 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
climsubc2.h ⊢ φ ∧ k ∈ Z → G ⁡ k = C − F ⁡ k
Assertion climsubc2 ⊢ φ → G ⇝ C − A

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ Z = ℤ ≥ M
2 climadd.2 ⊢ φ → M ∈ ℤ
3 climadd.4 ⊢ φ → F ⇝ A
4 climaddc1.5 ⊢ φ → C ∈ ℂ
5 climaddc1.6 ⊢ φ → G ∈ W
6 climaddc1.7 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
7 climsubc2.h ⊢ φ ∧ k ∈ Z → G ⁡ k = C − F ⁡ k
8 0z ⊢ 0 ∈ ℤ
9 uzssz ⊢ ℤ ≥ 0 ⊆ ℤ
10 zex ⊢ ℤ ∈ V
11 9 10 climconst2 ⊢ C ∈ ℂ ∧ 0 ∈ ℤ → ℤ × C ⇝ C
12 4 8 11 sylancl ⊢ φ → ℤ × C ⇝ C
13 eluzelz ⊢ k ∈ ℤ ≥ M → k ∈ ℤ
14 13 1 eleq2s ⊢ k ∈ Z → k ∈ ℤ
15 fvconst2g ⊢ C ∈ ℂ ∧ k ∈ ℤ → ℤ × C ⁡ k = C
16 4 14 15 syl2an ⊢ φ ∧ k ∈ Z → ℤ × C ⁡ k = C
17 4 adantr ⊢ φ ∧ k ∈ Z → C ∈ ℂ
18 16 17 eqeltrd ⊢ φ ∧ k ∈ Z → ℤ × C ⁡ k ∈ ℂ
19 16 oveq1d ⊢ φ ∧ k ∈ Z → ℤ × C ⁡ k − F ⁡ k = C − F ⁡ k
20 7 19 eqtr4d ⊢ φ ∧ k ∈ Z → G ⁡ k = ℤ × C ⁡ k − F ⁡ k
21 1 2 12 5 3 18 6 20 climsub ⊢ φ → G ⇝ C − A