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

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