Metamath Proof Explorer


Theorem 0sgm

Description: The value of the sum-of-divisors function, usually denoted ฯƒ0(n). (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion 0sgm ( ๐ด โˆˆ โ„• โ†’ ( 0 ฯƒ ๐ด ) = ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) )

Proof

Step Hyp Ref Expression
1 0z โŠข 0 โˆˆ โ„ค
2 sgmval2 โŠข ( ( 0 โˆˆ โ„ค โˆง ๐ด โˆˆ โ„• ) โ†’ ( 0 ฯƒ ๐ด ) = ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ( ๐‘˜ โ†‘ 0 ) )
3 1 2 mpan โŠข ( ๐ด โˆˆ โ„• โ†’ ( 0 ฯƒ ๐ด ) = ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ( ๐‘˜ โ†‘ 0 ) )
4 elrabi โŠข ( ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โ†’ ๐‘˜ โˆˆ โ„• )
5 4 nncnd โŠข ( ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โ†’ ๐‘˜ โˆˆ โ„‚ )
6 5 exp0d โŠข ( ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โ†’ ( ๐‘˜ โ†‘ 0 ) = 1 )
7 6 sumeq2i โŠข ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ( ๐‘˜ โ†‘ 0 ) = ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } 1
8 fzfid โŠข ( ๐ด โˆˆ โ„• โ†’ ( 1 ... ๐ด ) โˆˆ Fin )
9 dvdsssfz1 โŠข ( ๐ด โˆˆ โ„• โ†’ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โІ ( 1 ... ๐ด ) )
10 8 9 ssfid โŠข ( ๐ด โˆˆ โ„• โ†’ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โˆˆ Fin )
11 ax-1cn โŠข 1 โˆˆ โ„‚
12 fsumconst โŠข ( ( { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โˆˆ Fin โˆง 1 โˆˆ โ„‚ ) โ†’ ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } 1 = ( ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) ยท 1 ) )
13 10 11 12 sylancl โŠข ( ๐ด โˆˆ โ„• โ†’ ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } 1 = ( ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) ยท 1 ) )
14 7 13 eqtrid โŠข ( ๐ด โˆˆ โ„• โ†’ ฮฃ ๐‘˜ โˆˆ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ( ๐‘˜ โ†‘ 0 ) = ( ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) ยท 1 ) )
15 hashcl โŠข ( { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } โˆˆ Fin โ†’ ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) โˆˆ โ„•0 )
16 10 15 syl โŠข ( ๐ด โˆˆ โ„• โ†’ ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) โˆˆ โ„•0 )
17 16 nn0cnd โŠข ( ๐ด โˆˆ โ„• โ†’ ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) โˆˆ โ„‚ )
18 17 mulridd โŠข ( ๐ด โˆˆ โ„• โ†’ ( ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) ยท 1 ) = ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) )
19 3 14 18 3eqtrd โŠข ( ๐ด โˆˆ โ„• โ†’ ( 0 ฯƒ ๐ด ) = ( โ™ฏ โ€˜ { ๐‘ โˆˆ โ„• โˆฃ ๐‘ โˆฅ ๐ด } ) )