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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iprodcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iprodcl.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
	iprodcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	iprodrecl.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
Assertion	iprodrecl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		iprodcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iprodcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iprodcl.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
4		iprodcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		iprodrecl.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
6	5	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
7	1 2 3 4 6	iprodclim2	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ∏ 𝑘 ∈ 𝑍 𝐴 )
8	4 5	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9		remulcl	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
10	9	adantl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
11	1 2 8 10	seqf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℝ )
12	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
13	1 2 7 12	climrecl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 ∈ ℝ )