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	⊢ ( 𝜑 → 𝐺 ⇝ ( 𝐶 + 𝐴 ) )