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

Theorem sqff1o 24708
Description: There is a bijection from the squarefree divisors of a number 𝑁 to the powerset of the prime divisors of 𝑁. Among other things, this implies that a number has 2↑𝑘 squarefree divisors where 𝑘 is the number of prime divisors, and a squarefree number has 2↑𝑘 divisors (because all divisors of a squarefree number are squarefree). The inverse function to 𝐹 takes the product of all the primes in some subset of prime divisors of 𝑁. (Contributed by Mario Carneiro, 1-Jul-2015.)
Hypotheses
Ref Expression
sqff1o.1 𝑆 = {𝑥 ∈ ℕ ∣ ((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁)}
sqff1o.2 𝐹 = (𝑛𝑆 ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑛})
sqff1o.3 𝐺 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
Assertion
Ref Expression
sqff1o (𝑁 ∈ ℕ → 𝐹:𝑆1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
Distinct variable groups:   𝑛,𝑝,𝑥,𝐺   𝑛,𝑁,𝑝,𝑥   𝑆,𝑛,𝑝
Allowed substitution hints:   𝑆(𝑥)   𝐹(𝑥,𝑛,𝑝)

Proof of Theorem sqff1o
Dummy variables 𝑘 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sqff1o.2 . 2 𝐹 = (𝑛𝑆 ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑛})
2 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑛 → (μ‘𝑥) = (μ‘𝑛))
32neeq1d 2841 . . . . . . . . . 10 (𝑥 = 𝑛 → ((μ‘𝑥) ≠ 0 ↔ (μ‘𝑛) ≠ 0))
4 breq1 4586 . . . . . . . . . 10 (𝑥 = 𝑛 → (𝑥𝑁𝑛𝑁))
53, 4anbi12d 743 . . . . . . . . 9 (𝑥 = 𝑛 → (((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁) ↔ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
6 sqff1o.1 . . . . . . . . 9 𝑆 = {𝑥 ∈ ℕ ∣ ((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁)}
75, 6elrab2 3333 . . . . . . . 8 (𝑛𝑆 ↔ (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
87simprbi 479 . . . . . . 7 (𝑛𝑆 → ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁))
98simprd 478 . . . . . 6 (𝑛𝑆𝑛𝑁)
109ad2antlr 759 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛𝑁)
11 prmz 15227 . . . . . . 7 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
1211adantl 481 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
13 simplr 788 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛𝑆)
1413, 7sylib 207 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
1514simpld 474 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℕ)
1615nnzd 11357 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℤ)
17 nnz 11276 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
1817ad2antrr 758 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ)
19 dvdstr 14856 . . . . . 6 ((𝑝 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝𝑛𝑛𝑁) → 𝑝𝑁))
2012, 16, 18, 19syl3anc 1318 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝𝑛𝑛𝑁) → 𝑝𝑁))
2110, 20mpan2d 706 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝𝑛𝑝𝑁))
2221ss2rabdv 3646 . . 3 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → {𝑝 ∈ ℙ ∣ 𝑝𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
23 nnex 10903 . . . . . 6 ℕ ∈ V
24 prmnn 15226 . . . . . . 7 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
2524ssriv 3572 . . . . . 6 ℙ ⊆ ℕ
2623, 25ssexi 4731 . . . . 5 ℙ ∈ V
2726rabex 4740 . . . 4 {𝑝 ∈ ℙ ∣ 𝑝𝑛} ∈ V
2827elpw 4114 . . 3 ({𝑝 ∈ ℙ ∣ 𝑝𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ↔ {𝑝 ∈ ℙ ∣ 𝑝𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
2922, 28sylibr 223 . 2 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → {𝑝 ∈ ℙ ∣ 𝑝𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
30 1nn0 11185 . . . . . . . . . 10 1 ∈ ℕ0
31 0nn0 11184 . . . . . . . . . 10 0 ∈ ℕ0
3230, 31keepel 4105 . . . . . . . . 9 if(𝑘𝑧, 1, 0) ∈ ℕ0
3332rgenw 2908 . . . . . . . 8 𝑘 ∈ ℙ if(𝑘𝑧, 1, 0) ∈ ℕ0
34 eqid 2610 . . . . . . . . 9 (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))
3534fmpt 6289 . . . . . . . 8 (∀𝑘 ∈ ℙ if(𝑘𝑧, 1, 0) ∈ ℕ0 ↔ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0)
3633, 35mpbi 219 . . . . . . 7 (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0
3736a1i 11 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0)
38 nn0ex 11175 . . . . . . 7 0 ∈ V
3938, 26elmap 7772 . . . . . 6 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ (ℕ0𝑚 ℙ) ↔ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0)
4037, 39sylibr 223 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ (ℕ0𝑚 ℙ))
41 fzfi 12633 . . . . . 6 (1...𝑁) ∈ Fin
42 ffn 5958 . . . . . . . . . . 11 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0 → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) Fn ℙ)
43 elpreima 6245 . . . . . . . . . . 11 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) Fn ℙ → (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ↔ (𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ)))
4436, 42, 43mp2b 10 . . . . . . . . . 10 (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ↔ (𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ))
45 elequ1 1984 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝑘𝑧𝑥𝑧))
4645ifbid 4058 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → if(𝑘𝑧, 1, 0) = if(𝑥𝑧, 1, 0))
4730, 31keepel 4105 . . . . . . . . . . . . . 14 if(𝑥𝑧, 1, 0) ∈ ℕ0
4847elexi 3186 . . . . . . . . . . . . 13 if(𝑥𝑧, 1, 0) ∈ V
4946, 34, 48fvmpt 6191 . . . . . . . . . . . 12 (𝑥 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) = if(𝑥𝑧, 1, 0))
5049eleq1d 2672 . . . . . . . . . . 11 (𝑥 ∈ ℙ → (((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ ↔ if(𝑥𝑧, 1, 0) ∈ ℕ))
5150biimpa 500 . . . . . . . . . 10 ((𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ) → if(𝑥𝑧, 1, 0) ∈ ℕ)
5244, 51sylbi 206 . . . . . . . . 9 (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) → if(𝑥𝑧, 1, 0) ∈ ℕ)
53 0nnn 10929 . . . . . . . . . . 11 ¬ 0 ∈ ℕ
54 iffalse 4045 . . . . . . . . . . . 12 𝑥𝑧 → if(𝑥𝑧, 1, 0) = 0)
5554eleq1d 2672 . . . . . . . . . . 11 𝑥𝑧 → (if(𝑥𝑧, 1, 0) ∈ ℕ ↔ 0 ∈ ℕ))
5653, 55mtbiri 316 . . . . . . . . . 10 𝑥𝑧 → ¬ if(𝑥𝑧, 1, 0) ∈ ℕ)
5756con4i 112 . . . . . . . . 9 (if(𝑥𝑧, 1, 0) ∈ ℕ → 𝑥𝑧)
5852, 57syl 17 . . . . . . . 8 (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) → 𝑥𝑧)
5958ssriv 3572 . . . . . . 7 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ⊆ 𝑧
60 elpwi 4117 . . . . . . . . 9 (𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
6160adantl 481 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
62 rabss2 3648 . . . . . . . . . 10 (ℙ ⊆ ℕ → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝𝑁})
6325, 62ax-mp 5 . . . . . . . . 9 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝𝑁}
64 dvdsssfz1 14878 . . . . . . . . . 10 (𝑁 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝𝑁} ⊆ (1...𝑁))
6564adantr 480 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → {𝑝 ∈ ℕ ∣ 𝑝𝑁} ⊆ (1...𝑁))
6663, 65syl5ss 3579 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ (1...𝑁))
6761, 66sstrd 3578 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑧 ⊆ (1...𝑁))
6859, 67syl5ss 3579 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁))
69 ssfi 8065 . . . . . 6 (((1...𝑁) ∈ Fin ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁)) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin)
7041, 68, 69sylancr 694 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin)
71 cnveq 5218 . . . . . . . 8 (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) → 𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))
7271imaeq1d 5384 . . . . . . 7 (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) → (𝑦 “ ℕ) = ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ))
7372eleq1d 2672 . . . . . 6 (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) → ((𝑦 “ ℕ) ∈ Fin ↔ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin))
7473elrab 3331 . . . . 5 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} ↔ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ (ℕ0𝑚 ℙ) ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin))
7540, 70, 74sylanbrc 695 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin})
76 sqff1o.3 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
77 eqid 2610 . . . . . . 7 {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} = {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}
7876, 771arith 15469 . . . . . 6 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}
79 f1ocnv 6062 . . . . . 6 (𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} → 𝐺:{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ)
80 f1of 6050 . . . . . 6 (𝐺:{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ → 𝐺:{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}⟶ℕ)
8178, 79, 80mp2b 10 . . . . 5 𝐺:{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}⟶ℕ
8281ffvelrni 6266 . . . 4 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ)
8375, 82syl 17 . . 3 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ)
84 f1ocnvfv2 6433 . . . . . . . . . . . 12 ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} ∧ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}) → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))
8578, 75, 84sylancr 694 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))
86761arithlem1 15465 . . . . . . . . . . . 12 ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))))
8783, 86syl 17 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))))
8885, 87eqtr3d 2646 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))))
8988fveq1d 6105 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑞) = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞))
90 elequ1 1984 . . . . . . . . . . 11 (𝑘 = 𝑞 → (𝑘𝑧𝑞𝑧))
9190ifbid 4058 . . . . . . . . . 10 (𝑘 = 𝑞 → if(𝑘𝑧, 1, 0) = if(𝑞𝑧, 1, 0))
9230, 31keepel 4105 . . . . . . . . . . 11 if(𝑞𝑧, 1, 0) ∈ ℕ0
9392elexi 3186 . . . . . . . . . 10 if(𝑞𝑧, 1, 0) ∈ V
9491, 34, 93fvmpt 6191 . . . . . . . . 9 (𝑞 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑞) = if(𝑞𝑧, 1, 0))
9589, 94sylan9req 2665 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞) = if(𝑞𝑧, 1, 0))
96 oveq1 6556 . . . . . . . . . 10 (𝑝 = 𝑞 → (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
97 eqid 2610 . . . . . . . . . 10 (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
98 ovex 6577 . . . . . . . . . 10 (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ∈ V
9996, 97, 98fvmpt 6191 . . . . . . . . 9 (𝑞 ∈ ℙ → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
10099adantl 481 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
10195, 100eqtr3d 2646 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞𝑧, 1, 0) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
102 breq1 4586 . . . . . . . 8 (1 = if(𝑞𝑧, 1, 0) → (1 ≤ 1 ↔ if(𝑞𝑧, 1, 0) ≤ 1))
103 breq1 4586 . . . . . . . 8 (0 = if(𝑞𝑧, 1, 0) → (0 ≤ 1 ↔ if(𝑞𝑧, 1, 0) ≤ 1))
104 1le1 10534 . . . . . . . 8 1 ≤ 1
105 0le1 10430 . . . . . . . 8 0 ≤ 1
106102, 103, 104, 105keephyp 4102 . . . . . . 7 if(𝑞𝑧, 1, 0) ≤ 1
107101, 106syl6eqbrr 4623 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1)
108107ralrimiva 2949 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1)
109 issqf 24662 . . . . . 6 ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ → ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1))
11083, 109syl 17 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1))
111108, 110mpbird 246 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0)
112 iftrue 4042 . . . . . . . . . . . 12 (𝑞𝑧 → if(𝑞𝑧, 1, 0) = 1)
113112adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → if(𝑞𝑧, 1, 0) = 1)
11461sselda 3568 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
115 breq1 4586 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑁𝑞𝑁))
116115elrab 3331 . . . . . . . . . . . . . . 15 (𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝑁} ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑁))
117114, 116sylib 207 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → (𝑞 ∈ ℙ ∧ 𝑞𝑁))
118117simprd 478 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑞𝑁)
119117simpld 474 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑞 ∈ ℙ)
120 simpll 786 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑁 ∈ ℕ)
121 pcelnn 15412 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞𝑁))
122119, 120, 121syl2anc 691 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞𝑁))
123118, 122mpbird 246 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → (𝑞 pCnt 𝑁) ∈ ℕ)
124123nnge1d 10940 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 1 ≤ (𝑞 pCnt 𝑁))
125113, 124eqbrtrd 4605 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))
126125ex 449 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑞𝑧 → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)))
127126adantr 480 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞𝑧 → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)))
128 simpr 476 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ)
12917ad2antrr 758 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑁 ∈ ℤ)
130 pcge0 15404 . . . . . . . . . 10 ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑞 pCnt 𝑁))
131128, 129, 130syl2anc 691 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → 0 ≤ (𝑞 pCnt 𝑁))
132 iffalse 4045 . . . . . . . . . 10 𝑞𝑧 → if(𝑞𝑧, 1, 0) = 0)
133132breq1d 4593 . . . . . . . . 9 𝑞𝑧 → (if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁) ↔ 0 ≤ (𝑞 pCnt 𝑁)))
134131, 133syl5ibrcom 236 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (¬ 𝑞𝑧 → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)))
135127, 134pm2.61d 169 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))
136101, 135eqbrtrrd 4607 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))
137136ralrimiva 2949 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))
13883nnzd 11357 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℤ)
13917adantr 480 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑁 ∈ ℤ)
140 pc2dvds 15421 . . . . . 6 (((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)))
141138, 139, 140syl2anc 691 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)))
142137, 141mpbird 246 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁)
143111, 142jca 553 . . 3 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ∧ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁))
144 fveq2 6103 . . . . . 6 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → (μ‘𝑥) = (μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
145144neeq1d 2841 . . . . 5 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → ((μ‘𝑥) ≠ 0 ↔ (μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0))
146 breq1 4586 . . . . 5 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → (𝑥𝑁 ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁))
147145, 146anbi12d 743 . . . 4 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → (((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁) ↔ ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ∧ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁)))
148147, 6elrab2 3333 . . 3 ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ 𝑆 ↔ ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ ∧ ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ∧ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁)))
14983, 143, 148sylanbrc 695 . 2 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ 𝑆)
150 eqcom 2617 . . 3 (𝑛 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛)
1517simplbi 475 . . . . . . 7 (𝑛𝑆𝑛 ∈ ℕ)
152151ad2antrl 760 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑛 ∈ ℕ)
15326mptex 6390 . . . . . 6 (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V
15476fvmpt2 6200 . . . . . 6 ((𝑛 ∈ ℕ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V) → (𝐺𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
155152, 153, 154sylancl 693 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝐺𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
156155eqeq1d 2612 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝐺𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))
15778a1i 11 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin})
15875adantrl 748 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin})
159 f1ocnvfvb 6435 . . . . 5 ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} ∧ 𝑛 ∈ ℕ ∧ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0𝑚 ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}) → ((𝐺𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛))
160157, 152, 158, 159syl3anc 1318 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝐺𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛))
16126a1i 11 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ℙ ∈ V)
162 0cnd 9912 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 0 ∈ ℂ)
163 1cnd 9935 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 1 ∈ ℂ)
164 0ne1 10965 . . . . . . . 8 0 ≠ 1
165164a1i 11 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 0 ≠ 1)
166161, 162, 163, 165pw2f1olem 7949 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚 ℙ) ∧ 𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}))))
167 ssrab2 3650 . . . . . . . . 9 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ ℙ
168 sspwb 4844 . . . . . . . . 9 ({𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ ℙ ↔ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ 𝒫 ℙ)
169167, 168mpbi 219 . . . . . . . 8 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ 𝒫 ℙ
170 simprr 792 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
171169, 170sseldi 3566 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑧 ∈ 𝒫 ℙ)
172171biantrurd 528 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
173 id 22 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
174151adantl 481 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → 𝑛 ∈ ℕ)
175 pccl 15392 . . . . . . . . . . . . . . 15 ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → (𝑝 pCnt 𝑛) ∈ ℕ0)
176173, 174, 175syl2anr 494 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈ ℕ0)
177 elnn0 11171 . . . . . . . . . . . . . 14 ((𝑝 pCnt 𝑛) ∈ ℕ0 ↔ ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0))
178176, 177sylib 207 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0))
179178orcomd 402 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ))
1808simpld 474 . . . . . . . . . . . . . . . . 17 (𝑛𝑆 → (μ‘𝑛) ≠ 0)
181180adantl 481 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → (μ‘𝑛) ≠ 0)
182 issqf 24662 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((μ‘𝑛) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1))
183174, 182syl 17 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → ((μ‘𝑛) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1))
184181, 183mpbid 221 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1)
185184r19.21bi 2916 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ≤ 1)
186 nnle1eq1 10925 . . . . . . . . . . . . . 14 ((𝑝 pCnt 𝑛) ∈ ℕ → ((𝑝 pCnt 𝑛) ≤ 1 ↔ (𝑝 pCnt 𝑛) = 1))
187185, 186syl5ibcom 234 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ → (𝑝 pCnt 𝑛) = 1))
188187orim2d 881 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1)))
189179, 188mpd 15 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1))
190 ovex 6577 . . . . . . . . . . . 12 (𝑝 pCnt 𝑛) ∈ V
191190elpr 4146 . . . . . . . . . . 11 ((𝑝 pCnt 𝑛) ∈ {0, 1} ↔ ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1))
192189, 191sylibr 223 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈ {0, 1})
193 eqid 2610 . . . . . . . . . 10 (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))
194192, 193fmptd 6292 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1})
195194adantrr 749 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1})
196 prex 4836 . . . . . . . . 9 {0, 1} ∈ V
197196, 26elmap 7772 . . . . . . . 8 ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚 ℙ) ↔ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1})
198195, 197sylibr 223 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚 ℙ))
199198biantrurd 528 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑𝑚 ℙ) ∧ 𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}))))
200166, 172, 1993bitr4d 299 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ 𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1})))
201193mptiniseg 5546 . . . . . . . 8 (1 ∈ ℕ0 → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1})
20230, 201ax-mp 5 . . . . . . 7 ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1}
203 id 22 . . . . . . . . . . . 12 ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) = 1)
204 1nn 10908 . . . . . . . . . . . 12 1 ∈ ℕ
205203, 204syl6eqel 2696 . . . . . . . . . . 11 ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) ∈ ℕ)
206205, 187impbid2 215 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ (𝑝 pCnt 𝑛) ∈ ℕ))
207 simpr 476 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
208 pcelnn 15412 . . . . . . . . . . 11 ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝𝑛))
209207, 15, 208syl2anc 691 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝𝑛))
210206, 209bitrd 267 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ 𝑝𝑛))
211210rabbidva 3163 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝𝑛})
212211adantrr 749 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝𝑛})
213202, 212syl5eq 2656 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ 𝑝𝑛})
214213eqeq2d 2620 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
215200, 214bitrd 267 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
216156, 160, 2153bitr3d 297 . . 3 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
217150, 216syl5bb 271 . 2 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑛 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
2181, 29, 149, 217f1o2d 6785 1 (𝑁 ∈ ℕ → 𝐹:𝑆1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383   = wceq 1475  wcel 1977  wne 2780  wral 2896  {crab 2900  Vcvv 3173  wss 3540  ifcif 4036  𝒫 cpw 4108  {csn 4125  {cpr 4127   class class class wbr 4583  cmpt 4643  ccnv 5037  cima 5041   Fn wfn 5799  wf 5800  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  𝑚 cmap 7744  Fincfn 7841  cc 9813  0cc0 9815  1c1 9816  cle 9954  cn 10897  0cn0 11169  cz 11254  ...cfz 12197  cdvds 14821  cprime 15223   pCnt cpc 15379  μcmu 24621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-fz 12198  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822  df-gcd 15055  df-prm 15224  df-pc 15380  df-mu 24627
This theorem is referenced by:  musum  24717
  Copyright terms: Public domain W3C validator