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 
|- ( ( 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 )