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 d x | x N ϕ d = N

Proof

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