Theorem iprodrecl

Description: The product of a non-trivially converging infinite real sequence is a real number. (Contributed by Scott Fenton, 18-Dec-2017)

	Ref	Expression
Hypotheses	iprodcl.1	|- Z = ( ZZ>= ` M )
	iprodcl.2	|- ( ph -> M e. ZZ )
	iprodcl.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
	iprodcl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	iprodrecl.5	|- ( ( ph /\ k e. Z ) -> A e. RR )
Assertion	iprodrecl	|- ( ph -> prod_ k e. Z A e. RR )

Proof

Step	Hyp	Ref	Expression
1		iprodcl.1	|- Z = ( ZZ>= ` M )
2		iprodcl.2	|- ( ph -> M e. ZZ )
3		iprodcl.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
4		iprodcl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5		iprodrecl.5	|- ( ( ph /\ k e. Z ) -> A e. RR )
6	5	recnd	|- ( ( ph /\ k e. Z ) -> A e. CC )
7	1 2 3 4 6	iprodclim2	|- ( ph -> seq M ( x. , F ) ~~> prod_ k e. Z A )
8	4 5	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
9		remulcl	|- ( ( k e. RR /\ x e. RR ) -> ( k x. x ) e. RR )
10	9	adantl	|- ( ( ph /\ ( k e. RR /\ x e. RR ) ) -> ( k x. x ) e. RR )
11	1 2 8 10	seqf	|- ( ph -> seq M ( x. , F ) : Z --> RR )
12	11	ffvelrnda	|- ( ( ph /\ j e. Z ) -> ( seq M ( x. , F ) ` j ) e. RR )
13	1 2 7 12	climrecl	|- ( ph -> prod_ k e. Z A e. RR )