0sgmppw

Description: A prime power P ^ K has K + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016)

		Ref	Expression
	Assertion	0sgmppw	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to 0 σ P^{K} = K + 1$

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2		nnexpcl	$⊢ (P \in ℕ \land K \in ℕ_{0}) \to P^{K} \in ℕ$
3	1 2	sylan	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to P^{K} \in ℕ$
4		0sgm	$⊢ P^{K} \in ℕ \to 0 σ P^{K} = \|\{x \in ℕ \| x ∥ P^{K}\}\|$
5	3 4	syl	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to 0 σ P^{K} = \|\{x \in ℕ \| x ∥ P^{K}\}\|$
6		fzfid	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to (0 \dots K) \in Fin$
7		eqid	$⊢ (n \in (0 \dots K) ⟼ P^{n}) = (n \in (0 \dots K) ⟼ P^{n})$
8	7	dvdsppwf1o	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to (n \in (0 \dots K) ⟼ P^{n}) : (0 \dots K) \underset{1-1 onto}{⟶} \{x \in ℕ \| x ∥ P^{K}\}$
9	6 8	hasheqf1od	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to \|(0 \dots K)\| = \|\{x \in ℕ \| x ∥ P^{K}\}\|$
10	5 9	eqtr4d	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to 0 σ P^{K} = \|(0 \dots K)\|$
11		simpr	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to K \in ℕ_{0}$
12		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
13	11 12	eleqtrdi	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to K \in ℤ_{\geq 0}$
14		hashfz	$⊢ K \in ℤ_{\geq 0} \to \|(0 \dots K)\| = K - 0 + 1$
15	13 14	syl	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to \|(0 \dots K)\| = K - 0 + 1$
16		nn0cn	$⊢ K \in ℕ_{0} \to K \in ℂ$
17	16	adantl	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to K \in ℂ$
18	17	subid1d	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to K - 0 = K$
19	18	oveq1d	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to K - 0 + 1 = K + 1$
20	10 15 19	3eqtrd	$⊢ (P \in ℙ \land K \in ℕ_{0}) \to 0 σ P^{K} = K + 1$

Metamath Proof Explorer