This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prodfclim1

Description: The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017)

		Ref	Expression
	Hypothesis	prodf1.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	prodfclim1	$⊢ M \in ℤ \to seq M (\times (Z \times \{1\})) ⇝ 1$

Step	Hyp	Ref	Expression
1		prodf1.1	$⊢ Z = ℤ_{\geq M}$
2	1	prodf1f	$⊢ M \in ℤ \to seq M (\times (Z \times \{1\})) = Z \times \{1\}$
3		ax-1cn	$⊢ 1 \in ℂ$
4	1	eqimss2i	$⊢ ℤ_{\geq M} \subseteq Z$
5	1	fvexi	$⊢ Z \in V$
6	4 5	climconst2	$⊢ (1 \in ℂ \land M \in ℤ) \to (Z \times \{1\}) ⇝ 1$
7	3 6	mpan	$⊢ M \in ℤ \to (Z \times \{1\}) ⇝ 1$
8	2 7	eqbrtrd	$⊢ M \in ℤ \to seq M (\times (Z \times \{1\})) ⇝ 1$