climmul

Description: Limit of the product of two converging sequences. Proposition 12-2.1(c) of Gleason p. 168. (Contributed by NM, 27-Dec-2005) (Proof shortened by Mario Carneiro, 1-Feb-2014)

	Ref	Expression
Hypotheses	climadd.1	$⊢ Z = ℤ_{\geq M}$
	climadd.2	$⊢ φ \to M \in ℤ$
	climadd.4	$⊢ φ \to F ⇝ A$
	climadd.6	$⊢ φ \to H \in X$
	climadd.7	$⊢ φ \to G ⇝ B$
	climadd.8	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	climadd.9	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
	climmul.h	$⊢ (φ \land k \in Z) \to H (k) = F (k) G (k)$
Assertion	climmul	$⊢ φ \to H ⇝ A B$

Proof

Step	Hyp	Ref	Expression
1		climadd.1	$⊢ Z = ℤ_{\geq M}$
2		climadd.2	$⊢ φ \to M \in ℤ$
3		climadd.4	$⊢ φ \to F ⇝ A$
4		climadd.6	$⊢ φ \to H \in X$
5		climadd.7	$⊢ φ \to G ⇝ B$
6		climadd.8	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
7		climadd.9	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
8		climmul.h	$⊢ (φ \land k \in Z) \to H (k) = F (k) G (k)$
9		climcl	$⊢ F ⇝ A \to A \in ℂ$
10	3 9	syl	$⊢ φ \to A \in ℂ$
11		climcl	$⊢ G ⇝ B \to B \in ℂ$
12	5 11	syl	$⊢ φ \to B \in ℂ$
13		mulcl	$⊢ (u \in ℂ \land v \in ℂ) \to u v \in ℂ$
14	13	adantl	$⊢ (φ \land (u \in ℂ \land v \in ℂ)) \to u v \in ℂ$
15		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
16	10	adantr	$⊢ (φ \land x \in ℝ^{+}) \to A \in ℂ$
17	12	adantr	$⊢ (φ \land x \in ℝ^{+}) \to B \in ℂ$
18		mulcn2	$⊢ (x \in ℝ^{+} \land A \in ℂ \land B \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - A\| < y \land \|v - B\| < z) \to \|u v - A B\| < x)$
19	15 16 17 18	syl3anc	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - A\| < y \land \|v - B\| < z) \to \|u v - A B\| < x)$
20	1 2 10 12 14 3 5 4 19 6 7 8	climcn2	$⊢ φ \to H ⇝ A B$

Metamath Proof Explorer

Theorem climmul

Proof