Theorem iprodclim

Description: An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017)

	Ref	Expression
Hypotheses	iprodclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iprodclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iprodclim.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
	iprodclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	iprodclim.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	iprodclim.6	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝐵 )
Assertion	iprodclim	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		iprodclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iprodclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iprodclim.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
4		iprodclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		iprodclim.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
6		iprodclim.6	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝐵 )
7	1 2 3 4 5	iprod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
8		fclim	⊢ ⇝ : dom ⇝ ⟶ ℂ
9		ffun	⊢ ( ⇝ : dom ⇝ ⟶ ℂ → Fun ⇝ )
10	8 9	ax-mp	⊢ Fun ⇝
11		funbrfv	⊢ ( Fun ⇝ → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐵 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 𝐵 ) )
12	10 6 11	mpsyl	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 𝐵 )
13	7 12	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = 𝐵 )