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