Metamath Proof Explorer

Theorem ser0f

Description: A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014)

Ref Expression
Hypothesis ser0.1 ⊢ Z = ℤ ≥ M
Assertion ser0f ⊢ M ∈ ℤ → seq M + Z × 0 = Z × 0

Proof

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