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	|- F/ k ph
	fprodsubrecnncnv.2	|- ( ph -> X e. Fin )
	fprodsubrecnncnv.3	|- ( ( ph /\ k e. X ) -> A e. CC )
	fprodsubrecnncnv.4	|- S = ( n e. NN |-> prod_ k e. X ( A - ( 1 / n ) ) )
Assertion	fprodsubrecnncnv	|- ( ph -> S ~~> prod_ k e. X A )

Proof

Step	Hyp	Ref	Expression
1		fprodsubrecnncnv.1	|- F/ k ph
2		fprodsubrecnncnv.2	|- ( ph -> X e. Fin )
3		fprodsubrecnncnv.3	|- ( ( ph /\ k e. X ) -> A e. CC )
4		fprodsubrecnncnv.4	|- S = ( n e. NN |-> prod_ k e. X ( A - ( 1 / n ) ) )
5		eqid	|- ( x e. CC |-> prod_ k e. X ( A - x ) ) = ( x e. CC |-> prod_ k e. X ( A - x ) )
6		oveq2	|- ( m = n -> ( 1 / m ) = ( 1 / n ) )
7	6	cbvmptv	|- ( m e. NN |-> ( 1 / m ) ) = ( n e. NN |-> ( 1 / n ) )
8	1 2 3 4 5 7	fprodsubrecnncnvlem	|- ( ph -> S ~~> prod_ k e. X A )