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

Metamath Proof Explorer

Theorem iprodn0

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

Ref Expression
Hypotheses zprodn0.1 ⊢ Z = ℤ ≥ M
zprodn0.2 ⊢ φ → M ∈ ℤ
zprodn0.3 ⊢ φ → X ≠ 0
zprodn0.4 ⊢ φ → seq M × F ⇝ X
iprodn0.5 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
iprodn0.6 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
Assertion iprodn0 ⊢ φ → ∏ k ∈ Z B = X

Proof

Step Hyp Ref Expression
1 zprodn0.1 ⊢ Z = ℤ ≥ M
2 zprodn0.2 ⊢ φ → M ∈ ℤ
3 zprodn0.3 ⊢ φ → X ≠ 0
4 zprodn0.4 ⊢ φ → seq M × F ⇝ X
5 iprodn0.5 ⊢ φ ∧ k ∈ Z → F ⁡ k = B
6 iprodn0.6 ⊢ φ ∧ k ∈ Z → B ∈ ℂ
7 ssidd ⊢ φ → Z ⊆ Z
8 iftrue ⊢ k ∈ Z → if k ∈ Z B 1 = B
9 8 adantl ⊢ φ ∧ k ∈ Z → if k ∈ Z B 1 = B
10 5 9 eqtr4d ⊢ φ ∧ k ∈ Z → F ⁡ k = if k ∈ Z B 1
11 1 2 3 4 7 10 6 zprodn0 ⊢ φ → ∏ k ∈ Z B = X