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={\mathbb{Z}}_{\ge M}$$
	iprodcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
	iprodcl.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
	iprodcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	iprodrecl.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
Assertion	iprodrecl	$$⊢\phi \to \prod _{k\in Z}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		iprodcl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		iprodcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		iprodcl.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
4		iprodcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
5		iprodrecl.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
6	5	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
7	1 2 3 4 6	iprodclim2	$$⊢\phi \to seqM\left(\times ,F\right)⇝\prod _{k\in Z}A$$
8	4 5	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
9		remulcl	$$⊢\left(k\in ℝ\wedge x\in ℝ\right)\to kx\in ℝ$$
10	9	adantl	$$⊢\left(\phi \wedge \left(k\in ℝ\wedge x\in ℝ\right)\right)\to kx\in ℝ$$
11	1 2 8 10	seqf	$$⊢\phi \to seqM\left(\times ,F\right):Z⟶ℝ$$
12	11	ffvelrnda	$$⊢\left(\phi \wedge j\in Z\right)\to seqM\left(\times ,F\right)\left(j\right)\in ℝ$$
13	1 2 7 12	climrecl	$$⊢\phi \to \prod _{k\in Z}A\in ℝ$$