This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dvdsfi 
 |-  ( N e. NN -> { n e. NN | n || N } e. Fin )
34 13 19 32 33 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 ) )
35 fveq2 
 |-  ( x = { p e. Prime | p || k } -> ( # ` x ) = ( # ` { p e. Prime | p || k } ) )
36 35 oveq2d 
 |-  ( x = { p e. Prime | p || k } -> ( -u 1 ^ ( # ` x ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || k } ) ) )
37 33 13 ssfid 
 |-  ( N e. NN -> { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } e. Fin )
38 eqid 
 |-  { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) } = { n e. NN | ( ( mmu ` n ) =/= 0 /\ n || N ) }
39 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 } )
40 oveq1 
 |-  ( q = p -> ( q pCnt x ) = ( p pCnt x ) )
41 40 cbvmptv 
 |-  ( q e. Prime |-> ( q pCnt x ) ) = ( p e. Prime |-> ( p pCnt x ) )
42 oveq2 
 |-  ( x = m -> ( p pCnt x ) = ( p pCnt m ) )
43 42 mpteq2dv 
 |-  ( x = m -> ( p e. Prime |-> ( p pCnt x ) ) = ( p e. Prime |-> ( p pCnt m ) ) )
44 41 43 eqtrid 
 |-  ( x = m -> ( q e. Prime |-> ( q pCnt x ) ) = ( p e. Prime |-> ( p pCnt m ) ) )
45 44 cbvmptv 
 |-  ( x e. NN |-> ( q e. Prime |-> ( q pCnt x ) ) ) = ( m e. NN |-> ( p e. Prime |-> ( p pCnt m ) ) )
46 38 39 45 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 } )
47 breq2 
 |-  ( m = k -> ( p || m <-> p || k ) )
48 47 rabbidv 
 |-  ( m = k -> { p e. Prime | p || m } = { p e. Prime | p || k } )
49 prmex 
 |-  Prime e. _V
50 49 rabex 
 |-  { p e. Prime | p || k } e. _V
51 48 39 50 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 } )
52 51 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 } )
53 neg1cn 
 |-  -u 1 e. CC
54 prmdvdsfi 
 |-  ( N e. NN -> { p e. Prime | p || N } e. Fin )
55 elpwi 
 |-  ( x e. ~P { p e. Prime | p || N } -> x C_ { p e. Prime | p || N } )
56 ssfi 
 |-  ( ( { p e. Prime | p || N } e. Fin /\ x C_ { p e. Prime | p || N } ) -> x e. Fin )
57 54 55 56 syl2an 
 |-  ( ( N e. NN /\ x e. ~P { p e. Prime | p || N } ) -> x e. Fin )
58 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
59 57 58 syl 
 |-  ( ( N e. NN /\ x e. ~P { p e. Prime | p || N } ) -> ( # ` x ) e. NN0 )
60 expcl 
 |-  ( ( -u 1 e. CC /\ ( # ` x ) e. NN0 ) -> ( -u 1 ^ ( # ` x ) ) e. CC )
61 53 59 60 sylancr 
 |-  ( ( N e. NN /\ x e. ~P { p e. Prime | p || N } ) -> ( -u 1 ^ ( # ` x ) ) e. CC )
62 36 37 46 52 61 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 } ) ) )
63 fzfid 
 |-  ( N e. NN -> ( 0 ... ( # ` { p e. Prime | p || N } ) ) e. Fin )
64 54 adantr 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> { p e. Prime | p || N } e. Fin )
65 pwfi 
 |-  ( { p e. Prime | p || N } e. Fin <-> ~P { p e. Prime | p || N } e. Fin )
66 64 65 sylib 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> ~P { p e. Prime | p || N } e. Fin )
67 ssrab2 
 |-  { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } C_ ~P { p e. Prime | p || N }
68 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 )
69 66 67 68 sylancl 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } e. Fin )
70 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 } )
71 fveqeq2 
 |-  ( s = x -> ( ( # ` s ) = z <-> ( # ` x ) = z ) )
72 71 elrab 
 |-  ( x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } <-> ( x e. ~P { p e. Prime | p || N } /\ ( # ` x ) = z ) )
73 72 simprbi 
 |-  ( x e. { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } -> ( # ` x ) = z )
74 70 73 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 )
75 74 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 )
76 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 } )
77 75 76 syl 
 |-  ( N e. NN -> Disj_ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) { s e. ~P { p e. Prime | p || N } | ( # ` s ) = z } )
78 54 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 )
79 67 70 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 } )
80 79 55 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 } )
81 78 80 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 )
82 81 58 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 )
83 53 82 60 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 )
84 63 69 77 83 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 ) ) )
85 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 }
86 54 adantr 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> { p e. Prime | p || N } e. Fin )
87 elpwi 
 |-  ( s e. ~P { p e. Prime | p || N } -> s C_ { p e. Prime | p || N } )
88 87 adantl 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> s C_ { p e. Prime | p || N } )
89 ssdomg 
 |-  ( { p e. Prime | p || N } e. Fin -> ( s C_ { p e. Prime | p || N } -> s ~<_ { p e. Prime | p || N } ) )
90 86 88 89 sylc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> s ~<_ { p e. Prime | p || N } )
91 ssfi 
 |-  ( ( { p e. Prime | p || N } e. Fin /\ s C_ { p e. Prime | p || N } ) -> s e. Fin )
92 54 87 91 syl2an 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> s e. Fin )
93 hashdom 
 |-  ( ( s e. Fin /\ { p e. Prime | p || N } e. Fin ) -> ( ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) <-> s ~<_ { p e. Prime | p || N } ) )
94 92 86 93 syl2anc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) <-> s ~<_ { p e. Prime | p || N } ) )
95 90 94 mpbird 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) <_ ( # ` { p e. Prime | p || N } ) )
96 hashcl 
 |-  ( s e. Fin -> ( # ` s ) e. NN0 )
97 92 96 syl 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) e. NN0 )
98 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
99 97 98 eleqtrdi 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) e. ( ZZ>= ` 0 ) )
100 hashcl 
 |-  ( { p e. Prime | p || N } e. Fin -> ( # ` { p e. Prime | p || N } ) e. NN0 )
101 54 100 syl 
 |-  ( N e. NN -> ( # ` { p e. Prime | p || N } ) e. NN0 )
102 101 adantr 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` { p e. Prime | p || N } ) e. NN0 )
103 102 nn0zd 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` { p e. Prime | p || N } ) e. ZZ )
104 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 } ) ) )
105 99 103 104 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 } ) ) )
106 95 105 mpbird 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) )
107 eqidd 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> ( # ` s ) = ( # ` s ) )
108 eqeq2 
 |-  ( z = ( # ` s ) -> ( ( # ` s ) = z <-> ( # ` s ) = ( # ` s ) ) )
109 108 rspcev 
 |-  ( ( ( # ` s ) e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) /\ ( # ` s ) = ( # ` s ) ) -> E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
110 106 107 109 syl2anc 
 |-  ( ( N e. NN /\ s e. ~P { p e. Prime | p || N } ) -> E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
111 110 ralrimiva 
 |-  ( N e. NN -> A. s e. ~P { p e. Prime | p || N } E. z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ( # ` s ) = z )
112 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 )
113 111 112 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 } )
114 85 113 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 } )
115 114 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 ) ) )
116 elfznn0 
 |-  ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) -> z e. NN0 )
117 116 adantl 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> z e. NN0 )
118 expcl 
 |-  ( ( -u 1 e. CC /\ z e. NN0 ) -> ( -u 1 ^ z ) e. CC )
119 53 117 118 sylancr 
 |-  ( ( N e. NN /\ z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) ) -> ( -u 1 ^ z ) e. CC )
120 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 ) ) )
121 69 119 120 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 ) ) )
122 73 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 )
123 122 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 ) )
124 123 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 ) )
125 elfzelz 
 |-  ( z e. ( 0 ... ( # ` { p e. Prime | p || N } ) ) -> z e. ZZ )
126 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 } ) )
127 54 125 126 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 } ) )
128 127 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 ) ) )
129 121 124 128 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 ) ) )
130 129 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 ) ) )
131 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
132 131 oveq1i 
 |-  ( ( 1 + -u 1 ) ^ ( # ` { p e. Prime | p || N } ) ) = ( 0 ^ ( # ` { p e. Prime | p || N } ) )
133 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 ) ) )
134 53 101 133 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 ) ) )
135 132 134 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 ) ) )
136 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 ) ) )
137 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 ) ) )
138 nprmdvds1 
 |-  ( p e. Prime -> -. p || 1 )
139 simpr 
 |-  ( ( N e. NN /\ N = 1 ) -> N = 1 )
140 139 breq2d 
 |-  ( ( N e. NN /\ N = 1 ) -> ( p || N <-> p || 1 ) )
141 140 notbid 
 |-  ( ( N e. NN /\ N = 1 ) -> ( -. p || N <-> -. p || 1 ) )
142 138 141 imbitrrid 
 |-  ( ( N e. NN /\ N = 1 ) -> ( p e. Prime -> -. p || N ) )
143 142 ralrimiv 
 |-  ( ( N e. NN /\ N = 1 ) -> A. p e. Prime -. p || N )
144 rabeq0 
 |-  ( { p e. Prime | p || N } = (/) <-> A. p e. Prime -. p || N )
145 143 144 sylibr 
 |-  ( ( N e. NN /\ N = 1 ) -> { p e. Prime | p || N } = (/) )
146 145 fveq2d 
 |-  ( ( N e. NN /\ N = 1 ) -> ( # ` { p e. Prime | p || N } ) = ( # ` (/) ) )
147 hash0 
 |-  ( # ` (/) ) = 0
148 146 147 eqtrdi 
 |-  ( ( N e. NN /\ N = 1 ) -> ( # ` { p e. Prime | p || N } ) = 0 )
149 148 oveq2d 
 |-  ( ( N e. NN /\ N = 1 ) -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = ( 0 ^ 0 ) )
150 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
151 149 150 eqtrdi 
 |-  ( ( N e. NN /\ N = 1 ) -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = 1 )
152 df-ne 
 |-  ( N =/= 1 <-> -. N = 1 )
153 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
154 153 biimpri 
 |-  ( ( N e. NN /\ N =/= 1 ) -> N e. ( ZZ>= ` 2 ) )
155 152 154 sylan2br 
 |-  ( ( N e. NN /\ -. N = 1 ) -> N e. ( ZZ>= ` 2 ) )
156 exprmfct 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. p e. Prime p || N )
157 155 156 syl 
 |-  ( ( N e. NN /\ -. N = 1 ) -> E. p e. Prime p || N )
158 rabn0 
 |-  ( { p e. Prime | p || N } =/= (/) <-> E. p e. Prime p || N )
159 157 158 sylibr 
 |-  ( ( N e. NN /\ -. N = 1 ) -> { p e. Prime | p || N } =/= (/) )
160 54 adantr 
 |-  ( ( N e. NN /\ -. N = 1 ) -> { p e. Prime | p || N } e. Fin )
161 hashnncl 
 |-  ( { p e. Prime | p || N } e. Fin -> ( ( # ` { p e. Prime | p || N } ) e. NN <-> { p e. Prime | p || N } =/= (/) ) )
162 160 161 syl 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( ( # ` { p e. Prime | p || N } ) e. NN <-> { p e. Prime | p || N } =/= (/) ) )
163 159 162 mpbird 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( # ` { p e. Prime | p || N } ) e. NN )
164 163 0expd 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = 0 )
165 136 137 151 164 ifbothda 
 |-  ( N e. NN -> ( 0 ^ ( # ` { p e. Prime | p || N } ) ) = if ( N = 1 , 1 , 0 ) )
166 130 135 165 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 ) )
167 84 115 166 3eqtr3d 
 |-  ( N e. NN -> sum_ x e. ~P { p e. Prime | p || N } ( -u 1 ^ ( # ` x ) ) = if ( N = 1 , 1 , 0 ) )
168 62 167 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 ) )
169 10 34 168 3eqtr3d 
 |-  ( N e. NN -> sum_ k e. { n e. NN | n || N } ( mmu ` k ) = if ( N = 1 , 1 , 0 ) )