Theorem iprod

Description: Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		zprod.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		zprod.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		zprod.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
4		iprod.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
5		iprod.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
6		ssidd	⊢ ( 𝜑 → 𝑍 ⊆ 𝑍 )
7		iftrue	⊢ ( 𝑘 ∈ 𝑍 → if ( 𝑘 ∈ 𝑍 , 𝐵 , 1 ) = 𝐵 )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝑍 , 𝐵 , 1 ) = 𝐵 )
9	4 8	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝑍 , 𝐵 , 1 ) )
10	1 2 3 6 9 5	zprod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )