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	$⊢ Z = ℤ_{\geq M}$
	climadd.2	$⊢ φ \to M \in ℤ$
	climadd.4	$⊢ φ \to F ⇝ A$
	climaddc1.5	$⊢ φ \to C \in ℂ$
	climaddc1.6	$⊢ φ \to G \in W$
	climaddc1.7	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	climmulc2.h	$⊢ (φ \land k \in Z) \to G (k) = C F (k)$
Assertion	climmulc2	$⊢ φ \to G ⇝ C A$

Proof

Step	Hyp	Ref	Expression
1		climadd.1	$⊢ Z = ℤ_{\geq M}$
2		climadd.2	$⊢ φ \to M \in ℤ$
3		climadd.4	$⊢ φ \to F ⇝ A$
4		climaddc1.5	$⊢ φ \to C \in ℂ$
5		climaddc1.6	$⊢ φ \to G \in W$
6		climaddc1.7	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
7		climmulc2.h	$⊢ (φ \land k \in Z) \to G (k) = C F (k)$
8		0z	$⊢ 0 \in ℤ$
9		uzssz	$⊢ ℤ_{\geq 0} \subseteq ℤ$
10		zex	$⊢ ℤ \in V$
11	9 10	climconst2	$⊢ (C \in ℂ \land 0 \in ℤ) \to (ℤ \times \{C\}) ⇝ C$
12	4 8 11	sylancl	$⊢ φ \to (ℤ \times \{C\}) ⇝ C$
13		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
14	13 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
15		fvconst2g	$⊢ (C \in ℂ \land k \in ℤ) \to (ℤ \times \{C\}) (k) = C$
16	4 14 15	syl2an	$⊢ (φ \land k \in Z) \to (ℤ \times \{C\}) (k) = C$
17	4	adantr	$⊢ (φ \land k \in Z) \to C \in ℂ$
18	16 17	eqeltrd	$⊢ (φ \land k \in Z) \to (ℤ \times \{C\}) (k) \in ℂ$
19	16	oveq1d	$⊢ (φ \land k \in Z) \to (ℤ \times \{C\}) (k) F (k) = C F (k)$
20	7 19	eqtr4d	$⊢ (φ \land k \in Z) \to G (k) = (ℤ \times \{C\}) (k) F (k)$
21	1 2 12 5 3 18 6 20	climmul	$⊢ φ \to G ⇝ C A$

Metamath Proof Explorer

Theorem climmulc2

Proof