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 dvdsfi 
 |-  ( N e. NN -> { x e. NN | x || N } e. Fin )
11 fzofi 
 |-  ( 0 ..^ N ) e. Fin
12 ssrab2 
 |-  { z e. ( 0 ..^ N ) | ( z gcd N ) = y } C_ ( 0 ..^ N )
13 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 )
14 11 12 13 mp2an 
 |-  { z e. ( 0 ..^ N ) | ( z gcd N ) = y } e. Fin
15 14 a1i 
 |-  ( ( N e. NN /\ y e. { x e. NN | x || N } ) -> { z e. ( 0 ..^ N ) | ( z gcd N ) = y } e. Fin )
16 oveq1 
 |-  ( z = w -> ( z gcd N ) = ( w gcd N ) )
17 16 eqeq1d 
 |-  ( z = w -> ( ( z gcd N ) = y <-> ( w gcd N ) = y ) )
18 17 elrab 
 |-  ( w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } <-> ( w e. ( 0 ..^ N ) /\ ( w gcd N ) = y ) )
19 18 simprbi 
 |-  ( w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } -> ( w gcd N ) = y )
20 19 rgen 
 |-  A. w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ( w gcd N ) = y
21 20 rgenw 
 |-  A. y e. { x e. NN | x || N } A. w e. { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ( w gcd N ) = y
22 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 } )
23 21 22 mp1i 
 |-  ( N e. NN -> Disj_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } )
24 10 15 23 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 } ) )
25 fveq2 
 |-  ( d = ( N / y ) -> ( phi ` d ) = ( phi ` ( N / y ) ) )
26 eqid 
 |-  { x e. NN | x || N } = { x e. NN | x || N }
27 eqid 
 |-  ( z e. { x e. NN | x || N } |-> ( N / z ) ) = ( z e. { x e. NN | x || N } |-> ( N / z ) )
28 26 27 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 } )
29 oveq2 
 |-  ( z = y -> ( N / z ) = ( N / y ) )
30 ovex 
 |-  ( N / y ) e. _V
31 29 27 30 fvmpt 
 |-  ( y e. { x e. NN | x || N } -> ( ( z e. { x e. NN | x || N } |-> ( N / z ) ) ` y ) = ( N / y ) )
32 31 adantl 
 |-  ( ( N e. NN /\ y e. { x e. NN | x || N } ) -> ( ( z e. { x e. NN | x || N } |-> ( N / z ) ) ` y ) = ( N / y ) )
33 elrabi 
 |-  ( d e. { x e. NN | x || N } -> d e. NN )
34 33 adantl 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> d e. NN )
35 34 phicld 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( phi ` d ) e. NN )
36 35 nncnd 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( phi ` d ) e. CC )
37 25 10 28 32 36 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 ) ) )
38 9 24 37 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 } ) )
39 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 }
40 breq1 
 |-  ( x = ( z gcd N ) -> ( x || N <-> ( z gcd N ) || N ) )
41 elfzoelz 
 |-  ( z e. ( 0 ..^ N ) -> z e. ZZ )
42 41 adantl 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> z e. ZZ )
43 nnz 
 |-  ( N e. NN -> N e. ZZ )
44 43 adantr 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> N e. ZZ )
45 nnne0 
 |-  ( N e. NN -> N =/= 0 )
46 45 neneqd 
 |-  ( N e. NN -> -. N = 0 )
47 46 intnand 
 |-  ( N e. NN -> -. ( z = 0 /\ N = 0 ) )
48 47 adantr 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> -. ( z = 0 /\ N = 0 ) )
49 gcdn0cl 
 |-  ( ( ( z e. ZZ /\ N e. ZZ ) /\ -. ( z = 0 /\ N = 0 ) ) -> ( z gcd N ) e. NN )
50 42 44 48 49 syl21anc 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( z gcd N ) e. NN )
51 gcddvds 
 |-  ( ( z e. ZZ /\ N e. ZZ ) -> ( ( z gcd N ) || z /\ ( z gcd N ) || N ) )
52 42 44 51 syl2anc 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( ( z gcd N ) || z /\ ( z gcd N ) || N ) )
53 52 simprd 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( z gcd N ) || N )
54 40 50 53 elrabd 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> ( z gcd N ) e. { x e. NN | x || N } )
55 clel5 
 |-  ( ( z gcd N ) e. { x e. NN | x || N } <-> E. y e. { x e. NN | x || N } ( z gcd N ) = y )
56 54 55 sylib 
 |-  ( ( N e. NN /\ z e. ( 0 ..^ N ) ) -> E. y e. { x e. NN | x || N } ( z gcd N ) = y )
57 56 ralrimiva 
 |-  ( N e. NN -> A. z e. ( 0 ..^ N ) E. y e. { x e. NN | x || N } ( z gcd N ) = y )
58 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 )
59 57 58 sylibr 
 |-  ( N e. NN -> ( 0 ..^ N ) = { z e. ( 0 ..^ N ) | E. y e. { x e. NN | x || N } ( z gcd N ) = y } )
60 39 59 eqtr4id 
 |-  ( N e. NN -> U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } = ( 0 ..^ N ) )
61 60 fveq2d 
 |-  ( N e. NN -> ( # ` U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = ( # ` ( 0 ..^ N ) ) )
62 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
63 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
64 62 63 syl 
 |-  ( N e. NN -> ( # ` ( 0 ..^ N ) ) = N )
65 61 64 eqtrd 
 |-  ( N e. NN -> ( # ` U_ y e. { x e. NN | x || N } { z e. ( 0 ..^ N ) | ( z gcd N ) = y } ) = N )
66 38 65 eqtrd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )