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 ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ( μ ‘ 𝑘 ) = if ( 𝑁 = 1 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑛 = 𝑘 → ( μ ‘ 𝑛 ) = ( μ ‘ 𝑘 ) )
2 1 neeq1d ( 𝑛 = 𝑘 → ( ( μ ‘ 𝑛 ) ≠ 0 ↔ ( μ ‘ 𝑘 ) ≠ 0 ) )
3 breq1 ( 𝑛 = 𝑘 → ( 𝑛𝑁𝑘𝑁 ) )
4 2 3 anbi12d ( 𝑛 = 𝑘 → ( ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) ↔ ( ( μ ‘ 𝑘 ) ≠ 0 ∧ 𝑘𝑁 ) ) )
5 4 elrab ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ↔ ( 𝑘 ∈ ℕ ∧ ( ( μ ‘ 𝑘 ) ≠ 0 ∧ 𝑘𝑁 ) ) )
6 muval2 ( ( 𝑘 ∈ ℕ ∧ ( μ ‘ 𝑘 ) ≠ 0 ) → ( μ ‘ 𝑘 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
7 6 adantrr ( ( 𝑘 ∈ ℕ ∧ ( ( μ ‘ 𝑘 ) ≠ 0 ∧ 𝑘𝑁 ) ) → ( μ ‘ 𝑘 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
8 5 7 sylbi ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } → ( μ ‘ 𝑘 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
9 8 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → ( μ ‘ 𝑘 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
10 9 sumeq2dv ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ( μ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
11 simpr ( ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) → 𝑛𝑁 )
12 11 a1i ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) → 𝑛𝑁 ) )
13 12 ss2rabdv ( 𝑁 ∈ ℕ → { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } )
14 ssrab2 { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ⊆ ℕ
15 simpr ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } )
16 14 15 sselid ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → 𝑘 ∈ ℕ )
17 mucl ( 𝑘 ∈ ℕ → ( μ ‘ 𝑘 ) ∈ ℤ )
18 16 17 syl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → ( μ ‘ 𝑘 ) ∈ ℤ )
19 18 zcnd ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → ( μ ‘ 𝑘 ) ∈ ℂ )
20 difrab ( { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ∖ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) = { 𝑛 ∈ ℕ ∣ ( 𝑛𝑁 ∧ ¬ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) ) }
21 pm3.21 ( 𝑛𝑁 → ( ( μ ‘ 𝑛 ) ≠ 0 → ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) ) )
22 21 necon1bd ( 𝑛𝑁 → ( ¬ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) → ( μ ‘ 𝑛 ) = 0 ) )
23 22 imp ( ( 𝑛𝑁 ∧ ¬ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) ) → ( μ ‘ 𝑛 ) = 0 )
24 23 a1i ( 𝑛 ∈ ℕ → ( ( 𝑛𝑁 ∧ ¬ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) ) → ( μ ‘ 𝑛 ) = 0 ) )
25 24 ss2rabi { 𝑛 ∈ ℕ ∣ ( 𝑛𝑁 ∧ ¬ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) ) } ⊆ { 𝑛 ∈ ℕ ∣ ( μ ‘ 𝑛 ) = 0 }
26 20 25 eqsstri ( { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ∖ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) ⊆ { 𝑛 ∈ ℕ ∣ ( μ ‘ 𝑛 ) = 0 }
27 26 sseli ( 𝑘 ∈ ( { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ∖ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( μ ‘ 𝑛 ) = 0 } )
28 fveqeq2 ( 𝑛 = 𝑘 → ( ( μ ‘ 𝑛 ) = 0 ↔ ( μ ‘ 𝑘 ) = 0 ) )
29 28 elrab ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( μ ‘ 𝑛 ) = 0 } ↔ ( 𝑘 ∈ ℕ ∧ ( μ ‘ 𝑘 ) = 0 ) )
30 29 simprbi ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( μ ‘ 𝑛 ) = 0 } → ( μ ‘ 𝑘 ) = 0 )
31 27 30 syl ( 𝑘 ∈ ( { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ∖ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → ( μ ‘ 𝑘 ) = 0 )
32 31 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ∖ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) ) → ( μ ‘ 𝑘 ) = 0 )
33 fzfid ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
34 dvdsssfz1 ( 𝑁 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ⊆ ( 1 ... 𝑁 ) )
35 33 34 ssfid ( 𝑁 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ∈ Fin )
36 13 19 32 35 fsumss ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ( μ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ( μ ‘ 𝑘 ) )
37 fveq2 ( 𝑥 = { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) )
38 37 oveq2d ( 𝑥 = { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
39 35 13 ssfid ( 𝑁 ∈ ℕ → { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ∈ Fin )
40 eqid { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } = { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) }
41 eqid ( 𝑚 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ↦ { 𝑝 ∈ ℙ ∣ 𝑝𝑚 } ) = ( 𝑚 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ↦ { 𝑝 ∈ ℙ ∣ 𝑝𝑚 } )
42 oveq1 ( 𝑞 = 𝑝 → ( 𝑞 pCnt 𝑥 ) = ( 𝑝 pCnt 𝑥 ) )
43 42 cbvmptv ( 𝑞 ∈ ℙ ↦ ( 𝑞 pCnt 𝑥 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑥 ) )
44 oveq2 ( 𝑥 = 𝑚 → ( 𝑝 pCnt 𝑥 ) = ( 𝑝 pCnt 𝑚 ) )
45 44 mpteq2dv ( 𝑥 = 𝑚 → ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑥 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑚 ) ) )
46 43 45 syl5eq ( 𝑥 = 𝑚 → ( 𝑞 ∈ ℙ ↦ ( 𝑞 pCnt 𝑥 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑚 ) ) )
47 46 cbvmptv ( 𝑥 ∈ ℕ ↦ ( 𝑞 ∈ ℙ ↦ ( 𝑞 pCnt 𝑥 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑚 ) ) )
48 40 41 47 sqff1o ( 𝑁 ∈ ℕ → ( 𝑚 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ↦ { 𝑝 ∈ ℙ ∣ 𝑝𝑚 } ) : { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } –1-1-onto→ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
49 breq2 ( 𝑚 = 𝑘 → ( 𝑝𝑚𝑝𝑘 ) )
50 49 rabbidv ( 𝑚 = 𝑘 → { 𝑝 ∈ ℙ ∣ 𝑝𝑚 } = { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } )
51 prmex ℙ ∈ V
52 51 rabex { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ∈ V
53 50 41 52 fvmpt ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } → ( ( 𝑚 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ↦ { 𝑝 ∈ ℙ ∣ 𝑝𝑚 } ) ‘ 𝑘 ) = { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } )
54 53 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ) → ( ( 𝑚 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ↦ { 𝑝 ∈ ℙ ∣ 𝑝𝑚 } ) ‘ 𝑘 ) = { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } )
55 neg1cn - 1 ∈ ℂ
56 prmdvdsfi ( 𝑁 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
57 elpwi ( 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } → 𝑥 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
58 ssfi ( ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin ∧ 𝑥 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → 𝑥 ∈ Fin )
59 56 57 58 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → 𝑥 ∈ Fin )
60 hashcl ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
61 59 60 syl ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
62 expcl ( ( - 1 ∈ ℂ ∧ ( ♯ ‘ 𝑥 ) ∈ ℕ0 ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ∈ ℂ )
63 55 61 62 sylancr ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ∈ ℂ )
64 38 39 48 54 63 fsumf1o ( 𝑁 ∈ ℕ → Σ 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) )
65 fzfid ( 𝑁 ∈ ℕ → ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∈ Fin )
66 56 adantr ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
67 pwfi ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin ↔ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
68 66 67 sylib ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
69 ssrab2 { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ⊆ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 }
70 ssfi ( ( 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin ∧ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ⊆ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ∈ Fin )
71 68 69 70 sylancl ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ∈ Fin )
72 simprr ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } )
73 fveqeq2 ( 𝑠 = 𝑥 → ( ( ♯ ‘ 𝑠 ) = 𝑧 ↔ ( ♯ ‘ 𝑥 ) = 𝑧 ) )
74 73 elrab ( 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ↔ ( 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∧ ( ♯ ‘ 𝑥 ) = 𝑧 ) )
75 74 simprbi ( 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } → ( ♯ ‘ 𝑥 ) = 𝑧 )
76 72 75 syl ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → ( ♯ ‘ 𝑥 ) = 𝑧 )
77 76 ralrimivva ( 𝑁 ∈ ℕ → ∀ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∀ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( ♯ ‘ 𝑥 ) = 𝑧 )
78 invdisj ( ∀ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∀ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( ♯ ‘ 𝑥 ) = 𝑧Disj 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } )
79 77 78 syl ( 𝑁 ∈ ℕ → Disj 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } )
80 56 adantr ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
81 69 72 sselid ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
82 81 57 syl ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → 𝑥 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
83 80 82 ssfid ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → 𝑥 ∈ Fin )
84 83 60 syl ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
85 55 84 62 sylancr ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ∈ ℂ )
86 65 71 79 85 fsumiun ( 𝑁 ∈ ℕ → Σ 𝑥 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
87 iunrab 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } = { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 }
88 56 adantr ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
89 elpwi ( 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } → 𝑠 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
90 89 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → 𝑠 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
91 ssdomg ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin → ( 𝑠 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } → 𝑠 ≼ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) )
92 88 90 91 sylc ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → 𝑠 ≼ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
93 ssfi ( ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin ∧ 𝑠 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → 𝑠 ∈ Fin )
94 56 89 93 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → 𝑠 ∈ Fin )
95 hashdom ( ( 𝑠 ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin ) → ( ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ↔ 𝑠 ≼ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) )
96 94 88 95 syl2anc ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ↔ 𝑠 ≼ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) )
97 92 96 mpbird ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) )
98 hashcl ( 𝑠 ∈ Fin → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
99 94 98 syl ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
100 nn0uz 0 = ( ℤ ‘ 0 )
101 99 100 eleqtrdi ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ 𝑠 ) ∈ ( ℤ ‘ 0 ) )
102 hashcl ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ0 )
103 56 102 syl ( 𝑁 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ0 )
104 103 adantr ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ0 )
105 104 nn0zd ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℤ )
106 elfz5 ( ( ( ♯ ‘ 𝑠 ) ∈ ( ℤ ‘ 0 ) ∧ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℤ ) → ( ( ♯ ‘ 𝑠 ) ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ↔ ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) )
107 101 105 106 syl2anc ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ( ♯ ‘ 𝑠 ) ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ↔ ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) )
108 97 107 mpbird ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ 𝑠 ) ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) )
109 eqidd ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑠 ) )
110 eqeq2 ( 𝑧 = ( ♯ ‘ 𝑠 ) → ( ( ♯ ‘ 𝑠 ) = 𝑧 ↔ ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑠 ) ) )
111 110 rspcev ( ( ( ♯ ‘ 𝑠 ) ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ∧ ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑠 ) ) → ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 )
112 108 109 111 syl2anc ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) → ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 )
113 112 ralrimiva ( 𝑁 ∈ ℕ → ∀ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 )
114 rabid2 ( 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } = { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 } ↔ ∀ 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 )
115 113 114 sylibr ( 𝑁 ∈ ℕ → 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } = { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ∃ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ♯ ‘ 𝑠 ) = 𝑧 } )
116 87 115 eqtr4id ( 𝑁 ∈ ℕ → 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } = 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } )
117 116 sumeq1d ( 𝑁 ∈ ℕ → Σ 𝑥 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = Σ 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
118 elfznn0 ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) → 𝑧 ∈ ℕ0 )
119 118 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → 𝑧 ∈ ℕ0 )
120 expcl ( ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℕ0 ) → ( - 1 ↑ 𝑧 ) ∈ ℂ )
121 55 119 120 sylancr ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → ( - 1 ↑ 𝑧 ) ∈ ℂ )
122 fsumconst ( ( { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ∈ Fin ∧ ( - 1 ↑ 𝑧 ) ∈ ℂ ) → Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ 𝑧 ) = ( ( ♯ ‘ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) · ( - 1 ↑ 𝑧 ) ) )
123 71 121 122 syl2anc ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ 𝑧 ) = ( ( ♯ ‘ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) · ( - 1 ↑ 𝑧 ) ) )
124 75 adantl ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) → ( ♯ ‘ 𝑥 ) = 𝑧 )
125 124 oveq2d ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) ∧ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) → ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( - 1 ↑ 𝑧 ) )
126 125 sumeq2dv ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ 𝑧 ) )
127 elfzelz ( 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) → 𝑧 ∈ ℤ )
128 hashbc ( ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin ∧ 𝑧 ∈ ℤ ) → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) )
129 56 127 128 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) )
130 129 oveq1d ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → ( ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) · ( - 1 ↑ 𝑧 ) ) = ( ( ♯ ‘ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ) · ( - 1 ↑ 𝑧 ) ) )
131 123 126 130 3eqtr4d ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ) → Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = ( ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) · ( - 1 ↑ 𝑧 ) ) )
132 131 sumeq2dv ( 𝑁 ∈ ℕ → Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) · ( - 1 ↑ 𝑧 ) ) )
133 1pneg1e0 ( 1 + - 1 ) = 0
134 133 oveq1i ( ( 1 + - 1 ) ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) )
135 binom1p ( ( - 1 ∈ ℂ ∧ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ0 ) → ( ( 1 + - 1 ) ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) · ( - 1 ↑ 𝑧 ) ) )
136 55 103 135 sylancr ( 𝑁 ∈ ℕ → ( ( 1 + - 1 ) ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) · ( - 1 ↑ 𝑧 ) ) )
137 134 136 eqtr3id ( 𝑁 ∈ ℕ → ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) ( ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) C 𝑧 ) · ( - 1 ↑ 𝑧 ) ) )
138 eqeq2 ( 1 = if ( 𝑁 = 1 , 1 , 0 ) → ( ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = 1 ↔ ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = if ( 𝑁 = 1 , 1 , 0 ) ) )
139 eqeq2 ( 0 = if ( 𝑁 = 1 , 1 , 0 ) → ( ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = 0 ↔ ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = if ( 𝑁 = 1 , 1 , 0 ) ) )
140 nprmdvds1 ( 𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1 )
141 simpr ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → 𝑁 = 1 )
142 141 breq2d ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( 𝑝𝑁𝑝 ∥ 1 ) )
143 142 notbid ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( ¬ 𝑝𝑁 ↔ ¬ 𝑝 ∥ 1 ) )
144 140 143 syl5ibr ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( 𝑝 ∈ ℙ → ¬ 𝑝𝑁 ) )
145 144 ralrimiv ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ∀ 𝑝 ∈ ℙ ¬ 𝑝𝑁 )
146 rabeq0 ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } = ∅ ↔ ∀ 𝑝 ∈ ℙ ¬ 𝑝𝑁 )
147 145 146 sylibr ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } = ∅ )
148 147 fveq2d ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) = ( ♯ ‘ ∅ ) )
149 hash0 ( ♯ ‘ ∅ ) = 0
150 148 149 eqtrdi ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) = 0 )
151 150 oveq2d ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = ( 0 ↑ 0 ) )
152 0exp0e1 ( 0 ↑ 0 ) = 1
153 151 152 eqtrdi ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 1 ) → ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = 1 )
154 df-ne ( 𝑁 ≠ 1 ↔ ¬ 𝑁 = 1 )
155 eluz2b3 ( 𝑁 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
156 155 biimpri ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 𝑁 ∈ ( ℤ ‘ 2 ) )
157 154 156 sylan2br ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → 𝑁 ∈ ( ℤ ‘ 2 ) )
158 exprmfct ( 𝑁 ∈ ( ℤ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝𝑁 )
159 157 158 syl ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ∃ 𝑝 ∈ ℙ 𝑝𝑁 )
160 rabn0 ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ≠ ∅ ↔ ∃ 𝑝 ∈ ℙ 𝑝𝑁 )
161 159 160 sylibr ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ≠ ∅ )
162 56 adantr ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin )
163 hashnncl ( { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∈ Fin → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ ↔ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ≠ ∅ ) )
164 162 163 syl ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ ↔ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ≠ ∅ ) )
165 161 164 mpbird ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ∈ ℕ )
166 165 0expd ( ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1 ) → ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = 0 )
167 138 139 153 166 ifbothda ( 𝑁 ∈ ℕ → ( 0 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) = if ( 𝑁 = 1 , 1 , 0 ) )
168 132 137 167 3eqtr2d ( 𝑁 ∈ ℕ → Σ 𝑧 ∈ ( 0 ... ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ) ) Σ 𝑥 ∈ { 𝑠 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ∣ ( ♯ ‘ 𝑠 ) = 𝑧 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = if ( 𝑁 = 1 , 1 , 0 ) )
169 86 117 168 3eqtr3d ( 𝑁 ∈ ℕ → Σ 𝑥 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝𝑁 } ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) = if ( 𝑁 = 1 , 1 , 0 ) )
170 64 169 eqtr3d ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛𝑁 ) } ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝑘 } ) ) = if ( 𝑁 = 1 , 1 , 0 ) )
171 10 36 170 3eqtr3d ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛𝑁 } ( μ ‘ 𝑘 ) = if ( 𝑁 = 1 , 1 , 0 ) )