Metamath Proof Explorer

Theorem climsubc1

Description: Limit of a constant C subtracted from each term of a sequence. (Contributed 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 ∈ ℂ
climsubc1.h ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k − C
Assertion climsubc1 ⊢ φ → G ⇝ A − C

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 climsubc1.h ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k − C
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 oveq2d ⊢ φ ∧ k ∈ Z → F ⁡ k − ℤ × C ⁡ k = F ⁡ k − C
20 7 19 eqtr4d ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k − ℤ × C ⁡ k
21 1 2 3 5 12 6 18 20 climsub ⊢ φ → G ⇝ A − C