Metamath Proof Explorer

Theorem sgmnncl

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

Ref Expression
Assertion sgmnncl ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ → A σ B ∈ ℕ

Proof

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