Step | Hyp | Ref
| Expression |
1 | | sqff1o.2 |
. 2
⊢ 𝐹 = (𝑛 ∈ 𝑆 ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) |
2 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (μ‘𝑥) = (μ‘𝑛)) |
3 | 2 | neeq1d 2853 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → ((μ‘𝑥) ≠ 0 ↔ (μ‘𝑛) ≠ 0)) |
4 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁)) |
5 | 3, 4 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁) ↔ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) |
6 | | sqff1o.1 |
. . . . . . . . 9
⊢ 𝑆 = {𝑥 ∈ ℕ ∣ ((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁)} |
7 | 5, 6 | elrab2 3366 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑆 ↔ (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) |
8 | 7 | simprbi 480 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑆 → ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)) |
9 | 8 | simprd 479 |
. . . . . 6
⊢ (𝑛 ∈ 𝑆 → 𝑛 ∥ 𝑁) |
10 | 9 | ad2antlr 763 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∥ 𝑁) |
11 | | prmz 15389 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
12 | 11 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ) |
13 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ 𝑆) |
14 | 13, 7 | sylib 208 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) |
15 | 14 | simpld 475 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℕ) |
16 | 15 | nnzd 11481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℤ) |
17 | | nnz 11399 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
18 | 17 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ) |
19 | | dvdstr 15018 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝑛 ∧ 𝑛 ∥ 𝑁) → 𝑝 ∥ 𝑁)) |
20 | 12, 16, 18, 19 | syl3anc 1326 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑛 ∧ 𝑛 ∥ 𝑁) → 𝑝 ∥ 𝑁)) |
21 | 10, 20 | mpan2d 710 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ 𝑛 → 𝑝 ∥ 𝑁)) |
22 | 21 | ss2rabdv 3683 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
23 | | nnex 11026 |
. . . . . 6
⊢ ℕ
∈ V |
24 | | prmnn 15388 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
25 | 24 | ssriv 3607 |
. . . . . 6
⊢ ℙ
⊆ ℕ |
26 | 23, 25 | ssexi 4803 |
. . . . 5
⊢ ℙ
∈ V |
27 | 26 | rabex 4813 |
. . . 4
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ∈ V |
28 | 27 | elpw 4164 |
. . 3
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ↔ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
29 | 22, 28 | sylibr 224 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
30 | | 1nn0 11308 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
31 | | 0nn0 11307 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
32 | 30, 31 | keepel 4155 |
. . . . . . . . 9
⊢ if(𝑘 ∈ 𝑧, 1, 0) ∈
ℕ0 |
33 | 32 | rgenw 2924 |
. . . . . . . 8
⊢
∀𝑘 ∈
ℙ if(𝑘 ∈ 𝑧, 1, 0) ∈
ℕ0 |
34 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) |
35 | 34 | fmpt 6381 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℙ if(𝑘 ∈ 𝑧, 1, 0) ∈
ℕ0 ↔ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0) |
36 | 33, 35 | mpbi 220 |
. . . . . . 7
⊢ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0 |
37 | 36 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0) |
38 | | nn0ex 11298 |
. . . . . . 7
⊢
ℕ0 ∈ V |
39 | 38, 26 | elmap 7886 |
. . . . . 6
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ (ℕ0
↑𝑚 ℙ) ↔ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1,
0)):ℙ⟶ℕ0) |
40 | 37, 39 | sylibr 224 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ (ℕ0
↑𝑚 ℙ)) |
41 | | fzfi 12771 |
. . . . . 6
⊢
(1...𝑁) ∈
Fin |
42 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)):ℙ⟶ℕ0
→ (𝑘 ∈ ℙ
↦ if(𝑘 ∈ 𝑧, 1, 0)) Fn
ℙ) |
43 | | elpreima 6337 |
. . . . . . . . . . 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 1997 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → (𝑘 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
46 | 45 | ifbid 4108 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑥 → if(𝑘 ∈ 𝑧, 1, 0) = if(𝑥 ∈ 𝑧, 1, 0)) |
47 | 30, 31 | keepel 4155 |
. . . . . . . . . . . . . 14
⊢ if(𝑥 ∈ 𝑧, 1, 0) ∈
ℕ0 |
48 | 47 | elexi 3213 |
. . . . . . . . . . . . 13
⊢ if(𝑥 ∈ 𝑧, 1, 0) ∈ V |
49 | 46, 34, 48 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) = if(𝑥 ∈ 𝑧, 1, 0)) |
50 | 49 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℙ → (((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) ∈ ℕ ↔ if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ)) |
51 | 50 | biimpa 501 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑥) ∈ ℕ) → if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ) |
52 | 44, 51 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) → if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ) |
53 | | 0nnn 11052 |
. . . . . . . . . . 11
⊢ ¬ 0
∈ ℕ |
54 | | iffalse 4095 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, 1, 0) = 0) |
55 | 54 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝑧 → (if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ ↔ 0 ∈
ℕ)) |
56 | 53, 55 | mtbiri 317 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝑧 → ¬ if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ) |
57 | 56 | con4i 113 |
. . . . . . . . 9
⊢ (if(𝑥 ∈ 𝑧, 1, 0) ∈ ℕ → 𝑥 ∈ 𝑧) |
58 | 52, 57 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) → 𝑥 ∈ 𝑧) |
59 | 58 | ssriv 3607 |
. . . . . . 7
⊢ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ⊆ 𝑧 |
60 | | elpwi 4168 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
61 | 60 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
62 | | rabss2 3685 |
. . . . . . . . . 10
⊢ (ℙ
⊆ ℕ → {𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁}) |
63 | 25, 62 | ax-mp 5 |
. . . . . . . . 9
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁} |
64 | | dvdsssfz1 15040 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁} ⊆ (1...𝑁)) |
65 | 64 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁} ⊆ (1...𝑁)) |
66 | 63, 65 | syl5ss 3614 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ (1...𝑁)) |
67 | 61, 66 | sstrd 3613 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑧 ⊆ (1...𝑁)) |
68 | 59, 67 | syl5ss 3614 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁)) |
69 | | ssfi 8180 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁)) → (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin) |
70 | 41, 68, 69 | sylancr 695 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin) |
71 | | cnveq 5296 |
. . . . . . . 8
⊢ (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) → ◡𝑦 = ◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) |
72 | 71 | imaeq1d 5465 |
. . . . . . 7
⊢ (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) → (◡𝑦 “ ℕ) = (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ)) |
73 | 72 | eleq1d 2686 |
. . . . . 6
⊢ (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) → ((◡𝑦 “ ℕ) ∈ Fin ↔ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin)) |
74 | 73 | elrab 3363 |
. . . . 5
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} ↔ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ (ℕ0
↑𝑚 ℙ) ∧ (◡(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) “ ℕ) ∈
Fin)) |
75 | 40, 70, 74 | sylanbrc 698 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}) |
76 | | sqff1o.3 |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
77 | | eqid 2622 |
. . . . . . 7
⊢ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} = {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin} |
78 | 76, 77 | 1arith 15631 |
. . . . . 6
⊢ 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin} |
79 | | f1ocnv 6149 |
. . . . . 6
⊢ (𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} → ◡𝐺:{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ) |
80 | | f1of 6137 |
. . . . . 6
⊢ (◡𝐺:{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ → ◡𝐺:{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}⟶ℕ) |
81 | 78, 79, 80 | mp2b 10 |
. . . . 5
⊢ ◡𝐺:{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}⟶ℕ |
82 | 81 | ffvelrni 6358 |
. . . 4
⊢ ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ) |
83 | 75, 82 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ) |
84 | | f1ocnvfv2 6533 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} ∧ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}) → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) |
85 | 78, 75, 84 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) |
86 | 76 | 1arithlem1 15627 |
. . . . . . . . . . . 12
⊢ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))) |
87 | 83, 86 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝐺‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))) |
88 | 85, 87 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))) |
89 | 88 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑞) = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞)) |
90 | | elequ1 1997 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑞 → (𝑘 ∈ 𝑧 ↔ 𝑞 ∈ 𝑧)) |
91 | 90 | ifbid 4108 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑞 → if(𝑘 ∈ 𝑧, 1, 0) = if(𝑞 ∈ 𝑧, 1, 0)) |
92 | 30, 31 | keepel 4155 |
. . . . . . . . . . 11
⊢ if(𝑞 ∈ 𝑧, 1, 0) ∈
ℕ0 |
93 | 92 | elexi 3213 |
. . . . . . . . . 10
⊢ if(𝑞 ∈ 𝑧, 1, 0) ∈ V |
94 | 91, 34, 93 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))‘𝑞) = if(𝑞 ∈ 𝑧, 1, 0)) |
95 | 89, 94 | sylan9req 2677 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞) = if(𝑞 ∈ 𝑧, 1, 0)) |
96 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
97 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
98 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ∈ V |
99 | 96, 97, 98 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℙ → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
100 | 99 | adantl 482 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
101 | 95, 100 | eqtr3d 2658 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞 ∈ 𝑧, 1, 0) = (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
102 | | breq1 4656 |
. . . . . . . 8
⊢ (1 =
if(𝑞 ∈ 𝑧, 1, 0) → (1 ≤ 1 ↔
if(𝑞 ∈ 𝑧, 1, 0) ≤
1)) |
103 | | breq1 4656 |
. . . . . . . 8
⊢ (0 =
if(𝑞 ∈ 𝑧, 1, 0) → (0 ≤ 1 ↔
if(𝑞 ∈ 𝑧, 1, 0) ≤
1)) |
104 | | 1le1 10655 |
. . . . . . . 8
⊢ 1 ≤
1 |
105 | | 0le1 10551 |
. . . . . . . 8
⊢ 0 ≤
1 |
106 | 102, 103,
104, 105 | keephyp 4152 |
. . . . . . 7
⊢ if(𝑞 ∈ 𝑧, 1, 0) ≤ 1 |
107 | 101, 106 | syl6eqbrr 4693 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1) |
108 | 107 | ralrimiva 2966 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1) |
109 | | issqf 24862 |
. . . . . 6
⊢ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ →
((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1)) |
110 | 83, 109 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ 1)) |
111 | 108, 110 | mpbird 247 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0) |
112 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) = 1) |
113 | 112 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → if(𝑞 ∈ 𝑧, 1, 0) = 1) |
114 | 61 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
115 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁)) |
116 | 115 | elrab 3363 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) |
117 | 114, 116 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) |
118 | 117 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑞 ∥ 𝑁) |
119 | 117 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑞 ∈ ℙ) |
120 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 𝑁 ∈ ℕ) |
121 | | pcelnn 15574 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞 ∥ 𝑁)) |
122 | 119, 120,
121 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞 ∥ 𝑁)) |
123 | 118, 122 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → (𝑞 pCnt 𝑁) ∈ ℕ) |
124 | 123 | nnge1d 11063 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → 1 ≤ (𝑞 pCnt 𝑁)) |
125 | 113, 124 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ 𝑧) → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)) |
126 | 125 | ex 450 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))) |
127 | 126 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))) |
128 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ) |
129 | 17 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑁 ∈ ℤ) |
130 | | pcge0 15566 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤
(𝑞 pCnt 𝑁)) |
131 | 128, 129,
130 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → 0 ≤ (𝑞 pCnt 𝑁)) |
132 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) = 0) |
133 | 132 | breq1d 4663 |
. . . . . . . . 9
⊢ (¬
𝑞 ∈ 𝑧 → (if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁) ↔ 0 ≤ (𝑞 pCnt 𝑁))) |
134 | 131, 133 | syl5ibrcom 237 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (¬ 𝑞 ∈ 𝑧 → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))) |
135 | 127, 134 | pm2.61d 170 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞 ∈ 𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)) |
136 | 101, 135 | eqbrtrrd 4677 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)) |
137 | 136 | ralrimiva 2966 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)) |
138 | 83 | nnzd 11481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℤ) |
139 | 17 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑁 ∈ ℤ) |
140 | | pc2dvds 15583 |
. . . . . 6
⊢ (((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))) |
141 | 138, 139,
140 | syl2anc 693 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))) |
142 | 137, 141 | mpbird 247 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁) |
143 | 111, 142 | jca 554 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ∧ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁)) |
144 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → (μ‘𝑥) = (μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
145 | 144 | neeq1d 2853 |
. . . . 5
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → ((μ‘𝑥) ≠ 0 ↔
(μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0)) |
146 | | breq1 4656 |
. . . . 5
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → (𝑥 ∥ 𝑁 ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁)) |
147 | 145, 146 | anbi12d 747 |
. . . 4
⊢ (𝑥 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) → (((μ‘𝑥) ≠ 0 ∧ 𝑥 ∥ 𝑁) ↔ ((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ∧ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁))) |
148 | 147, 6 | elrab2 3366 |
. . 3
⊢ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ 𝑆 ↔ ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ ℕ ∧
((μ‘(◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) ≠ 0 ∧ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∥ 𝑁))) |
149 | 83, 143, 148 | sylanbrc 698 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ∈ 𝑆) |
150 | | eqcom 2629 |
. . 3
⊢ (𝑛 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛) |
151 | 7 | simplbi 476 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑆 → 𝑛 ∈ ℕ) |
152 | 151 | ad2antrl 764 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑛 ∈ ℕ) |
153 | 26 | mptex 6486 |
. . . . . 6
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V |
154 | 76 | fvmpt2 6291 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V) → (𝐺‘𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
155 | 152, 153,
154 | sylancl 694 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝐺‘𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
156 | 155 | eqeq1d 2624 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝐺‘𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)))) |
157 | 78 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}) |
158 | 75 | adantrl 752 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈
Fin}) |
159 | | f1ocnvfvb 6535 |
. . . . 5
⊢ ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin} ∧ 𝑛 ∈ ℕ ∧ (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑦 “ ℕ) ∈ Fin}) → ((𝐺‘𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛)) |
160 | 157, 152,
158, 159 | syl3anc 1326 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝐺‘𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛)) |
161 | 26 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ℙ ∈
V) |
162 | | 0cnd 10033 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 0 ∈
ℂ) |
163 | | 1cnd 10056 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 1 ∈
ℂ) |
164 | | 0ne1 11088 |
. . . . . . . 8
⊢ 0 ≠
1 |
165 | 164 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 0 ≠ 1) |
166 | 161, 162,
163, 165 | pw2f1olem 8064 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚
ℙ) ∧ 𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1})))) |
167 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ ℙ |
168 | | sspwb 4917 |
. . . . . . . . 9
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ ℙ ↔ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ⊆ 𝒫
ℙ) |
169 | 167, 168 | mpbi 220 |
. . . . . . . 8
⊢ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} ⊆ 𝒫 ℙ |
170 | | simprr 796 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
171 | 169, 170 | sseldi 3601 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑧 ∈ 𝒫 ℙ) |
172 | 171 | biantrurd 529 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ (𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))))) |
173 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) |
174 | 151 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → 𝑛 ∈ ℕ) |
175 | | pccl 15554 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → (𝑝 pCnt 𝑛) ∈
ℕ0) |
176 | 173, 174,
175 | syl2anr 495 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈
ℕ0) |
177 | | elnn0 11294 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 pCnt 𝑛) ∈ ℕ0 ↔ ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0)) |
178 | 176, 177 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0)) |
179 | 178 | orcomd 403 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ)) |
180 | 8 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑆 → (μ‘𝑛) ≠ 0) |
181 | 180 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → (μ‘𝑛) ≠ 0) |
182 | | issqf 24862 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((μ‘𝑛) ≠ 0
↔ ∀𝑝 ∈
ℙ (𝑝 pCnt 𝑛) ≤ 1)) |
183 | 174, 182 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → ((μ‘𝑛) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1)) |
184 | 181, 183 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1) |
185 | 184 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ≤ 1) |
186 | | nnle1eq1 11048 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 pCnt 𝑛) ∈ ℕ → ((𝑝 pCnt 𝑛) ≤ 1 ↔ (𝑝 pCnt 𝑛) = 1)) |
187 | 185, 186 | syl5ibcom 235 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ → (𝑝 pCnt 𝑛) = 1)) |
188 | 187 | orim2d 885 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1))) |
189 | 179, 188 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1)) |
190 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑝 pCnt 𝑛) ∈ V |
191 | 190 | elpr 4198 |
. . . . . . . . . . 11
⊢ ((𝑝 pCnt 𝑛) ∈ {0, 1} ↔ ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1)) |
192 | 189, 191 | sylibr 224 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈ {0, 1}) |
193 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) |
194 | 192, 193 | fmptd 6385 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1}) |
195 | 194 | adantrr 753 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1}) |
196 | | prex 4909 |
. . . . . . . . 9
⊢ {0, 1}
∈ V |
197 | 196, 26 | elmap 7886 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚
ℙ) ↔ (𝑝 ∈
ℙ ↦ (𝑝 pCnt
𝑛)):ℙ⟶{0,
1}) |
198 | 195, 197 | sylibr 224 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚
ℙ)) |
199 | 198 | biantrurd 529 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚
ℙ) ∧ 𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1})))) |
200 | 166, 172,
199 | 3bitr4d 300 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ 𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}))) |
201 | 193 | mptiniseg 5629 |
. . . . . . . 8
⊢ (1 ∈
ℕ0 → (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1}) |
202 | 30, 201 | ax-mp 5 |
. . . . . . 7
⊢ (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} |
203 | | id 22 |
. . . . . . . . . . . 12
⊢ ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) = 1) |
204 | | 1nn 11031 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
205 | 203, 204 | syl6eqel 2709 |
. . . . . . . . . . 11
⊢ ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) ∈ ℕ) |
206 | 205, 187 | impbid2 216 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ (𝑝 pCnt 𝑛) ∈ ℕ)) |
207 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
208 | | pcelnn 15574 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝 ∥ 𝑛)) |
209 | 207, 15, 208 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝 ∥ 𝑛)) |
210 | 206, 209 | bitrd 268 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ 𝑝 ∥ 𝑛)) |
211 | 210 | rabbidva 3188 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) |
212 | 211 | adantrr 753 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) |
213 | 202, 212 | syl5eq 2668 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛}) |
214 | 213 | eqeq2d 2632 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑧 = (◡(𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) |
215 | 200, 214 | bitrd 268 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0)) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) |
216 | 156, 160,
215 | 3bitr3d 298 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → ((◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) = 𝑛 ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) |
217 | 150, 216 | syl5bb 272 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → (𝑛 = (◡𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘 ∈ 𝑧, 1, 0))) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛})) |
218 | 1, 29, 149, 217 | f1o2d 6887 |
1
⊢ (𝑁 ∈ ℕ → 𝐹:𝑆–1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |