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	imbitrrid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 = 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 ) )