This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )