prodf1

Description: The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017)

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

Step	Hyp	Ref	Expression
1		prodf1.1	$⊢ Z = ℤ_{\geq M}$
2		1t1e1	$⊢ 1 \cdot 1 = 1$
3	2	a1i	$⊢ N \in Z \to 1 \cdot 1 = 1$
4	1	eleq2i	$⊢ N \in Z \leftrightarrow N \in ℤ_{\geq M}$
5	4	biimpi	$⊢ N \in Z \to N \in ℤ_{\geq M}$
6		ax-1cn	$⊢ 1 \in ℂ$
7		elfzuz	$⊢ k \in (M \dots N) \to k \in ℤ_{\geq M}$
8	7 1	eleqtrrdi	$⊢ k \in (M \dots N) \to k \in Z$
9	8	adantl	$⊢ (N \in Z \land k \in (M \dots N)) \to k \in Z$
10		fvconst2g	$⊢ (1 \in ℂ \land k \in Z) \to (Z \times \{1\}) (k) = 1$
11	6 9 10	sylancr	$⊢ (N \in Z \land k \in (M \dots N)) \to (Z \times \{1\}) (k) = 1$
12	3 5 11	seqid3	$⊢ N \in Z \to seq M (\times (Z \times \{1\})) (N) = 1$

Metamath Proof Explorer