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

Metamath Proof Explorer

Theorem isumnn0nn

Description: Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumnn0nn.1 ⊢ ( 𝑘 = 0 → 𝐴 = 𝐵 )
isumnn0nn.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumnn0nn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
isumnn0nn.4 ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion isumnn0nn ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐴 = ( 𝐵 + Σ 𝑘 ∈ ℕ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isumnn0nn.1 ⊢ ( 𝑘 = 0 → 𝐴 = 𝐵 )
2 isumnn0nn.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
3 isumnn0nn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
4 isumnn0nn.4 ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
5 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
7 5 6 2 3 4 isum1p ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐴 = ( ( 𝐹 ‘ 0 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 ) )
8 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
9 8 1 eqeq12d ⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ 𝑘 ) = 𝐴 ↔ ( 𝐹 ‘ 0 ) = 𝐵 ) )
10 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) = 𝐴 )
11 0nn0 ⊢ 0 ∈ ℕ0
12 11 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
13 9 10 12 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝐵 )
14 0p1e1 ⊢ ( 0 + 1 ) = 1
15 14 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
16 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
17 15 16 eqtr4i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
18 17 sumeq1i ⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 = Σ 𝑘 ∈ ℕ 𝐴
19 18 a1i ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )
20 13 19 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ℕ 𝐴 ) )
21 7 20 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐴 = ( 𝐵 + Σ 𝑘 ∈ ℕ 𝐴 ) )