Metamath Proof Explorer

Theorem prodf1f

Description: A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017)

Ref Expression
Hypothesis prodf1.1 ⊢ Z = ℤ ≥ M
Assertion prodf1f ⊢ M ∈ ℤ → seq M × Z × 1 = Z × 1

Proof

Step Hyp Ref Expression
1 prodf1.1 ⊢ Z = ℤ ≥ M
2 1 prodf1 ⊢ k ∈ Z → seq M × Z × 1 ⁡ k = 1
3 1ex ⊢ 1 ∈ V
4 3 fvconst2 ⊢ k ∈ Z → Z × 1 ⁡ k = 1
5 2 4 eqtr4d ⊢ k ∈ Z → seq M × Z × 1 ⁡ k = Z × 1 ⁡ k
6 5 rgen ⊢ ∀ k ∈ Z seq M × Z × 1 ⁡ k = Z × 1 ⁡ k
7 seqfn ⊢ M ∈ ℤ → seq M × Z × 1 Fn ℤ ≥ M
8 1 fneq2i ⊢ seq M × Z × 1 Fn Z ↔ seq M × Z × 1 Fn ℤ ≥ M
9 7 8 sylibr ⊢ M ∈ ℤ → seq M × Z × 1 Fn Z
10 3 fconst ⊢ Z × 1 : Z ⟶ 1
11 ffn ⊢ Z × 1 : Z ⟶ 1 → Z × 1 Fn Z
12 10 11 ax-mp ⊢ Z × 1 Fn Z
13 eqfnfv ⊢ seq M × Z × 1 Fn Z ∧ Z × 1 Fn Z → seq M × Z × 1 = Z × 1 ↔ ∀ k ∈ Z seq M × Z × 1 ⁡ k = Z × 1 ⁡ k
14 9 12 13 sylancl ⊢ M ∈ ℤ → seq M × Z × 1 = Z × 1 ↔ ∀ k ∈ Z seq M × Z × 1 ⁡ k = Z × 1 ⁡ k
15 6 14 mpbiri ⊢ M ∈ ℤ → seq M × Z × 1 = Z × 1