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