Metamath Proof Explorer

Theorem phisum

Description: The divisor sum identity of the totient function. Theorem 2.2 in ApostolNT p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion phisum 
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = y -> ( x || N <-> y || N ) )
2 1 elrab 
 |-  ( y e. { x e. NN | x || N } <-> ( y e. NN /\ y || N ) )
3 hashgcdeq 
 |-  ( ( N e. NN /\ y e. NN ) -> ( # ` { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = if ( y || N , ( phi ` ( N / y ) ) , 0 ) )
4 3 adantrr 
 |-  ( ( N e. NN /\ ( y e. NN /\ y || N ) ) -> ( # ` { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = if ( y || N , ( phi ` ( N / y ) ) , 0 ) )
5 iftrue 
 |-  ( y || N -> if ( y || N , ( phi ` ( N / y ) ) , 0 ) = ( phi ` ( N / y ) ) )
6 5 ad2antll 
 |-  ( ( N e. NN /\ ( y e. NN /\ y || N ) ) -> if ( y || N , ( phi ` ( N / y ) ) , 0 ) = ( phi ` ( N / y ) ) )
7 4 6 eqtrd 
 |-  ( ( N e. NN /\ ( y e. NN /\ y || N ) ) -> ( # ` { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = ( phi ` ( N / y ) ) )
8 2 7 sylan2b 
 |-  ( ( N e. NN /\ y e. { x e. NN | x || N } ) -> ( # ` { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = ( phi ` ( N / y ) ) )
9 8 sumeq2dv 
 |-  ( N e. NN -> sum_ y e. { x e. NN | x || N } ( # ` { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = sum_ y e. { x e. NN | x || N } ( phi ` ( N / y ) ) )
10 fzfi 
 |-  ( 1 ... N ) e. Fin
11 dvdsssfz1 
 |-  ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) )
12 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ { x e. NN | x || N } C_ ( 1 ... N ) ) -> { x e. NN | x || N } e. Fin )
13 10 11 12 sylancr 
 |-  ( N e. NN -> { x e. NN | x || N } e. Fin )
14 fzofi 
 |-  ( 0 ..^ N ) e. Fin
15 ssrab2 
 |-  { z e. ( 0 ..^ N ) | ( z gcd N ) = y } C_ ( 0 ..^ N )
16 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ { z e. ( 0 ..^ N ) | ( z gcd N ) = y } C_ ( 0 ..^ N ) ) -> { z e. ( 0 ..^ N ) | ( z gcd N ) = y } e. Fin )
17 14 15 16 mp2an 
 |-  { z e. ( 0 ..^ N ) | ( z gcd N ) = y } e. Fin
18 17 a1i 
 |-  ( ( N e. NN /\ y e. { x e. NN | x || N } ) -> { z e. ( 0 ..^ N ) | ( z gcd N ) = y } e. Fin )
19 oveq1 
 |-  ( z = w -> ( z gcd N ) = ( w gcd N ) )
20 19 eqeq1d 
 |-  ( z = w -> ( ( z gcd N ) = y <-> ( w gcd N ) = y ) )
21 20 elrab 
 |-  ( w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } <-> ( w e. ( 0 ..^ N ) /\ ( w gcd N ) = y ) )
22 21 simprbi 
 |-  ( w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } -> ( w gcd N ) = y )
23 22 rgen 
 |-  A. w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ( w gcd N ) = y
24 23 rgenw 
 |-  A. y e. { x e. NN | x || N } A. w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ( w gcd N ) = y
25 invdisj 
 |-  ( A. y e. { x e. NN | x || N } A. w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ( w gcd N ) = y -> Disj_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } )
26 24 25 mp1i 
 |-  ( N e. NN -> Disj_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } )
27 13 18 26 hashiun 
 |-  ( N e. NN -> ( # ` U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = sum_ y e. { x e. NN | x || N } ( # ` { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) )
28 fveq2 
 |-  ( d = ( N / y ) -> ( phi ` d ) = ( phi ` ( N / y ) ) )
29 eqid 
 |-  { x e. NN | x || N } = { x e. NN | x || N }
30 eqid 
 |-  ( z e. { x e. NN | x || N } |-> ( N / z ) ) = ( z e. { x e. NN | x || N } |-> ( N / z ) )
31 29 30 dvdsflip 
 |-  ( N e. NN -> ( z e. { x e. NN | x || N } |-> ( N / z ) ) : { x e. NN | x || N } -1-1-onto-> { x e. NN | x || N } )
32 oveq2 
 |-  ( z = y -> ( N / z ) = ( N / y ) )
33 ovex 
 |-  ( N / y ) e. _V
34 32 30 33 fvmpt 
 |-  ( y e. { x e. NN | x || N } -> ( ( z e. { x e. NN | x || N } |-> ( N / z ) ) ` y ) = ( N / y ) )
35 34 adantl 
 |-  ( ( N e. NN /\ y e. { x e. NN | x || N } ) -> ( ( z e. { x e. NN | x || N } |-> ( N / z ) ) ` y ) = ( N / y ) )
36 elrabi 
 |-  ( d e. { x e. NN | x || N } -> d e. NN )
37 36 adantl 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> d e. NN )
38 37 phicld 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( phi ` d ) e. NN )
39 38 nncnd 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( phi ` d ) e. CC )
40 28 13 31 35 39 fsumf1o 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = sum_ y e. { x e. NN | x || N } ( phi ` ( N / y ) ) )
41 9 27 40 3eqtr4rd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = ( # ` U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) )
42 iunrab 
 |-  U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } = { z e. ( 0 ..^ N ) | E. y e. { x e. NN | x || N } ( z gcd N ) = y }
43 breq1 
 |-  ( x = ( z gcd N ) -> ( x || N <-> ( z gcd N ) || N ) )
44 elfzoelz 
 |-  ( z e. ( 0 ..^ N ) -> z e. ZZ )
45 44 adantl 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> z e. ZZ )
46 nnz 
 |-  ( N e. NN -> N e. ZZ )
47 46 adantr 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> N e. ZZ )
48 nnne0 
 |-  ( N e. NN -> N =/= 0 )
49 48 neneqd 
 |-  ( N e. NN -> -. N = 0 )
50 49 intnand 
 |-  ( N e. NN -> -. ( z = 0 /\ N = 0 ) )
51 50 adantr 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> -. ( z = 0 /\ N = 0 ) )
52 gcdn0cl 
 |-  ( ( ( z e. ZZ /\ N e. ZZ ) /\ -. ( z = 0 /\ N = 0 ) ) -> ( z gcd N ) e. NN )
53 45 47 51 52 syl21anc 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( z gcd N ) e. NN )
54 gcddvds 
 |-  ( ( z e. ZZ /\ N e. ZZ ) -> ( ( z gcd N ) || z /\ ( z gcd N ) || N ) )
55 45 47 54 syl2anc 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( ( z gcd N ) || z /\ ( z gcd N ) || N ) )
56 55 simprd 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( z gcd N ) || N )
57 43 53 56 elrabd 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( z gcd N ) e. { x e. NN | x || N } )
58 clel5 
 |-  ( ( z gcd N ) e. { x e. NN | x || N } <-> E. y e. { x e. NN | x || N } ( z gcd N ) = y )
59 57 58 sylib 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> E. y e. { x e. NN | x || N } ( z gcd N ) = y )
60 59 ralrimiva 
 |-  ( N e. NN -> A. z e. ( 0 ..^ N ) E. y e. { x e. NN | x || N } ( z gcd N ) = y )
61 rabid2 
 |-  ( ( 0 ..^ N ) = { z e. ( 0 ..^ N ) | E. y e. { x e. NN | x || N } ( z gcd N ) = y } <-> A. z e. ( 0 ..^ N ) E. y e. { x e. NN | x || N } ( z gcd N ) = y )
62 60 61 sylibr 
 |-  ( N e. NN -> ( 0 ..^ N ) = { z e. ( 0 ..^ N ) | E. y e. { x e. NN | x || N } ( z gcd N ) = y } )
63 42 62 eqtr4id 
 |-  ( N e. NN -> U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } = ( 0 ..^ N ) )
64 63 fveq2d 
 |-  ( N e. NN -> ( # ` U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = ( # ` ( 0 ..^ N ) ) )
65 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
66 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
67 65 66 syl 
 |-  ( N e. NN -> ( # ` ( 0 ..^ N ) ) = N )
68 64 67 eqtrd 
 |-  ( N e. NN -> ( # ` U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = N )
69 41 68 eqtrd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )