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