Theorem climmulc2

Description: Limit of a sequence multiplied by a constant C . Corollary 12-2.2 of Gleason p. 171. (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	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	climmulc2.h	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
Assertion	climmulc2	⊢ ( 𝜑 → 𝐺 ⇝ ( 𝐶 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climadd.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climadd.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climadd.4	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4		climaddc1.5	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5		climaddc1.6	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
6		climaddc1.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7		climmulc2.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	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
20	7 19	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) )
21	1 2 12 5 3 18 6 20	climmul	⊢ ( 𝜑 → 𝐺 ⇝ ( 𝐶 · 𝐴 ) )