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

Proof

Step Hyp Ref Expression
1 fprodsubrecnncnv.1 k φ
2 fprodsubrecnncnv.2 φ X Fin
3 fprodsubrecnncnv.3 φ k X A
4 fprodsubrecnncnv.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 fprodsubrecnncnvlem φ S k X A