Metamath Proof Explorer


Theorem sgmnncl

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

Ref Expression
Assertion sgmnncl
|- ( ( A e. NN0 /\ B e. NN ) -> ( A sigma B ) e. NN )

Proof

Step Hyp Ref Expression
1 nn0z
 |-  ( A e. NN0 -> A e. ZZ )
2 sgmval2
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )
3 1 2 sylan
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )
4 fzfid
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( 1 ... B ) e. Fin )
5 dvdsssfz1
 |-  ( B e. NN -> { p e. NN | p || B } C_ ( 1 ... B ) )
6 5 adantl
 |-  ( ( A e. NN0 /\ B e. NN ) -> { p e. NN | p || B } C_ ( 1 ... B ) )
7 4 6 ssfid
 |-  ( ( A e. NN0 /\ B e. NN ) -> { p e. NN | p || B } e. Fin )
8 elrabi
 |-  ( k e. { p e. NN | p || B } -> k e. NN )
9 simpl
 |-  ( ( A e. NN0 /\ B e. NN ) -> A e. NN0 )
10 nnexpcl
 |-  ( ( k e. NN /\ A e. NN0 ) -> ( k ^ A ) e. NN )
11 8 9 10 syl2anr
 |-  ( ( ( A e. NN0 /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> ( k ^ A ) e. NN )
12 11 nnzd
 |-  ( ( ( A e. NN0 /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> ( k ^ A ) e. ZZ )
13 7 12 fsumzcl
 |-  ( ( A e. NN0 /\ B e. NN ) -> sum_ k e. { p e. NN | p || B } ( k ^ A ) e. ZZ )
14 nnz
 |-  ( B e. NN -> B e. ZZ )
15 iddvds
 |-  ( B e. ZZ -> B || B )
16 14 15 syl
 |-  ( B e. NN -> B || B )
17 breq1
 |-  ( p = B -> ( p || B <-> B || B ) )
18 17 rspcev
 |-  ( ( B e. NN /\ B || B ) -> E. p e. NN p || B )
19 16 18 mpdan
 |-  ( B e. NN -> E. p e. NN p || B )
20 rabn0
 |-  ( { p e. NN | p || B } =/= (/) <-> E. p e. NN p || B )
21 19 20 sylibr
 |-  ( B e. NN -> { p e. NN | p || B } =/= (/) )
22 21 adantl
 |-  ( ( A e. NN0 /\ B e. NN ) -> { p e. NN | p || B } =/= (/) )
23 11 nnrpd
 |-  ( ( ( A e. NN0 /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> ( k ^ A ) e. RR+ )
24 7 22 23 fsumrpcl
 |-  ( ( A e. NN0 /\ B e. NN ) -> sum_ k e. { p e. NN | p || B } ( k ^ A ) e. RR+ )
25 24 rpgt0d
 |-  ( ( A e. NN0 /\ B e. NN ) -> 0 < sum_ k e. { p e. NN | p || B } ( k ^ A ) )
26 elnnz
 |-  ( sum_ k e. { p e. NN | p || B } ( k ^ A ) e. NN <-> ( sum_ k e. { p e. NN | p || B } ( k ^ A ) e. ZZ /\ 0 < sum_ k e. { p e. NN | p || B } ( k ^ A ) ) )
27 13 25 26 sylanbrc
 |-  ( ( A e. NN0 /\ B e. NN ) -> sum_ k e. { p e. NN | p || B } ( k ^ A ) e. NN )
28 3 27 eqeltrd
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A sigma B ) e. NN )