prodf1f

Description: A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017)

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

Step	Hyp	Ref	Expression
1		prodf1.1	$⊢ Z = ℤ_{\geq M}$
2	1	prodf1	$⊢ k \in Z \to seq M (\times (Z \times \{1\})) (k) = 1$
3		1ex	$⊢ 1 \in V$
4	3	fvconst2	$⊢ k \in Z \to (Z \times \{1\}) (k) = 1$
5	2 4	eqtr4d	$⊢ k \in Z \to seq M (\times (Z \times \{1\})) (k) = (Z \times \{1\}) (k)$
6	5	rgen	$⊢ \forall k \in Z seq M (\times (Z \times \{1\})) (k) = (Z \times \{1\}) (k)$
7		seqfn	$⊢ M \in ℤ \to seq M (\times (Z \times \{1\})) Fn ℤ_{\geq M}$
8	1	fneq2i	$⊢ seq M (\times (Z \times \{1\})) Fn Z \leftrightarrow seq M (\times (Z \times \{1\})) Fn ℤ_{\geq M}$
9	7 8	sylibr	$⊢ M \in ℤ \to seq M (\times (Z \times \{1\})) Fn Z$
10	3	fconst	$⊢ (Z \times \{1\}) : Z ⟶ \{1\}$
11		ffn	$⊢ (Z \times \{1\}) : Z ⟶ \{1\} \to (Z \times \{1\}) Fn Z$
12	10 11	ax-mp	$⊢ (Z \times \{1\}) Fn Z$
13		eqfnfv	$⊢ (seq M (\times (Z \times \{1\})) Fn Z \land (Z \times \{1\}) Fn Z) \to (seq M (\times (Z \times \{1\})) = Z \times \{1\} \leftrightarrow \forall k \in Z seq M (\times (Z \times \{1\})) (k) = (Z \times \{1\}) (k))$
14	9 12 13	sylancl	$⊢ M \in ℤ \to (seq M (\times (Z \times \{1\})) = Z \times \{1\} \leftrightarrow \forall k \in Z seq M (\times (Z \times \{1\})) (k) = (Z \times \{1\}) (k))$
15	6 14	mpbiri	$⊢ M \in ℤ \to seq M (\times (Z \times \{1\})) = Z \times \{1\}$

Metamath Proof Explorer