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 syl5eq
 |-  ( 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 ) )