Theorem sgmnncl

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

	Ref	Expression
Assertion	sgmnncl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
2		sgmval2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )
4		fzfid	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 ... 𝐵 ) ∈ Fin )
5		dvdsssfz1	⊢ ( 𝐵 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
7	4 6	ssfid	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ∈ Fin )
8		elrabi	⊢ ( 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } → 𝑘 ∈ ℕ )
9		simpl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℕ0 )
10		nnexpcl	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑘 ↑ 𝐴 ) ∈ ℕ )
11	8 9 10	syl2anr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → ( 𝑘 ↑ 𝐴 ) ∈ ℕ )
12	11	nnzd	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → ( 𝑘 ↑ 𝐴 ) ∈ ℤ )
13	7 12	fsumzcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) ∈ ℤ )
14		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
15		iddvds	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∥ 𝐵 )
16	14 15	syl	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∥ 𝐵 )
17		breq1	⊢ ( 𝑝 = 𝐵 → ( 𝑝 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵 ) )
18	17	rspcev	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐵 ) → ∃ 𝑝 ∈ ℕ 𝑝 ∥ 𝐵 )
19	16 18	mpdan	⊢ ( 𝐵 ∈ ℕ → ∃ 𝑝 ∈ ℕ 𝑝 ∥ 𝐵 )
20		rabn0	⊢ ( { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ≠ ∅ ↔ ∃ 𝑝 ∈ ℕ 𝑝 ∥ 𝐵 )
21	19 20	sylibr	⊢ ( 𝐵 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ≠ ∅ )
22	21	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ≠ ∅ )
23	11	nnrpd	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → ( 𝑘 ↑ 𝐴 ) ∈ ℝ+ )
24	7 22 23	fsumrpcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) ∈ ℝ+ )
25	24	rpgt0d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 0 < Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )
26		elnnz	⊢ ( Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) ∈ ℕ ↔ ( Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) ∈ ℤ ∧ 0 < Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) ) )
27	13 25 26	sylanbrc	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) ∈ ℕ )
28	3 27	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) ∈ ℕ )