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

Metamath Proof Explorer

Theorem fprodaddrecnncnv

Description: The sequence S of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021)

		Ref	Expression
	Hypotheses	fprodaddrecnncnv.1	$⊢ Ⅎ k φ$
		fprodaddrecnncnv.2	$⊢ φ \to X \in Fin$
		fprodaddrecnncnv.3	$⊢ (φ \land k \in X) \to A \in ℂ$
		fprodaddrecnncnv.4	$⊢ S = (n \in ℕ ⟼ \prod_{k \in X} (A + (\frac{1}{n})))$
	Assertion	fprodaddrecnncnv	$⊢ φ \to S ⇝ \prod_{k \in X} A$

Proof

Step	Hyp	Ref	Expression
1		fprodaddrecnncnv.1	$⊢ Ⅎ k φ$
2		fprodaddrecnncnv.2	$⊢ φ \to X \in Fin$
3		fprodaddrecnncnv.3	$⊢ (φ \land k \in X) \to A \in ℂ$
4		fprodaddrecnncnv.4	$⊢ S = (n \in ℕ ⟼ \prod_{k \in X} (A + (\frac{1}{n})))$
5		eqid	$⊢ (x \in ℂ ⟼ \prod_{k \in X} (A + x)) = (x \in ℂ ⟼ \prod_{k \in X} (A + x))$
6		oveq2	$⊢ m = n \to \frac{1}{m} = \frac{1}{n}$
7	6	cbvmptv	$⊢ (m \in ℕ ⟼ \frac{1}{m}) = (n \in ℕ ⟼ \frac{1}{n})$
8	1 2 3 4 5 7	fprodaddrecnncnvlem	$⊢ φ \to S ⇝ \prod_{k \in X} A$