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

Proof

Step	Hyp	Ref	Expression
1		fprodaddrecnncnv.1	|- F/ k ph
2		fprodaddrecnncnv.2	|- ( ph -> X e. Fin )
3		fprodaddrecnncnv.3	|- ( ( ph /\ k e. X ) -> A e. CC )
4		fprodaddrecnncnv.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	fprodaddrecnncnvlem	|- ( ph -> S ~~> prod_ k e. X A )