rpnnen2lem6

		Ref	Expression
	Hypothesis	rpnnen2.1	$⊢ F = (x \in 𝒫 ℕ ⟼ (n \in ℕ ⟼ if (n \in x, {(\frac{1}{3})}^{n}, 0)))$
	Assertion	rpnnen2lem6	$⊢ (A \subseteq ℕ \land M \in ℕ) \to \sum_{k \in ℤ_{\geq M}} F (A) (k) \in ℝ$

Step	Hyp	Ref	Expression
1		rpnnen2.1	$⊢ F = (x \in 𝒫 ℕ ⟼ (n \in ℕ ⟼ if (n \in x, {(\frac{1}{3})}^{n}, 0)))$
2		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
3		nnz	$⊢ M \in ℕ \to M \in ℤ$
4	3	adantl	$⊢ (A \subseteq ℕ \land M \in ℕ) \to M \in ℤ$
5		eqidd	$⊢ ((A \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (A) (k) = F (A) (k)$
6	1	rpnnen2lem2	$⊢ A \subseteq ℕ \to F (A) : ℕ ⟶ ℝ$
7	6	ad2antrr	$⊢ ((A \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (A) : ℕ ⟶ ℝ$
8		eluznn	$⊢ (M \in ℕ \land k \in ℤ_{\geq M}) \to k \in ℕ$
9	8	adantll	$⊢ ((A \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to k \in ℕ$
10	7 9	ffvelrnd	$⊢ ((A \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (A) (k) \in ℝ$
11	1	rpnnen2lem5	$⊢ (A \subseteq ℕ \land M \in ℕ) \to seq M (+ F (A)) \in dom ⇝$
12	2 4 5 10 11	isumrecl	$⊢ (A \subseteq ℕ \land M \in ℕ) \to \sum_{k \in ℤ_{\geq M}} F (A) (k) \in ℝ$

Metamath Proof Explorer