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

Metamath Proof Explorer

Theorem fprodsubrecnncnv

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

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

Proof

Step	Hyp	Ref	Expression
1		fprodsubrecnncnv.1	$⊢ Ⅎ k φ$
2		fprodsubrecnncnv.2	$⊢ φ \to X \in Fin$
3		fprodsubrecnncnv.3	$⊢ (φ \land k \in X) \to A \in ℂ$
4		fprodsubrecnncnv.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	fprodsubrecnncnvlem	$⊢ φ \to S ⇝ \prod_{k \in X} A$