Theorem 0sgmppw

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

	Ref	Expression
Assertion	0sgmppw	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 0 σ ( 𝑃 ↑ 𝐾 ) ) = ( 𝐾 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2		nnexpcl	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ )
3	1 2	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ )
4		0sgm	⊢ ( ( 𝑃 ↑ 𝐾 ) ∈ ℕ → ( 0 σ ( 𝑃 ↑ 𝐾 ) ) = ( ♯ ‘ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐾 ) } ) )
5	3 4	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 0 σ ( 𝑃 ↑ 𝐾 ) ) = ( ♯ ‘ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐾 ) } ) )
6		fzfid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 0 ... 𝐾 ) ∈ Fin )
7		eqid	⊢ ( 𝑛 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑃 ↑ 𝑛 ) ) = ( 𝑛 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑃 ↑ 𝑛 ) )
8	7	dvdsppwf1o	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑛 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑃 ↑ 𝑛 ) ) : ( 0 ... 𝐾 ) –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐾 ) } )
9	6 8	hasheqf1od	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( ♯ ‘ ( 0 ... 𝐾 ) ) = ( ♯ ‘ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐾 ) } ) )
10	5 9	eqtr4d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 0 σ ( 𝑃 ↑ 𝐾 ) ) = ( ♯ ‘ ( 0 ... 𝐾 ) ) )
11		simpr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
12		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
13	11 12	eleqtrdi	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ( ℤ≥ ‘ 0 ) )
14		hashfz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 0 ... 𝐾 ) ) = ( ( 𝐾 − 0 ) + 1 ) )
15	13 14	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( ♯ ‘ ( 0 ... 𝐾 ) ) = ( ( 𝐾 − 0 ) + 1 ) )
16		nn0cn	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
17	16	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℂ )
18	17	subid1d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 − 0 ) = 𝐾 )
19	18	oveq1d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 − 0 ) + 1 ) = ( 𝐾 + 1 ) )
20	10 15 19	3eqtrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ0 ) → ( 0 σ ( 𝑃 ↑ 𝐾 ) ) = ( 𝐾 + 1 ) )