Theorem prodf1

Description: The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypothesis	prodf1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	prodf1	⊢ ( 𝑁 ∈ 𝑍 → ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		prodf1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		1t1e1	⊢ ( 1 · 1 ) = 1
3	2	a1i	⊢ ( 𝑁 ∈ 𝑍 → ( 1 · 1 ) = 1 )
4	1	eleq2i	⊢ ( 𝑁 ∈ 𝑍 ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5	4	biimpi	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
6		ax-1cn	⊢ 1 ∈ ℂ
7		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
8	7 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ 𝑍 )
9	8	adantl	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ 𝑍 )
10		fvconst2g	⊢ ( ( 1 ∈ ℂ ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 1 } ) ‘ 𝑘 ) = 1 )
11	6 9 10	sylancr	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑍 × { 1 } ) ‘ 𝑘 ) = 1 )
12	3 5 11	seqid3	⊢ ( 𝑁 ∈ 𝑍 → ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑁 ) = 1 )