Metamath Proof Explorer

Theorem musum

Description: The sum of the Möbius function over the divisors of N gives one if N = 1 , but otherwise always sums to zero. Theorem 2.1 in ApostolNT p. 25. This makes the Möbius function useful for inverting divisor sums; see also muinv . (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion musum 
|- ( N e. NN -> sum_ k e. { n e. NN | n || N } ( mmu ` k ) = if ( N = 1 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = k -> ( mmu ` n ) = ( mmu ` k ) )
2 1 neeq1d 
 |-  ( n = k -> ( ( mmu ` n ) =/= 0 <-> ( mmu ` k ) =/= 0 ) )
3 breq1 
 |-  ( n = k -> ( n || N <-> k || N ) )
4 2 3 anbi12d 
 |-  ( n = k -> ( ( ( mmu ` n ) =/= 0 /\ n || N ) <-> ( ( mmu ` k ) =/= 0 /\ k || N ) ) )
5 4 elrab 
 |-  ( k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } <-> ( k e. NN /\ ( ( mmu ` k ) =/= 0 /\ k || N ) ) )
6 muval2 
 |-  ( ( k e. NN /\ ( mmu ` k ) =/= 0 ) -> ( mmu ` k ) = ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
7 6 adantrr 
 |-  ( ( k e. NN /\ ( ( mmu ` k ) =/= 0 /\ k || N ) ) -> ( mmu ` k ) = ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
8 5 7 sylbi 
 |-  ( k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } -> ( mmu ` k ) = ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
9 8 adantl 
 |-  ( ( N e. NN /\ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> ( mmu ` k ) = ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
10 9 sumeq2dv 
 |-  ( N e. NN -> sum_ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ( mmu ` k ) = sum_ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
11 simpr 
 |-  ( ( ( mmu ` n ) =/= 0 /\ n || N ) -> n || N )
12 11 a1i 
 |-  ( ( N e. NN /\ n e. NN ) -> ( ( ( mmu ` n ) =/= 0 /\ n || N ) -> n || N ) )
13 12 ss2rabdv 
 |-  ( N e. NN -> { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } C_ { n e. NN | n || N } )
14 ssrab2 
 |-  { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } C_ NN
15 simpr 
 |-  ( ( N e. NN /\ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } )
16 14 15 sselid 
 |-  ( ( N e. NN /\ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> k e. NN )
17 mucl 
 |-  ( k e. NN -> ( mmu ` k ) e. ZZ )
18 16 17 syl 
 |-  ( ( N e. NN /\ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> ( mmu ` k ) e. ZZ )
19 18 zcnd 
 |-  ( ( N e. NN /\ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> ( mmu ` k ) e. CC )
20 difrab 
 |-  ( { n e. NN | n || N } \ { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) = { n e. NN | ( n || N /\ -. ( ( mmu ` n ) =/= 0 /\ n || N ) ) }
21 pm3.21 
 |-  ( n || N -> ( ( mmu ` n ) =/= 0 -> ( ( mmu ` n ) =/= 0 /\ n || N ) ) )
22 21 necon1bd 
 |-  ( n || N -> ( -. ( ( mmu ` n ) =/= 0 /\ n || N ) -> ( mmu ` n ) = 0 ) )
23 22 imp 
 |-  ( ( n || N /\ -. ( ( mmu ` n ) =/= 0 /\ n || N ) ) -> ( mmu ` n ) = 0 )
24 23 a1i 
 |-  ( n e. NN -> ( ( n || N /\ -. ( ( mmu ` n ) =/= 0 /\ n || N ) ) -> ( mmu ` n ) = 0 ) )
25 24 ss2rabi 
 |-  { n e. NN | ( n || N /\ -. ( ( mmu ` n ) =/= 0 /\ n || N ) ) } C_ { n e. NN | ( mmu ` n ) = 0 }
26 20 25 eqsstri 
 |-  ( { n e. NN | n || N } \ { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) C_ { n e. NN | ( mmu ` n ) = 0 }
27 26 sseli 
 |-  ( k e. ( { n e. NN | n || N } \ { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> k e. { n e. NN | ( mmu ` n ) = 0 } )
28 fveqeq2 
 |-  ( n = k -> ( ( mmu ` n ) = 0 <-> ( mmu ` k ) = 0 ) )
29 28 elrab 
 |-  ( k e. { n e. NN | ( mmu ` n ) = 0 } <-> ( k e. NN /\ ( mmu ` k ) = 0 ) )
30 29 simprbi 
 |-  ( k e. { n e. NN | ( mmu ` n ) = 0 } -> ( mmu ` k ) = 0 )
31 27 30 syl 
 |-  ( k e. ( { n e. NN | n || N } \ { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> ( mmu ` k ) = 0 )
32 31 adantl 
 |-  ( ( N e. NN /\ k e. ( { n e. NN | n || N } \ { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) ) -> ( mmu ` k ) = 0 )
33 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
34 dvdsssfz1 
 |-  ( N e. NN -> { n e. NN | n || N } C_ ( 1 ... N ) )
35 33 34 ssfid 
 |-  ( N e. NN -> { n e. NN | n || N } e. Fin )
36 13 19 32 35 fsumss 
 |-  ( N e. NN -> sum_ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ( mmu ` k ) = sum_ k e. { n e. NN | n || N } ( mmu ` k ) )
37 fveq2 
 |-  ( x = { p e. Prime | p || k } -> ( # ` x ) = ( # ` { p e. Prime | p || k } ) )
38 37 oveq2d 
 |-  ( x = { p e. Prime | p || k } -> ( -u 1 ^ ( # ` x ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
39 35 13 ssfid 
 |-  ( N e. NN -> { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } e. Fin )
40 eqid 
 |-  { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } = { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) }
41 eqid 
 |-  ( m e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } |-> { p e. Prime | p || m } ) = ( m e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } |-> { p e. Prime | p || m } )
42 oveq1 
 |-  ( q = p -> ( q pCnt x ) = ( p pCnt x ) )
43 42 cbvmptv 
 |-  ( q e. Prime |-> ( q pCnt x ) ) = ( p e. Prime |-> ( p pCnt x ) )
44 oveq2 
 |-  ( x = m -> ( p pCnt x ) = ( p pCnt m ) )
45 44 mpteq2dv 
 |-  ( x = m -> ( p e. Prime |-> ( p pCnt x ) ) = ( p e. Prime |-> ( p pCnt m ) ) )
46 43 45 eqtrid 
 |-  ( x = m -> ( q e. Prime |-> ( q pCnt x ) ) = ( p e. Prime |-> ( p pCnt m ) ) )
47 46 cbvmptv 
 |-  ( x e. NN |-> ( q e. Prime |-> ( q pCnt x ) ) ) = ( m e. NN |-> ( p e. Prime |-> ( p pCnt m ) ) )
48 40 41 47 sqff1o 
 |-  ( N e. NN -> ( m e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } |-> { p e. Prime | p || m } ) : { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } -1-1-onto-> ~P { p e. Prime | p || N } )
49 breq2 
 |-  ( m = k -> ( p || m <-> p || k ) )
50 49 rabbidv 
 |-  ( m = k -> { p e. Prime | p || m } = { p e. Prime | p || k } )
51 prmex 
 |-  Prime e. _V
52 51 rabex 
 |-  { p e. Prime | p || k } e. _V
53 50 41 52 fvmpt 
 |-  ( k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } -> ( ( m e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } |-> { p e. Prime | p || m } ) ` k ) = { p e. Prime | p || k } )
54 53 adantl 
 |-  ( ( N e. NN /\ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ) -> ( ( m e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } |-> { p e. Prime | p || m } ) ` k ) = { p e. Prime | p || k } )
55 neg1cn 
 |-  -u 1 e. CC
56 prmdvdsfi 
 |-  ( N e. NN -> { p e. Prime | p || N } e. Fin )
57 elpwi 
 |-  ( x e. ~P { p e. Prime | p || N } -> x C_ { p e. Prime | p || N } )
58 ssfi 
 |-  ( ( { p e. Prime | p || N } e. Fin /\ x C_ { p e. Prime | p || N } ) -> x e. Fin )
59 56 57 58 syl2an 
 |-  ( ( N e. NN /\ x e. ~P { p e. Prime | p || N } ) -> x e. Fin )
60 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
61 59 60 syl 
 |-  ( ( N e. NN /\ x e. ~P { p e. Prime | p || N } ) -> ( # ` x ) e. NN0 )
62 expcl 
 |-  ( ( -u 1 e. CC /\ ( # ` x ) e. NN0 ) -> ( -u 1 ^ ( # ` x ) ) e. CC )
63 55 61 62 sylancr 
 |-  ( ( N e. NN /\ x e. ~P { p e. Prime | p || N } ) -> ( -u 1 ^ ( # ` x ) ) e. CC )
64 38 39 48 54 63 fsumf1o 
 |-  ( N e. NN -> sum_ x e. ~P { p e. Prime | p || N } ( -u 1 ^ ( # ` x ) ) = sum_ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
65 fzfid 
 |-  ( N e. NN -> ( 0 ... ( # ` { p e. Prime | p || N } ) ) e. Fin )
66 56 adantr 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> { p e. Prime | p || N } e. Fin )
67 pwfi 
 |-  ( { p e. Prime | p || N } e. Fin <-> ~P { p e. Prime | p || N } e. Fin )
68 66 67 sylib 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> ~P { p e. Prime | p || N } e. Fin )
69 ssrab2 
 |-  { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } C_ ~P { p e. Prime | p || N }
70 ssfi 
 |-  ( ( ~P { p e. Prime | p || N } e. Fin /\ { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } C_ ~P { p e. Prime | p || N } ) -> { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } e. Fin )
71 68 69 70 sylancl 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } e. Fin )
72 simprr 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } )
73 fveqeq2 
 |-  ( s = x -> ( ( # ` s ) = z <-> ( # ` x ) = z ) )
74 73 elrab 
 |-  ( x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } <-> ( x e. ~P { p e. Prime | p || N } /\ ( # ` x ) = z ) )
75 74 simprbi 
 |-  ( x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } -> ( # ` x ) = z )
76 72 75 syl 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> ( # ` x ) = z )
77 76 ralrimivva 
 |-  ( N e. NN -> A. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) A. x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( # ` x ) = z )
78 invdisj 
 |-  ( A. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) A. x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( # ` x ) = z -> Disj_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } )
79 77 78 syl 
 |-  ( N e. NN -> Disj_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } )
80 56 adantr 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> { p e. Prime | p || N } e. Fin )
81 69 72 sselid 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> x e. ~P { p e. Prime | p || N } )
82 81 57 syl 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> x C_ { p e. Prime | p || N } )
83 80 82 ssfid 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> x e. Fin )
84 83 60 syl 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> ( # ` x ) e. NN0 )
85 55 84 62 sylancr 
 |-  ( ( N e. NN /\ ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) ) -> ( -u 1 ^ ( # ` x ) ) e. CC )
86 65 71 79 85 fsumiun 
 |-  ( N e. NN -> sum_ x e. U_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) = sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) )
87 iunrab 
 |-  U_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } = { s e. ~P { p e. Prime | p || N } | E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z }
88 56 adantr 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> { p e. Prime | p || N } e. Fin )
89 elpwi 
 |-  ( s e. ~P { p e. Prime | p || N } -> s C_ { p e. Prime | p || N } )
90 89 adantl 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> s C_ { p e. Prime | p || N } )
91 ssdomg 
 |-  ( { p e. Prime | p || N } e. Fin -> ( s C_ { p e. Prime | p || N } -> s ~<_ { p e. Prime | p || N } ) )
92 88 90 91 sylc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> s ~<_ { p e. Prime | p || N } )
93 ssfi 
 |-  ( ( { p e. Prime | p || N } e. Fin /\ s C_ { p e. Prime | p || N } ) -> s e. Fin )
94 56 89 93 syl2an 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> s e. Fin )
95 hashdom 
 |-  ( ( s e. Fin /\ { p e. Prime | p || N } e. Fin ) -> ( ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) <-> s ~<_ { p e. Prime | p || N } ) )
96 94 88 95 syl2anc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) <-> s ~<_ { p e. Prime | p || N } ) )
97 92 96 mpbird 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) )
98 hashcl 
 |-  ( s e. Fin -> ( # ` s ) e. NN0 )
99 94 98 syl 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) e. NN0 )
100 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
101 99 100 eleqtrdi 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) e. ( ZZ>= ` 0 ) )
102 hashcl 
 |-  ( { p e. Prime | p || N } e. Fin -> ( # ` { p e. Prime | p || N } ) e. NN0 )
103 56 102 syl 
 |-  ( N e. NN -> ( # ` { p e. Prime | p || N } ) e. NN0 )
104 103 adantr 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` { p e. Prime | p || N } ) e. NN0 )
105 104 nn0zd 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` { p e. Prime | p || N } ) e. ZZ )
106 elfz5 
 |-  ( ( ( # ` s ) e. ( ZZ>= ` 0 ) /\ ( # ` { p e. Prime | p || N } ) e. ZZ ) -> ( ( # ` s ) e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) <-> ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) ) )
107 101 105 106 syl2anc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( ( # ` s ) e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) <-> ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) ) )
108 97 107 mpbird 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) )
109 eqidd 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) = ( # ` s ) )
110 eqeq2 
 |-  ( z = ( # ` s ) -> ( ( # ` s ) = z <-> ( # ` s ) = ( # ` s ) ) )
111 110 rspcev 
 |-  ( ( ( # ` s ) e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ ( # ` s ) = ( # ` s ) ) -> E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
112 108 109 111 syl2anc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
113 112 ralrimiva 
 |-  ( N e. NN -> A. s e. ~P { p e. Prime | p || N } E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
114 rabid2 
 |-  ( ~P { p e. Prime | p || N } = { s e. ~P { p e. Prime | p || N } | E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z } <-> A. s e. ~P { p e. Prime | p || N } E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
115 113 114 sylibr 
 |-  ( N e. NN -> ~P { p e. Prime | p || N } = { s e. ~P { p e. Prime | p || N } | E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z } )
116 87 115 eqtr4id 
 |-  ( N e. NN -> U_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } = ~P { p e. Prime | p || N } )
117 116 sumeq1d 
 |-  ( N e. NN -> sum_ x e. U_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) = sum_ x e. ~P { p e. Prime | p || N } ( -u 1 ^ ( # ` x ) ) )
118 elfznn0 
 |-  ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) -> z e. NN0 )
119 118 adantl 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> z e. NN0 )
120 expcl 
 |-  ( ( -u 1 e. CC /\ z e. NN0 ) -> ( -u 1 ^ z ) e. CC )
121 55 119 120 sylancr 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> ( -u 1 ^ z ) e. CC )
122 fsumconst 
 |-  ( ( { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } e. Fin /\ ( -u 1 ^ z ) e. CC ) -> sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ z ) = ( ( # ` { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) x. ( -u 1 ^ z ) ) )
123 71 121 122 syl2anc 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ z ) = ( ( # ` { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) x. ( -u 1 ^ z ) ) )
124 75 adantl 
 |-  ( ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) -> ( # ` x ) = z )
125 124 oveq2d 
 |-  ( ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) /\ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) -> ( -u 1 ^ ( # ` x ) ) = ( -u 1 ^ z ) )
126 125 sumeq2dv 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) = sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ z ) )
127 elfzelz 
 |-  ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) -> z e. ZZ )
128 hashbc 
 |-  ( ( { p e. Prime | p || N } e. Fin /\ z e. ZZ ) -> ( ( # ` { p e. Prime | p || N } ) _C z ) = ( # ` { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) )
129 56 127 128 syl2an 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> ( ( # ` { p e. Prime | p || N } ) _C z ) = ( # ` { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) )
130 129 oveq1d 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> ( ( ( # ` { p e. Prime | p || N } ) _C z ) x. ( -u 1 ^ z ) ) = ( ( # ` { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ) x. ( -u 1 ^ z ) ) )
131 123 126 130 3eqtr4d 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) = ( ( ( # ` { p e. Prime | p || N } ) _C z ) x. ( -u 1 ^ z ) ) )
132 131 sumeq2dv 
 |-  ( N e. NN -> sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) = sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( ( ( # ` { p e. Prime | p || N } ) _C z ) x. ( -u 1 ^ z ) ) )
133 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
134 133 oveq1i 
 |-  ( ( 1 + -u 1 ) ^ ( # ` { p e. Prime | p || N } ) ) = ( 0 ^ ( # ` { p e. Prime | p || N } ) )
135 binom1p 
 |-  ( ( -u 1 e. CC /\ ( # ` { p e. Prime | p || N } ) e. NN0 ) -> ( ( 1 + -u 1 ) ^ ( # ` { p e. Prime | p || N } ) ) = sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( ( ( # ` { p e. Prime | p || N } ) _C z ) x. ( -u 1 ^ z ) ) )
136 55 103 135 sylancr 
 |-  ( N e. NN -> ( ( 1 + -u 1 ) ^ ( # ` { p e. Prime | p || N } ) ) = sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( ( ( # ` { p e. Prime | p || N } ) _C z ) x. ( -u 1 ^ z ) ) )
137 134 136 eqtr3id 
 |-  ( N e. NN -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( ( ( # ` { p e. Prime | p || N } ) _C z ) x. ( -u 1 ^ z ) ) )
138 eqeq2 
 |-  ( 1 = if ( N = 1 , 1 , 0 ) -> ( ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = 1 <-> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = if ( N = 1 , 1 , 0 ) ) )
139 eqeq2 
 |-  ( 0 = if ( N = 1 , 1 , 0 ) -> ( ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = 0 <-> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = if ( N = 1 , 1 , 0 ) ) )
140 nprmdvds1 
 |-  ( p e. Prime -> -. p || 1 )
141 simpr 
 |-  ( ( N e. NN /\ N = 1 ) -> N = 1 )
142 141 breq2d 
 |-  ( ( N e. NN /\ N = 1 ) -> ( p || N <-> p || 1 ) )
143 142 notbid 
 |-  ( ( N e. NN /\ N = 1 ) -> ( -. p || N <-> -. p || 1 ) )
144 140 143 syl5ibr 
 |-  ( ( N e. NN /\ N = 1 ) -> ( p e. Prime -> -. p || N ) )
145 144 ralrimiv 
 |-  ( ( N e. NN /\ N = 1 ) -> A. p e. Prime -. p || N )
146 rabeq0 
 |-  ( { p e. Prime | p || N } = (/) <-> A. p e. Prime -. p || N )
147 145 146 sylibr 
 |-  ( ( N e. NN /\ N = 1 ) -> { p e. Prime | p || N } = (/) )
148 147 fveq2d 
 |-  ( ( N e. NN /\ N = 1 ) -> ( # ` { p e. Prime | p || N } ) = ( # ` (/) ) )
149 hash0 
 |-  ( # ` (/) ) = 0
150 148 149 eqtrdi 
 |-  ( ( N e. NN /\ N = 1 ) -> ( # ` { p e. Prime | p || N } ) = 0 )
151 150 oveq2d 
 |-  ( ( N e. NN /\ N = 1 ) -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = ( 0 ^ 0 ) )
152 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
153 151 152 eqtrdi 
 |-  ( ( N e. NN /\ N = 1 ) -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = 1 )
154 df-ne 
 |-  ( N =/= 1 <-> -. N = 1 )
155 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
156 155 biimpri 
 |-  ( ( N e. NN /\ N =/= 1 ) -> N e. ( ZZ>= ` 2 ) )
157 154 156 sylan2br 
 |-  ( ( N e. NN /\ -. N = 1 ) -> N e. ( ZZ>= ` 2 ) )
158 exprmfct 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. p e. Prime p || N )
159 157 158 syl 
 |-  ( ( N e. NN /\ -. N = 1 ) -> E. p e. Prime p || N )
160 rabn0 
 |-  ( { p e. Prime | p || N } =/= (/) <-> E. p e. Prime p || N )
161 159 160 sylibr 
 |-  ( ( N e. NN /\ -. N = 1 ) -> { p e. Prime | p || N } =/= (/) )
162 56 adantr 
 |-  ( ( N e. NN /\ -. N = 1 ) -> { p e. Prime | p || N } e. Fin )
163 hashnncl 
 |-  ( { p e. Prime | p || N } e. Fin -> ( ( # ` { p e. Prime | p || N } ) e. NN <-> { p e. Prime | p || N } =/= (/) ) )
164 162 163 syl 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( ( # ` { p e. Prime | p || N } ) e. NN <-> { p e. Prime | p || N } =/= (/) ) )
165 161 164 mpbird 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( # ` { p e. Prime | p || N } ) e. NN )
166 165 0expd 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = 0 )
167 138 139 153 166 ifbothda 
 |-  ( N e. NN -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = if ( N = 1 , 1 , 0 ) )
168 132 137 167 3eqtr2d 
 |-  ( N e. NN -> sum_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) sum_ x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } ( -u 1 ^ ( # ` x ) ) = if ( N = 1 , 1 , 0 ) )
169 86 117 168 3eqtr3d 
 |-  ( N e. NN -> sum_ x e. ~P { p e. Prime | p || N } ( -u 1 ^ ( # ` x ) ) = if ( N = 1 , 1 , 0 ) )
170 64 169 eqtr3d 
 |-  ( N e. NN -> sum_ k e. { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) = if ( N = 1 , 1 , 0 ) )
171 10 36 170 3eqtr3d 
 |-  ( N e. NN -> sum_ k e. { n e. NN | n || N } ( mmu ` k ) = if ( N = 1 , 1 , 0 ) )