Theorem rpnnen2lem8

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypothesis	rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion	rpnnen2lem8	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
4		simpr	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
5		eqidd	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) )
6	1	rpnnen2lem2	⊢ ( 𝐴 ⊆ ℕ → ( 𝐹 ‘ 𝐴 ) : ℕ ⟶ ℝ )
7	6	adantr	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) : ℕ ⟶ ℝ )
8	7	ffvelrnda	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
9	8	recnd	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℂ )
10		1nn	⊢ 1 ∈ ℕ
11	1	rpnnen2lem5	⊢ ( ( 𝐴 ⊆ ℕ ∧ 1 ∈ ℕ ) → seq 1 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ dom ⇝ )
12	10 11	mpan2	⊢ ( 𝐴 ⊆ ℕ → seq 1 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ dom ⇝ )
13	12	adantr	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → seq 1 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ dom ⇝ )
14	2 3 4 5 9 13	isumsplit	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )