This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )