Metamath Proof Explorer


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𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) ∈ ℕ )