Metamath Proof Explorer

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 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
Assertion rpnnen2lem8 ⊢ A ⊆ ℕ ∧ M ∈ ℕ → ∑ k ∈ ℕ F ⁡ A ⁡ k = ∑ k = 1 M − 1 F ⁡ A ⁡ k + ∑ k ∈ ℤ ≥ M F ⁡ A ⁡ k

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 nnuz ⊢ ℕ = ℤ ≥ 1
3 eqid ⊢ ℤ ≥ M = ℤ ≥ M
4 simpr ⊢ A ⊆ ℕ ∧ M ∈ ℕ → M ∈ ℕ
5 eqidd ⊢ A ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k = F ⁡ A ⁡ k
6 1 rpnnen2lem2 ⊢ A ⊆ ℕ → F ⁡ A : ℕ ⟶ ℝ
7 6 adantr ⊢ A ⊆ ℕ ∧ M ∈ ℕ → F ⁡ A : ℕ ⟶ ℝ
8 7 ffvelrnda ⊢ A ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ∈ ℝ
9 8 recnd ⊢ A ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ∈ ℂ
10 1nn ⊢ 1 ∈ ℕ
11 1 rpnnen2lem5 ⊢ A ⊆ ℕ ∧ 1 ∈ ℕ → seq 1 + F ⁡ A ∈ dom ⁡ ⇝
12 10 11 mpan2 ⊢ A ⊆ ℕ → seq 1 + F ⁡ A ∈ dom ⁡ ⇝
13 12 adantr ⊢ A ⊆ ℕ ∧ M ∈ ℕ → seq 1 + F ⁡ A ∈ dom ⁡ ⇝
14 2 3 4 5 9 13 isumsplit ⊢ A ⊆ ℕ ∧ M ∈ ℕ → ∑ k ∈ ℕ F ⁡ A ⁡ k = ∑ k = 1 M − 1 F ⁡ A ⁡ k + ∑ k ∈ ℤ ≥ M F ⁡ A ⁡ k