sgmval2

Description: The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015)

		Ref	Expression
	Assertion	sgmval2	$⊢ (A \in ℤ \land B \in ℕ) \to A σ B = \sum_{k \in \{p \in ℕ \| p ∥ B\}} k^{A}$

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2		sgmval	$⊢ (A \in ℂ \land B \in ℕ) \to A σ B = \sum_{k \in \{p \in ℕ \| p ∥ B\}} k^{A}$
3	1 2	sylan	$⊢ (A \in ℤ \land B \in ℕ) \to A σ B = \sum_{k \in \{p \in ℕ \| p ∥ B\}} k^{A}$
4		ssrab2	$⊢ \{p \in ℕ \| p ∥ B\} \subseteq ℕ$
5		simpr	$⊢ ((A \in ℤ \land B \in ℕ) \land k \in \{p \in ℕ \| p ∥ B\}) \to k \in \{p \in ℕ \| p ∥ B\}$
6	4 5	sselid	$⊢ ((A \in ℤ \land B \in ℕ) \land k \in \{p \in ℕ \| p ∥ B\}) \to k \in ℕ$
7	6	nncnd	$⊢ ((A \in ℤ \land B \in ℕ) \land k \in \{p \in ℕ \| p ∥ B\}) \to k \in ℂ$
8	6	nnne0d	$⊢ ((A \in ℤ \land B \in ℕ) \land k \in \{p \in ℕ \| p ∥ B\}) \to k \neq 0$
9		simpll	$⊢ ((A \in ℤ \land B \in ℕ) \land k \in \{p \in ℕ \| p ∥ B\}) \to A \in ℤ$
10	7 8 9	cxpexpzd	$⊢ ((A \in ℤ \land B \in ℕ) \land k \in \{p \in ℕ \| p ∥ B\}) \to k^{A} = k^{A}$
11	10	sumeq2dv	$⊢ (A \in ℤ \land B \in ℕ) \to \sum_{k \in \{p \in ℕ \| p ∥ B\}} k^{A} = \sum_{k \in \{p \in ℕ \| p ∥ B\}} k^{A}$
12	3 11	eqtrd	$⊢ (A \in ℤ \land B \in ℕ) \to A σ B = \sum_{k \in \{p \in ℕ \| p ∥ B\}} k^{A}$

Metamath Proof Explorer