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