| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sqff1o.2 | . 2
⊢ 𝐹 = (𝑛 ∈ 𝑆 ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) | 
| 2 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (μ‘𝑥) = (μ‘𝑛)) | 
| 3 | 2 | neeq1d 2999 | . . . . . . . . . 10
⊢ (𝑥 = 𝑛 → ((μ‘𝑥) ≠ 0 ↔ (μ‘𝑛) ≠ 0)) | 
| 4 |  | breq1 5145 | . . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁)) | 
| 5 | 3, 4 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → (((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁) ↔ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) | 
| 6 |  | sqff1o.1 | . . . . . . . . 9
⊢ 𝑆 = {𝑥 ∈ ℕ ∣ ((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁)} | 
| 7 | 5, 6 | elrab2 3694 | . . . . . . . 8
⊢ (𝑛 ∈ 𝑆 ↔ (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) | 
| 8 | 7 | simprbi 496 | . . . . . . 7
⊢ (𝑛 ∈ 𝑆 → ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)) | 
| 9 | 8 | simprd 495 | . . . . . 6
⊢ (𝑛 ∈ 𝑆 → 𝑛 ∥ 𝑁) | 
| 10 | 9 | ad2antlr 727 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∥ 𝑁) | 
| 11 |  | prmz 16713 | . . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) | 
| 12 | 11 | adantl 481 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ) | 
| 13 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ 𝑆) | 
| 14 | 13, 7 | sylib 218 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) | 
| 15 | 14 | simpld 494 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℕ) | 
| 16 | 15 | nnzd 12642 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℤ) | 
| 17 |  | nnz 12636 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 18 | 17 | ad2antrr 726 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ) | 
| 19 |  | dvdstr 16332 | . . . . . 6
⊢ ((𝑝 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝑛 ∧ 𝑛 ∥ 𝑁) → 𝑝 ∥ 𝑁)) | 
| 20 | 12, 16, 18, 19 | syl3anc 1372 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑛 ∧ 𝑛 ∥ 𝑁) → 𝑝 ∥ 𝑁)) | 
| 21 | 10, 20 | mpan2d 694 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ 𝑛 → 𝑝 ∥ 𝑁)) | 
| 22 | 21 | ss2rabdv 4075 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 23 |  | prmex 16715 | . . . . 5
⊢ ℙ
∈ V | 
| 24 | 23 | rabex 5338 | . . . 4
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ∈ V | 
| 25 | 24 | elpw 4603 | . . 3
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ↔ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 26 | 22, 25 | sylibr 234 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 27 |  | cnveq 5883 | . . . . . . 7
⊢ (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) → ◡𝑦 = ◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) | 
| 28 | 27 | imaeq1d 6076 | . . . . . 6
⊢ (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) → (◡𝑦 “ ℕ) = (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ)) | 
| 29 | 28 | eleq1d 2825 | . . . . 5
⊢ (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) → ((◡𝑦 “ ℕ) ∈ Fin ↔ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin)) | 
| 30 |  | 1nn0 12544 | . . . . . . . . . 10
⊢ 1 ∈
ℕ0 | 
| 31 |  | 0nn0 12543 | . . . . . . . . . 10
⊢ 0 ∈
ℕ0 | 
| 32 | 30, 31 | ifcli 4572 | . . . . . . . . 9
⊢ if(𝑘 ∈ 𝑧, 1, 0) ∈
ℕ0 | 
| 33 | 32 | rgenw 3064 | . . . . . . . 8
⊢
∀𝑘 ∈
ℙ if(𝑘 ∈ 𝑧, 1, 0) ∈
ℕ0 | 
| 34 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) | 
| 35 | 34 | fmpt 7129 | . . . . . . . 8
⊢
(∀𝑘 ∈
ℙ if(𝑘 ∈ 𝑧, 1, 0) ∈
ℕ0 ↔ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0) | 
| 36 | 33, 35 | mpbi 230 | . . . . . . 7
⊢ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0 | 
| 37 | 36 | a1i 11 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0) | 
| 38 |  | nn0ex 12534 | . . . . . . 7
⊢
ℕ0 ∈ V | 
| 39 | 38, 23 | elmap 8912 | . . . . . 6
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ (ℕ0
↑m ℙ) ↔ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0) | 
| 40 | 37, 39 | sylibr 234 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ (ℕ0
↑m ℙ)) | 
| 41 |  | fzfi 14014 | . . . . . 6
⊢
(1...𝑁) ∈
Fin | 
| 42 |  | ffn 6735 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)):ℙ⟶ℕ0
→ (𝑘 ∈ ℙ
↦ if(𝑘 ∈ 𝑧, 1, 0)) Fn
ℙ) | 
| 43 |  | elpreima 7077 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) Fn ℙ → (𝑥 ∈ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ↔ (𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) ∈ ℕ))) | 
| 44 | 36, 42, 43 | mp2b 10 | . . . . . . . . . 10
⊢ (𝑥 ∈ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ↔ (𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) ∈ ℕ)) | 
| 45 |  | elequ1 2114 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → (𝑘 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) | 
| 46 | 45 | ifbid 4548 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑥 → if(𝑘 ∈ 𝑧, 1, 0) = if(𝑥 ∈ 𝑧, 1, 0)) | 
| 47 | 30, 31 | ifcli 4572 | . . . . . . . . . . . . . 14
⊢ if(𝑥 ∈ 𝑧, 1, 0) ∈
ℕ0 | 
| 48 | 47 | elexi 3502 | . . . . . . . . . . . . 13
⊢ if(𝑥 ∈ 𝑧, 1, 0) ∈ V | 
| 49 | 46, 34, 48 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) = if(𝑥 ∈ 𝑧, 1, 0)) | 
| 50 | 49 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℙ → (((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) ∈ ℕ ↔ if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ)) | 
| 51 | 50 | biimpa 476 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) ∈ ℕ) → if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ) | 
| 52 | 44, 51 | sylbi 217 | . . . . . . . . 9
⊢ (𝑥 ∈ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) → if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ) | 
| 53 |  | 0nnn 12303 | . . . . . . . . . . 11
⊢  ¬ 0
∈ ℕ | 
| 54 |  | iffalse 4533 | . . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, 1, 0) = 0) | 
| 55 | 54 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝑧 → (if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ ↔ 0 ∈
ℕ)) | 
| 56 | 53, 55 | mtbiri 327 | . . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝑧 → ¬ if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ) | 
| 57 | 56 | con4i 114 | . . . . . . . . 9
⊢ (if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ → 𝑥 ∈ 𝑧) | 
| 58 | 52, 57 | syl 17 | . . . . . . . 8
⊢ (𝑥 ∈ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) → 𝑥 ∈ 𝑧) | 
| 59 | 58 | ssriv 3986 | . . . . . . 7
⊢ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ⊆ 𝑧 | 
| 60 |  | elpwi 4606 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 61 | 60 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 62 |  | prmssnn 16714 | . . . . . . . . . 10
⊢ ℙ
⊆ ℕ | 
| 63 |  | rabss2 4077 | . . . . . . . . . 10
⊢ (ℙ
⊆ ℕ → {𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁}) | 
| 64 | 62, 63 | ax-mp 5 | . . . . . . . . 9
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁} | 
| 65 |  | dvdsssfz1 16356 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁} ⊆ (1...𝑁)) | 
| 66 | 65 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁} ⊆ (1...𝑁)) | 
| 67 | 64, 66 | sstrid 3994 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ (1...𝑁)) | 
| 68 | 61, 67 | sstrd 3993 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑧 ⊆ (1...𝑁)) | 
| 69 | 59, 68 | sstrid 3994 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁)) | 
| 70 |  | ssfi 9214 | . . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁)) → (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin) | 
| 71 | 41, 69, 70 | sylancr 587 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin) | 
| 72 | 29, 40, 71 | elrabd 3693 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}) | 
| 73 |  | sqff1o.3 | . . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) | 
| 74 |  | eqid 2736 | . . . . . . 7
⊢ {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} = {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin} | 
| 75 | 73, 74 | 1arith 16966 | . . . . . 6
⊢ 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin} | 
| 76 |  | f1ocnv 6859 | . . . . . 6
⊢ (𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} → ◡𝐺:{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ) | 
| 77 |  | f1of 6847 | . . . . . 6
⊢ (◡𝐺:{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ → ◡𝐺:{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}⟶ℕ) | 
| 78 | 75, 76, 77 | mp2b 10 | . . . . 5
⊢ ◡𝐺:{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}⟶ℕ | 
| 79 | 78 | ffvelcdmi 7102 | . . . 4
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ) | 
| 80 | 72, 79 | syl 17 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ) | 
| 81 |  | f1ocnvfv2 7298 | . . . . . . . . . . . 12
⊢ ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} ∧ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}) → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) | 
| 82 | 75, 72, 81 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) | 
| 83 | 73 | 1arithlem1 16962 | . . . . . . . . . . . 12
⊢ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))) | 
| 84 | 80, 83 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))) | 
| 85 | 82, 84 | eqtr3d 2778 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))) | 
| 86 | 85 | fveq1d 6907 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑞) = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞)) | 
| 87 |  | elequ1 2114 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑞 → (𝑘 ∈ 𝑧 ↔ 𝑞 ∈ 𝑧)) | 
| 88 | 87 | ifbid 4548 | . . . . . . . . . 10
⊢ (𝑘 = 𝑞 → if(𝑘 ∈ 𝑧, 1, 0) = if(𝑞 ∈ 𝑧, 1, 0)) | 
| 89 | 30, 31 | ifcli 4572 | . . . . . . . . . . 11
⊢ if(𝑞 ∈ 𝑧, 1, 0) ∈
ℕ0 | 
| 90 | 89 | elexi 3502 | . . . . . . . . . 10
⊢ if(𝑞 ∈ 𝑧, 1, 0) ∈ V | 
| 91 | 88, 34, 90 | fvmpt 7015 | . . . . . . . . 9
⊢ (𝑞 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑞) = if(𝑞 ∈ 𝑧, 1, 0)) | 
| 92 | 86, 91 | sylan9req 2797 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞) = if(𝑞 ∈ 𝑧, 1, 0)) | 
| 93 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 94 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 95 |  | ovex 7465 | . . . . . . . . . 10
⊢ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ∈ V | 
| 96 | 93, 94, 95 | fvmpt 7015 | . . . . . . . . 9
⊢ (𝑞 ∈ ℙ → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 97 | 96 | adantl 481 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 98 | 92, 97 | eqtr3d 2778 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞 ∈ 𝑧, 1, 0) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 99 |  | breq1 5145 | . . . . . . . 8
⊢ (1 =
if(𝑞 ∈ 𝑧, 1, 0) → (1 ≤ 1 ↔
if(𝑞 ∈ 𝑧, 1, 0) ≤
1)) | 
| 100 |  | breq1 5145 | . . . . . . . 8
⊢ (0 =
if(𝑞 ∈ 𝑧, 1, 0) → (0 ≤ 1 ↔
if(𝑞 ∈ 𝑧, 1, 0) ≤
1)) | 
| 101 |  | 1le1 11892 | . . . . . . . 8
⊢ 1 ≤
1 | 
| 102 |  | 0le1 11787 | . . . . . . . 8
⊢ 0 ≤
1 | 
| 103 | 99, 100, 101, 102 | keephyp 4596 | . . . . . . 7
⊢ if(𝑞 ∈ 𝑧, 1, 0) ≤ 1 | 
| 104 | 98, 103 | eqbrtrrdi 5182 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1) | 
| 105 | 104 | ralrimiva 3145 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1) | 
| 106 |  | issqf 27180 | . . . . . 6
⊢ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ →
((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1)) | 
| 107 | 80, 106 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1)) | 
| 108 | 105, 107 | mpbird 257 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0) | 
| 109 |  | iftrue 4530 | . . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) = 1) | 
| 110 | 109 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → if(𝑞 ∈ 𝑧, 1, 0) = 1) | 
| 111 | 61 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 112 |  | breq1 5145 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁)) | 
| 113 | 112 | elrab 3691 | . . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) | 
| 114 | 111, 113 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) | 
| 115 | 114 | simprd 495 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑞 ∥ 𝑁) | 
| 116 | 114 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑞 ∈ ℙ) | 
| 117 |  | simpll 766 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑁 ∈ ℕ) | 
| 118 |  | pcelnn 16909 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞 ∥ 𝑁)) | 
| 119 | 116, 117,
118 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞 ∥ 𝑁)) | 
| 120 | 115, 119 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → (𝑞 pCnt 𝑁) ∈ ℕ) | 
| 121 | 120 | nnge1d 12315 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 1 ≤ (𝑞 pCnt 𝑁)) | 
| 122 | 110, 121 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)) | 
| 123 | 122 | ex 412 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))) | 
| 124 | 123 | adantr 480 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))) | 
| 125 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ) | 
| 126 | 17 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑁 ∈ ℤ) | 
| 127 |  | pcge0 16901 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤
(𝑞 pCnt 𝑁)) | 
| 128 | 125, 126,
127 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → 0 ≤ (𝑞 pCnt 𝑁)) | 
| 129 |  | iffalse 4533 | . . . . . . . . . 10
⊢ (¬
𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) = 0) | 
| 130 | 129 | breq1d 5152 | . . . . . . . . 9
⊢ (¬
𝑞 ∈ 𝑧 → (if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁) ↔ 0 ≤ (𝑞 pCnt 𝑁))) | 
| 131 | 128, 130 | syl5ibrcom 247 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (¬ 𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))) | 
| 132 | 124, 131 | pm2.61d 179 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)) | 
| 133 | 98, 132 | eqbrtrrd 5166 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)) | 
| 134 | 133 | ralrimiva 3145 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)) | 
| 135 | 80 | nnzd 12642 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℤ) | 
| 136 | 17 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑁 ∈ ℤ) | 
| 137 |  | pc2dvds 16918 | . . . . . 6
⊢ (((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))) | 
| 138 | 135, 136,
137 | syl2anc 584 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))) | 
| 139 | 134, 138 | mpbird 257 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁) | 
| 140 | 108, 139 | jca 511 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ∧ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁)) | 
| 141 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → (μ‘𝑥) = (μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 142 | 141 | neeq1d 2999 | . . . . 5
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → ((μ‘𝑥) ≠ 0 ↔
(μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0)) | 
| 143 |  | breq1 5145 | . . . . 5
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → (𝑥 ∥ 𝑁 ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁)) | 
| 144 | 142, 143 | anbi12d 632 | . . . 4
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → (((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁) ↔ ((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ∧ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁))) | 
| 145 | 144, 6 | elrab2 3694 | . . 3
⊢ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ 𝑆 ↔ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ ∧
((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ∧ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁))) | 
| 146 | 80, 140, 145 | sylanbrc 583 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ 𝑆) | 
| 147 |  | eqcom 2743 | . . 3
⊢ (𝑛 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛) | 
| 148 | 7 | simplbi 497 | . . . . . . 7
⊢ (𝑛 ∈ 𝑆 → 𝑛 ∈ ℕ) | 
| 149 | 148 | ad2antrl 728 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑛 ∈ ℕ) | 
| 150 | 23 | mptex 7244 | . . . . . 6
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V | 
| 151 | 73 | fvmpt2 7026 | . . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V) → (𝐺‘𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) | 
| 152 | 149, 150,
151 | sylancl 586 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝐺‘𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) | 
| 153 | 152 | eqeq1d 2738 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝐺‘𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) | 
| 154 | 75 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}) | 
| 155 | 72 | adantrl 716 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}) | 
| 156 |  | f1ocnvfvb 7300 | . . . . 5
⊢ ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} ∧ 𝑛 ∈ ℕ ∧ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}) → ((𝐺‘𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛)) | 
| 157 | 154, 149,
155, 156 | syl3anc 1372 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝐺‘𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛)) | 
| 158 | 23 | a1i 11 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ℙ ∈
V) | 
| 159 |  | 0cnd 11255 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 0 ∈
ℂ) | 
| 160 |  | 1cnd 11257 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 1 ∈
ℂ) | 
| 161 |  | 0ne1 12338 | . . . . . . . 8
⊢ 0 ≠
1 | 
| 162 | 161 | a1i 11 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 0 ≠ 1) | 
| 163 | 158, 159,
160, 162 | pw2f1olem 9117 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ)
∧ 𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1})))) | 
| 164 |  | ssrab2 4079 | . . . . . . . . 9
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ ℙ | 
| 165 | 164 | sspwi 4611 | . . . . . . . 8
⊢ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} ⊆ 𝒫 ℙ | 
| 166 |  | simprr 772 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) | 
| 167 | 165, 166 | sselid 3980 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑧 ∈ 𝒫 ℙ) | 
| 168 | 167 | biantrurd 532 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) | 
| 169 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) | 
| 170 | 148 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → 𝑛 ∈ ℕ) | 
| 171 |  | pccl 16888 | . . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → (𝑝 pCnt 𝑛) ∈
ℕ0) | 
| 172 | 169, 170,
171 | syl2anr 597 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈
ℕ0) | 
| 173 |  | elnn0 12530 | . . . . . . . . . . . . . 14
⊢ ((𝑝 pCnt 𝑛) ∈ ℕ0 ↔ ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0)) | 
| 174 | 172, 173 | sylib 218 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0)) | 
| 175 | 174 | orcomd 871 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ)) | 
| 176 | 8 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑆 → (μ‘𝑛) ≠ 0) | 
| 177 | 176 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → (μ‘𝑛) ≠ 0) | 
| 178 |  | issqf 27180 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((μ‘𝑛) ≠ 0
↔ ∀𝑝 ∈
ℙ (𝑝 pCnt 𝑛) ≤ 1)) | 
| 179 | 170, 178 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → ((μ‘𝑛) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1)) | 
| 180 | 177, 179 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1) | 
| 181 | 180 | r19.21bi 3250 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ≤ 1) | 
| 182 |  | nnle1eq1 12297 | . . . . . . . . . . . . . 14
⊢ ((𝑝 pCnt 𝑛) ∈ ℕ → ((𝑝 pCnt 𝑛) ≤ 1 ↔ (𝑝 pCnt 𝑛) = 1)) | 
| 183 | 181, 182 | syl5ibcom 245 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ → (𝑝 pCnt 𝑛) = 1)) | 
| 184 | 183 | orim2d 968 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1))) | 
| 185 | 175, 184 | mpd 15 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1)) | 
| 186 |  | ovex 7465 | . . . . . . . . . . . 12
⊢ (𝑝 pCnt 𝑛) ∈ V | 
| 187 | 186 | elpr 4649 | . . . . . . . . . . 11
⊢ ((𝑝 pCnt 𝑛) ∈ {0, 1} ↔ ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1)) | 
| 188 | 185, 187 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈ {0, 1}) | 
| 189 | 188 | fmpttd 7134 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1}) | 
| 190 | 189 | adantrr 717 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1}) | 
| 191 |  | prex 5436 | . . . . . . . . 9
⊢ {0, 1}
∈ V | 
| 192 | 191, 23 | elmap 8912 | . . . . . . . 8
⊢ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ)
↔ (𝑝 ∈ ℙ
↦ (𝑝 pCnt 𝑛)):ℙ⟶{0,
1}) | 
| 193 | 190, 192 | sylibr 234 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m
ℙ)) | 
| 194 | 193 | biantrurd 532 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ)
∧ 𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1})))) | 
| 195 | 163, 168,
194 | 3bitr4d 311 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ 𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}))) | 
| 196 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) | 
| 197 | 196 | mptiniseg 6258 | . . . . . . . 8
⊢ (1 ∈
ℕ0 → (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1}) | 
| 198 | 30, 197 | ax-mp 5 | . . . . . . 7
⊢ (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} | 
| 199 |  | id 22 | . . . . . . . . . . . 12
⊢ ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) = 1) | 
| 200 |  | 1nn 12278 | . . . . . . . . . . . 12
⊢ 1 ∈
ℕ | 
| 201 | 199, 200 | eqeltrdi 2848 | . . . . . . . . . . 11
⊢ ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) ∈ ℕ) | 
| 202 | 201, 183 | impbid2 226 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ (𝑝 pCnt 𝑛) ∈ ℕ)) | 
| 203 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) | 
| 204 |  | pcelnn 16909 | . . . . . . . . . . 11
⊢ ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝 ∥ 𝑛)) | 
| 205 | 203, 15, 204 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝 ∥ 𝑛)) | 
| 206 | 202, 205 | bitrd 279 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ 𝑝 ∥ 𝑛)) | 
| 207 | 206 | rabbidva 3442 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) | 
| 208 | 207 | adantrr 717 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) | 
| 209 | 198, 208 | eqtrid 2788 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) | 
| 210 | 209 | eqeq2d 2747 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) | 
| 211 | 195, 210 | bitrd 279 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) | 
| 212 | 153, 157,
211 | 3bitr3d 309 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛 ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) | 
| 213 | 147, 212 | bitrid 283 | . 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑛 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) | 
| 214 | 1, 26, 146, 213 | f1o2d 7688 | 1
⊢ (𝑁 ∈ ℕ → 𝐹:𝑆–1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |