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

Proof

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