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	⊢ Ⅎ 𝑘 𝜑
		fprodsubrecnncnv.2	⊢ ( 𝜑 → 𝑋 ∈ Fin )
		fprodsubrecnncnv.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
		fprodsubrecnncnv.4	⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( 𝐴 − ( 1 / 𝑛 ) ) )
	Assertion	fprodsubrecnncnv	⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝑋 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fprodsubrecnncnv.1	⊢ Ⅎ 𝑘 𝜑
2		fprodsubrecnncnv.2	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		fprodsubrecnncnv.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
4		fprodsubrecnncnv.4	⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( 𝐴 − ( 1 / 𝑛 ) ) )
5		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝑋 ( 𝐴 − 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝑋 ( 𝐴 − 𝑥 ) )
6		oveq2	⊢ ( 𝑚 = 𝑛 → ( 1 / 𝑚 ) = ( 1 / 𝑛 ) )
7	6	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ( 1 / 𝑚 ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
8	1 2 3 4 5 7	fprodsubrecnncnvlem	⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝑋 𝐴 )