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

Metamath Proof Explorer

Theorem climaddc2

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

Ref Expression
Hypotheses climadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climaddc1.5 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
climaddc1.6 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
climaddc1.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
climaddc2.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 + ( 𝐹 ‘ 𝑘 ) ) )
Assertion climaddc2 ( 𝜑 → 𝐺 ⇝ ( 𝐶 + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4 climaddc1.5 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 climaddc1.6 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
6 climaddc1.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7 climaddc2.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 + ( 𝐹 ‘ 𝑘 ) ) )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℂ )
9 8 6 7 comraddd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + 𝐶 ) )
10 1 2 3 4 5 6 9 climaddc1 ⊢ ( 𝜑 → 𝐺 ⇝ ( 𝐴 + 𝐶 ) )
11 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
12 3 11 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13 12 4 addcomd ⊢ ( 𝜑 → ( 𝐴 + 𝐶 ) = ( 𝐶 + 𝐴 ) )
14 10 13 breqtrd ⊢ ( 𝜑 → 𝐺 ⇝ ( 𝐶 + 𝐴 ) )