MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  musum Structured version   Visualization version   GIF version

Theorem musum 25701
Description: The sum of the Möbius function over the divisors of 𝑁 gives one if 𝑁 = 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 25703. (Contributed by Mario Carneiro, 2-Jul-2015.)
Assertion
Ref Expression
musum (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0))
Distinct variable group:   𝑘,𝑛,𝑁

Proof of Theorem musum
Dummy variables 𝑚 𝑝 𝑞 𝑠 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6669 . . . . . . . 8 (𝑛 = 𝑘 → (μ‘𝑛) = (μ‘𝑘))
21neeq1d 3080 . . . . . . 7 (𝑛 = 𝑘 → ((μ‘𝑛) ≠ 0 ↔ (μ‘𝑘) ≠ 0))
3 breq1 5066 . . . . . . 7 (𝑛 = 𝑘 → (𝑛𝑁𝑘𝑁))
42, 3anbi12d 630 . . . . . 6 (𝑛 = 𝑘 → (((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁) ↔ ((μ‘𝑘) ≠ 0 ∧ 𝑘𝑁)))
54elrab 3684 . . . . 5 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ↔ (𝑘 ∈ ℕ ∧ ((μ‘𝑘) ≠ 0 ∧ 𝑘𝑁)))
6 muval2 25644 . . . . . 6 ((𝑘 ∈ ℕ ∧ (μ‘𝑘) ≠ 0) → (μ‘𝑘) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
76adantrr 713 . . . . 5 ((𝑘 ∈ ℕ ∧ ((μ‘𝑘) ≠ 0 ∧ 𝑘𝑁)) → (μ‘𝑘) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
85, 7sylbi 218 . . . 4 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} → (μ‘𝑘) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
98adantl 482 . . 3 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → (μ‘𝑘) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
109sumeq2dv 15055 . 2 (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} (μ‘𝑘) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
11 simpr 485 . . . . 5 (((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁) → 𝑛𝑁)
1211a1i 11 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁) → 𝑛𝑁))
1312ss2rabdv 4056 . . 3 (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑁})
14 ssrab2 4060 . . . . . 6 {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ⊆ ℕ
15 simpr 485 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)})
1614, 15sseldi 3969 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → 𝑘 ∈ ℕ)
17 mucl 25651 . . . . 5 (𝑘 ∈ ℕ → (μ‘𝑘) ∈ ℤ)
1816, 17syl 17 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → (μ‘𝑘) ∈ ℤ)
1918zcnd 12082 . . 3 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → (μ‘𝑘) ∈ ℂ)
20 difrab 4281 . . . . . . 7 ({𝑛 ∈ ℕ ∣ 𝑛𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) = {𝑛 ∈ ℕ ∣ (𝑛𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁))}
21 pm3.21 472 . . . . . . . . . . 11 (𝑛𝑁 → ((μ‘𝑛) ≠ 0 → ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
2221necon1bd 3039 . . . . . . . . . 10 (𝑛𝑁 → (¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁) → (μ‘𝑛) = 0))
2322imp 407 . . . . . . . . 9 ((𝑛𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)) → (μ‘𝑛) = 0)
2423a1i 11 . . . . . . . 8 (𝑛 ∈ ℕ → ((𝑛𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)) → (μ‘𝑛) = 0))
2524ss2rabi 4057 . . . . . . 7 {𝑛 ∈ ℕ ∣ (𝑛𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁))} ⊆ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0}
2620, 25eqsstri 4005 . . . . . 6 ({𝑛 ∈ ℕ ∣ 𝑛𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) ⊆ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0}
2726sseli 3967 . . . . 5 (𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0})
28 fveqeq2 6678 . . . . . . 7 (𝑛 = 𝑘 → ((μ‘𝑛) = 0 ↔ (μ‘𝑘) = 0))
2928elrab 3684 . . . . . 6 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} ↔ (𝑘 ∈ ℕ ∧ (μ‘𝑘) = 0))
3029simprbi 497 . . . . 5 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} → (μ‘𝑘) = 0)
3127, 30syl 17 . . . 4 (𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → (μ‘𝑘) = 0)
3231adantl 482 . . 3 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)})) → (μ‘𝑘) = 0)
33 fzfid 13336 . . . 4 (𝑁 ∈ ℕ → (1...𝑁) ∈ Fin)
34 dvdsssfz1 15663 . . . 4 (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛𝑁} ⊆ (1...𝑁))
3533, 34ssfid 8735 . . 3 (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛𝑁} ∈ Fin)
3613, 19, 32, 35fsumss 15077 . 2 (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} (μ‘𝑘) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛𝑁} (μ‘𝑘))
37 fveq2 6669 . . . . 5 (𝑥 = {𝑝 ∈ ℙ ∣ 𝑝𝑘} → (♯‘𝑥) = (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘}))
3837oveq2d 7166 . . . 4 (𝑥 = {𝑝 ∈ ℙ ∣ 𝑝𝑘} → (-1↑(♯‘𝑥)) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
3935, 13ssfid 8735 . . . 4 (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ∈ Fin)
40 eqid 2826 . . . . 5 {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} = {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}
41 eqid 2826 . . . . 5 (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑚}) = (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑚})
42 oveq1 7157 . . . . . . . 8 (𝑞 = 𝑝 → (𝑞 pCnt 𝑥) = (𝑝 pCnt 𝑥))
4342cbvmptv 5166 . . . . . . 7 (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑥))
44 oveq2 7158 . . . . . . . 8 (𝑥 = 𝑚 → (𝑝 pCnt 𝑥) = (𝑝 pCnt 𝑚))
4544mpteq2dv 5159 . . . . . . 7 (𝑥 = 𝑚 → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚)))
4643, 45syl5eq 2873 . . . . . 6 (𝑥 = 𝑚 → (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚)))
4746cbvmptv 5166 . . . . 5 (𝑥 ∈ ℕ ↦ (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥))) = (𝑚 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚)))
4840, 41, 47sqff1o 25692 . . . 4 (𝑁 ∈ ℕ → (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑚}):{𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}–1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
49 breq2 5067 . . . . . . 7 (𝑚 = 𝑘 → (𝑝𝑚𝑝𝑘))
5049rabbidv 3486 . . . . . 6 (𝑚 = 𝑘 → {𝑝 ∈ ℙ ∣ 𝑝𝑚} = {𝑝 ∈ ℙ ∣ 𝑝𝑘})
51 prmex 16016 . . . . . . 7 ℙ ∈ V
5251rabex 5232 . . . . . 6 {𝑝 ∈ ℙ ∣ 𝑝𝑘} ∈ V
5350, 41, 52fvmpt 6767 . . . . 5 (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} → ((𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑚})‘𝑘) = {𝑝 ∈ ℙ ∣ 𝑝𝑘})
5453adantl 482 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)}) → ((𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑚})‘𝑘) = {𝑝 ∈ ℙ ∣ 𝑝𝑘})
55 neg1cn 11745 . . . . 5 -1 ∈ ℂ
56 prmdvdsfi 25617 . . . . . . 7 (𝑁 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
57 elpwi 4554 . . . . . . 7 (𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} → 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
58 ssfi 8732 . . . . . . 7 (({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin ∧ 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑥 ∈ Fin)
5956, 57, 58syl2an 595 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑥 ∈ Fin)
60 hashcl 13712 . . . . . 6 (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ0)
6159, 60syl 17 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘𝑥) ∈ ℕ0)
62 expcl 13442 . . . . 5 ((-1 ∈ ℂ ∧ (♯‘𝑥) ∈ ℕ0) → (-1↑(♯‘𝑥)) ∈ ℂ)
6355, 61, 62sylancr 587 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (-1↑(♯‘𝑥)) ∈ ℂ)
6438, 39, 48, 54, 63fsumf1o 15075 . . 3 (𝑁 ∈ ℕ → Σ𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} (-1↑(♯‘𝑥)) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})))
65 fzfid 13336 . . . . 5 (𝑁 ∈ ℕ → (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∈ Fin)
6656adantr 481 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
67 pwfi 8813 . . . . . . 7 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin ↔ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
6866, 67sylib 219 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
69 ssrab2 4060 . . . . . 6 {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} ⊆ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}
70 ssfi 8732 . . . . . 6 ((𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin ∧ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} ⊆ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} ∈ Fin)
7168, 69, 70sylancl 586 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} ∈ Fin)
72 simprr 769 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})
73 fveqeq2 6678 . . . . . . . . . 10 (𝑠 = 𝑥 → ((♯‘𝑠) = 𝑧 ↔ (♯‘𝑥) = 𝑧))
7473elrab 3684 . . . . . . . . 9 (𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} ↔ (𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∧ (♯‘𝑥) = 𝑧))
7574simprbi 497 . . . . . . . 8 (𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} → (♯‘𝑥) = 𝑧)
7672, 75syl 17 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → (♯‘𝑥) = 𝑧)
7776ralrimivva 3196 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))∀𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (♯‘𝑥) = 𝑧)
78 invdisj 5047 . . . . . 6 (∀𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))∀𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (♯‘𝑥) = 𝑧Disj 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})
7977, 78syl 17 . . . . 5 (𝑁 ∈ ℕ → Disj 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})
8056adantr 481 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
8169, 72sseldi 3969 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
8281, 57syl 17 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
8380, 82ssfid 8735 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ∈ Fin)
8483, 60syl 17 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → (♯‘𝑥) ∈ ℕ0)
8555, 84, 62sylancr 587 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧})) → (-1↑(♯‘𝑥)) ∈ ℂ)
8665, 71, 79, 85fsumiun 15171 . . . 4 (𝑁 ∈ ℕ → Σ𝑥 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)))
8756adantr 481 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
88 elpwi 4554 . . . . . . . . . . . . 13 (𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} → 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
8988adantl 482 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
90 ssdomg 8549 . . . . . . . . . . . 12 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin → (𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁} → 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝𝑁}))
9187, 89, 90sylc 65 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
92 ssfi 8732 . . . . . . . . . . . . 13 (({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin ∧ 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑠 ∈ Fin)
9356, 88, 92syl2an 595 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑠 ∈ Fin)
94 hashdom 13735 . . . . . . . . . . . 12 ((𝑠 ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin) → ((♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ↔ 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝𝑁}))
9593, 87, 94syl2anc 584 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ↔ 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝𝑁}))
9691, 95mpbird 258 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))
97 hashcl 13712 . . . . . . . . . . . . 13 (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ0)
9893, 97syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘𝑠) ∈ ℕ0)
99 nn0uz 12274 . . . . . . . . . . . 12 0 = (ℤ‘0)
10098, 99syl6eleq 2928 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘𝑠) ∈ (ℤ‘0))
101 hashcl 13712 . . . . . . . . . . . . . 14 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ0)
10256, 101syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ0)
103102adantr 481 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ0)
104103nn0zd 12079 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℤ)
105 elfz5 12895 . . . . . . . . . . 11 (((♯‘𝑠) ∈ (ℤ‘0) ∧ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℤ) → ((♯‘𝑠) ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ↔ (♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})))
106100, 104, 105syl2anc 584 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((♯‘𝑠) ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ↔ (♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})))
10796, 106mpbird 258 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘𝑠) ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})))
108 eqidd 2827 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (♯‘𝑠) = (♯‘𝑠))
109 eqeq2 2838 . . . . . . . . . 10 (𝑧 = (♯‘𝑠) → ((♯‘𝑠) = 𝑧 ↔ (♯‘𝑠) = (♯‘𝑠)))
110109rspcev 3627 . . . . . . . . 9 (((♯‘𝑠) ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) ∧ (♯‘𝑠) = (♯‘𝑠)) → ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧)
111107, 108, 110syl2anc 584 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧)
112111ralrimiva 3187 . . . . . . 7 (𝑁 ∈ ℕ → ∀𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧)
113 rabid2 3387 . . . . . . 7 (𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧} ↔ ∀𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧)
114112, 113sylibr 235 . . . . . 6 (𝑁 ∈ ℕ → 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧})
115 iunrab 4973 . . . . . 6 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(♯‘𝑠) = 𝑧}
116114, 115syl6reqr 2880 . . . . 5 (𝑁 ∈ ℕ → 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} = 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
117116sumeq1d 15053 . . . 4 (𝑁 ∈ ℕ → Σ𝑥 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} (-1↑(♯‘𝑥)))
118 elfznn0 12995 . . . . . . . . . 10 (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑧 ∈ ℕ0)
119118adantl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → 𝑧 ∈ ℕ0)
120 expcl 13442 . . . . . . . . 9 ((-1 ∈ ℂ ∧ 𝑧 ∈ ℕ0) → (-1↑𝑧) ∈ ℂ)
12155, 119, 120sylancr 587 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → (-1↑𝑧) ∈ ℂ)
122 fsumconst 15140 . . . . . . . 8 (({𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} ∈ Fin ∧ (-1↑𝑧) ∈ ℂ) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑𝑧) = ((♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}) · (-1↑𝑧)))
12371, 121, 122syl2anc 584 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑𝑧) = ((♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}) · (-1↑𝑧)))
12475adantl 482 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}) → (♯‘𝑥) = 𝑧)
125124oveq2d 7166 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}) → (-1↑(♯‘𝑥)) = (-1↑𝑧))
126125sumeq2dv 15055 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑𝑧))
127 elfzelz 12903 . . . . . . . . 9 (𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑧 ∈ ℤ)
128 hashbc 13806 . . . . . . . . 9 (({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin ∧ 𝑧 ∈ ℤ) → ((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) = (♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}))
12956, 127, 128syl2an 595 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → ((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) = (♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}))
130129oveq1d 7165 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → (((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) · (-1↑𝑧)) = ((♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧}) · (-1↑𝑧)))
131123, 126, 1303eqtr4d 2871 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = (((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) · (-1↑𝑧)))
132131sumeq2dv 15055 . . . . 5 (𝑁 ∈ ℕ → Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) · (-1↑𝑧)))
133 1pneg1e0 11750 . . . . . . 7 (1 + -1) = 0
134133oveq1i 7160 . . . . . 6 ((1 + -1)↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))
135 binom1p 15181 . . . . . . 7 ((-1 ∈ ℂ ∧ (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ0) → ((1 + -1)↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) · (-1↑𝑧)))
13655, 102, 135sylancr 587 . . . . . 6 (𝑁 ∈ ℕ → ((1 + -1)↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) · (-1↑𝑧)))
137134, 136syl5eqr 2875 . . . . 5 (𝑁 ∈ ℕ → (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})C𝑧) · (-1↑𝑧)))
138 eqeq2 2838 . . . . . 6 (1 = if(𝑁 = 1, 1, 0) → ((0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = 1 ↔ (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = if(𝑁 = 1, 1, 0)))
139 eqeq2 2838 . . . . . 6 (0 = if(𝑁 = 1, 1, 0) → ((0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = 0 ↔ (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = if(𝑁 = 1, 1, 0)))
140 nprmdvds1 16045 . . . . . . . . . . . . 13 (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
141 simpr 485 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → 𝑁 = 1)
142141breq2d 5075 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (𝑝𝑁𝑝 ∥ 1))
143142notbid 319 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (¬ 𝑝𝑁 ↔ ¬ 𝑝 ∥ 1))
144140, 143syl5ibr 247 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (𝑝 ∈ ℙ → ¬ 𝑝𝑁))
145144ralrimiv 3186 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → ∀𝑝 ∈ ℙ ¬ 𝑝𝑁)
146 rabeq0 4342 . . . . . . . . . . 11 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} = ∅ ↔ ∀𝑝 ∈ ℙ ¬ 𝑝𝑁)
147145, 146sylibr 235 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} = ∅)
148147fveq2d 6673 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) = (♯‘∅))
149 hash0 13723 . . . . . . . . 9 (♯‘∅) = 0
150148, 149syl6eq 2877 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) = 0)
151150oveq2d 7166 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = (0↑0))
152 0exp0e1 13429 . . . . . . 7 (0↑0) = 1
153151, 152syl6eq 2877 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = 1)
154 df-ne 3022 . . . . . . . . . . 11 (𝑁 ≠ 1 ↔ ¬ 𝑁 = 1)
155 eluz2b3 12316 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
156155biimpri 229 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 𝑁 ∈ (ℤ‘2))
157154, 156sylan2br 594 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → 𝑁 ∈ (ℤ‘2))
158 exprmfct 16043 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝𝑁)
159157, 158syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → ∃𝑝 ∈ ℙ 𝑝𝑁)
160 rabn0 4343 . . . . . . . . 9 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} ≠ ∅ ↔ ∃𝑝 ∈ ℙ 𝑝𝑁)
161159, 160sylibr 235 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ≠ ∅)
16256adantr 481 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin)
163 hashnncl 13722 . . . . . . . . 9 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} ∈ Fin → ((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ ↔ {𝑝 ∈ ℙ ∣ 𝑝𝑁} ≠ ∅))
164162, 163syl 17 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → ((♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ ↔ {𝑝 ∈ ℙ ∣ 𝑝𝑁} ≠ ∅))
165161, 164mpbird 258 . . . . . . 7 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∈ ℕ)
1661650expd 13498 . . . . . 6 ((𝑁 ∈ ℕ ∧ ¬ 𝑁 = 1) → (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = 0)
167138, 139, 153, 166ifbothda 4507 . . . . 5 (𝑁 ∈ ℕ → (0↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁})) = if(𝑁 = 1, 1, 0))
168132, 137, 1673eqtr2d 2867 . . . 4 (𝑁 ∈ ℕ → Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = if(𝑁 = 1, 1, 0))
16986, 117, 1683eqtr3d 2869 . . 3 (𝑁 ∈ ℕ → Σ𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} (-1↑(♯‘𝑥)) = if(𝑁 = 1, 1, 0))
17064, 169eqtr3d 2863 . 2 (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)} (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑘})) = if(𝑁 = 1, 1, 0))
17110, 36, 1703eqtr3d 2869 1 (𝑁 ∈ ℕ → Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1530  wcel 2107  wne 3021  wral 3143  wrex 3144  {crab 3147  cdif 3937  wss 3940  c0 4295  ifcif 4470  𝒫 cpw 4542   ciun 4917  Disj wdisj 5028   class class class wbr 5063  cmpt 5143  cfv 6354  (class class class)co 7150  cdom 8501  Fincfn 8503  cc 10529  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  cle 10670  -cneg 10865  cn 11632  2c2 11686  0cn0 11891  cz 11975  cuz 12237  ...cfz 12887  cexp 13424  Ccbc 13657  chash 13685  Σcsu 15037  cdvds 15602  cprime 16010   pCnt cpc 16168  μcmu 25605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-disj 5029  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-inf 8901  df-oi 8968  df-dju 9324  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-xnn0 11962  df-z 11976  df-uz 12238  df-q 12343  df-rp 12385  df-fz 12888  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13425  df-fac 13629  df-bc 13658  df-hash 13686  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038  df-dvds 15603  df-gcd 15839  df-prm 16011  df-pc 16169  df-mu 25611
This theorem is referenced by:  musumsum  25702  muinv  25703
  Copyright terms: Public domain W3C validator