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

Metamath Proof Explorer

Theorem sgmval2

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

Ref Expression
Assertion sgmval2 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2 sgmval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )
3 1 2 sylan ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )
4 ssrab2 ⊢ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ⊆ ℕ
5 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } )
6 4 5 sselid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ∈ ℕ )
7 6 nncnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ∈ ℂ )
8 6 nnne0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ≠ 0 )
9 simpll ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝐴 ∈ ℤ )
10 7 8 9 cxpexpzd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → ( 𝑘 ↑𝑐 𝐴 ) = ( 𝑘 ↑ 𝐴 ) )
11 10 sumeq2dv ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )
12 3 11 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )