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	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climadd.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climadd.4	$$⊢\phi \to F⇝A$$
	climaddc1.5	$$⊢\phi \to C\in ℂ$$
	climaddc1.6	$$⊢\phi \to G\in W$$
	climaddc1.7	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	climaddc2.h	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=C+F\left(k\right)$$
Assertion	climaddc2	$$⊢\phi \to G⇝\left(C+A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climadd.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climadd.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climadd.4	$$⊢\phi \to F⇝A$$
4		climaddc1.5	$$⊢\phi \to C\in ℂ$$
5		climaddc1.6	$$⊢\phi \to G\in W$$
6		climaddc1.7	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
7		climaddc2.h	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=C+F\left(k\right)$$
8	4	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to C\in ℂ$$
9	8 6 7	comraddd	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=F\left(k\right)+C$$
10	1 2 3 4 5 6 9	climaddc1	$$⊢\phi \to G⇝\left(A+C\right)$$
11		climcl	$$⊢F⇝A\to A\in ℂ$$
12	3 11	syl	$$⊢\phi \to A\in ℂ$$
13	12 4	addcomd	$$⊢\phi \to A+C=C+A$$
14	10 13	breqtrd	$$⊢\phi \to G⇝\left(C+A\right)$$