Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Continuous Functions
fprodsubrecnncnv
Metamath Proof Explorer
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
⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝑋 𝐴 )