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 φ X Fin
fprodaddrecnncnv.3 φ k X A
fprodaddrecnncnv.4 S = n k X A + 1 n
Assertion fprodaddrecnncnv φ S k X A

Proof

Step Hyp Ref Expression
1 fprodaddrecnncnv.1 k φ
2 fprodaddrecnncnv.2 φ X Fin
3 fprodaddrecnncnv.3 φ k X A
4 fprodaddrecnncnv.4 S = n k X A + 1 n
5 eqid x k X A + x = x k X A + x
6 oveq2 m = n 1 m = 1 n
7 6 cbvmptv m 1 m = n 1 n
8 1 2 3 4 5 7 fprodaddrecnncnvlem φ S k X A