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 eqtrid ⊢ ( 𝑥 = 𝑚 → ( 𝑞 ∈ ℙ ↦ ( 𝑞 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 ) )