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