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

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climaddc1.5 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
climaddc1.6 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
climaddc1.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
climsubc1.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − 𝐶 ) )
Assertion climsubc1 ( 𝜑 → 𝐺 ⇝ ( 𝐴 − 𝐶 ) )

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4 climaddc1.5 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 climaddc1.6 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
6 climaddc1.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7 climsubc1.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − 𝐶 ) )
8 0z ⊢ 0 ∈ ℤ
9 uzssz ⊢ ( ℤ≥ ‘ 0 ) ⊆ ℤ
10 zex ⊢ ℤ ∈ V
11 9 10 climconst2 ⊢ ( ( 𝐶 ∈ ℂ ∧ 0 ∈ ℤ ) → ( ℤ × { 𝐶 } ) ⇝ 𝐶 )
12 4 8 11 sylancl ⊢ ( 𝜑 → ( ℤ × { 𝐶 } ) ⇝ 𝐶 )
13 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
14 13 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
15 fvconst2g ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑘 ∈ ℤ ) → ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) = 𝐶 )
16 4 14 15 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) = 𝐶 )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℂ )
18 16 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) ∈ ℂ )
19 16 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) − ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) − 𝐶 ) )
20 7 19 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) ) )
21 1 2 3 5 12 6 18 20 climsub ⊢ ( 𝜑 → 𝐺 ⇝ ( 𝐴 − 𝐶 ) )