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

Theorem sqff1o 27240
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 6907 . . . . . . . . . . 11 (𝑥 = 𝑛 → (μ‘𝑥) = (μ‘𝑛))
32neeq1d 2998 . . . . . . . . . 10 (𝑥 = 𝑛 → ((μ‘𝑥) ≠ 0 ↔ (μ‘𝑛) ≠ 0))
4 breq1 5151 . . . . . . . . . 10 (𝑥 = 𝑛 → (𝑥𝑁𝑛𝑁))
53, 4anbi12d 632 . . . . . . . . 9 (𝑥 = 𝑛 → (((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁) ↔ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
6 sqff1o.1 . . . . . . . . 9 𝑆 = {𝑥 ∈ ℕ ∣ ((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁)}
75, 6elrab2 3698 . . . . . . . 8 (𝑛𝑆 ↔ (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
87simprbi 496 . . . . . . 7 (𝑛𝑆 → ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁))
98simprd 495 . . . . . 6 (𝑛𝑆𝑛𝑁)
109ad2antlr 727 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛𝑁)
11 prmz 16709 . . . . . . 7 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
1211adantl 481 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
13 simplr 769 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛𝑆)
1413, 7sylib 218 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑛 ∈ ℕ ∧ ((μ‘𝑛) ≠ 0 ∧ 𝑛𝑁)))
1514simpld 494 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℕ)
1615nnzd 12638 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℤ)
17 nnz 12632 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
1817ad2antrr 726 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ)
19 dvdstr 16328 . . . . . 6 ((𝑝 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝𝑛𝑛𝑁) → 𝑝𝑁))
2012, 16, 18, 19syl3anc 1370 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝𝑛𝑛𝑁) → 𝑝𝑁))
2110, 20mpan2d 694 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝𝑛𝑝𝑁))
2221ss2rabdv 4086 . . 3 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → {𝑝 ∈ ℙ ∣ 𝑝𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
23 prmex 16711 . . . . 5 ℙ ∈ V
2423rabex 5345 . . . 4 {𝑝 ∈ ℙ ∣ 𝑝𝑛} ∈ V
2524elpw 4609 . . 3 ({𝑝 ∈ ℙ ∣ 𝑝𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ↔ {𝑝 ∈ ℙ ∣ 𝑝𝑛} ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
2622, 25sylibr 234 . 2 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → {𝑝 ∈ ℙ ∣ 𝑝𝑛} ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
27 cnveq 5887 . . . . . . 7 (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) → 𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))
2827imaeq1d 6079 . . . . . 6 (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) → (𝑦 “ ℕ) = ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ))
2928eleq1d 2824 . . . . 5 (𝑦 = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) → ((𝑦 “ ℕ) ∈ Fin ↔ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin))
30 1nn0 12540 . . . . . . . . . 10 1 ∈ ℕ0
31 0nn0 12539 . . . . . . . . . 10 0 ∈ ℕ0
3230, 31ifcli 4578 . . . . . . . . 9 if(𝑘𝑧, 1, 0) ∈ ℕ0
3332rgenw 3063 . . . . . . . 8 𝑘 ∈ ℙ if(𝑘𝑧, 1, 0) ∈ ℕ0
34 eqid 2735 . . . . . . . . 9 (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))
3534fmpt 7130 . . . . . . . 8 (∀𝑘 ∈ ℙ if(𝑘𝑧, 1, 0) ∈ ℕ0 ↔ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0)
3633, 35mpbi 230 . . . . . . 7 (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0
3736a1i 11 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0)
38 nn0ex 12530 . . . . . . 7 0 ∈ V
3938, 23elmap 8910 . . . . . 6 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ (ℕ0m ℙ) ↔ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0)
4037, 39sylibr 234 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ (ℕ0m ℙ))
41 fzfi 14010 . . . . . 6 (1...𝑁) ∈ Fin
42 ffn 6737 . . . . . . . . . . 11 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)):ℙ⟶ℕ0 → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) Fn ℙ)
43 elpreima 7078 . . . . . . . . . . 11 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) Fn ℙ → (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ↔ (𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ)))
4436, 42, 43mp2b 10 . . . . . . . . . 10 (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ↔ (𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ))
45 elequ1 2113 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝑘𝑧𝑥𝑧))
4645ifbid 4554 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → if(𝑘𝑧, 1, 0) = if(𝑥𝑧, 1, 0))
4730, 31ifcli 4578 . . . . . . . . . . . . . 14 if(𝑥𝑧, 1, 0) ∈ ℕ0
4847elexi 3501 . . . . . . . . . . . . 13 if(𝑥𝑧, 1, 0) ∈ V
4946, 34, 48fvmpt 7016 . . . . . . . . . . . 12 (𝑥 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) = if(𝑥𝑧, 1, 0))
5049eleq1d 2824 . . . . . . . . . . 11 (𝑥 ∈ ℙ → (((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ ↔ if(𝑥𝑧, 1, 0) ∈ ℕ))
5150biimpa 476 . . . . . . . . . 10 ((𝑥 ∈ ℙ ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑥) ∈ ℕ) → if(𝑥𝑧, 1, 0) ∈ ℕ)
5244, 51sylbi 217 . . . . . . . . 9 (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) → if(𝑥𝑧, 1, 0) ∈ ℕ)
53 0nnn 12300 . . . . . . . . . . 11 ¬ 0 ∈ ℕ
54 iffalse 4540 . . . . . . . . . . . 12 𝑥𝑧 → if(𝑥𝑧, 1, 0) = 0)
5554eleq1d 2824 . . . . . . . . . . 11 𝑥𝑧 → (if(𝑥𝑧, 1, 0) ∈ ℕ ↔ 0 ∈ ℕ))
5653, 55mtbiri 327 . . . . . . . . . 10 𝑥𝑧 → ¬ if(𝑥𝑧, 1, 0) ∈ ℕ)
5756con4i 114 . . . . . . . . 9 (if(𝑥𝑧, 1, 0) ∈ ℕ → 𝑥𝑧)
5852, 57syl 17 . . . . . . . 8 (𝑥 ∈ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) → 𝑥𝑧)
5958ssriv 3999 . . . . . . 7 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ⊆ 𝑧
60 elpwi 4612 . . . . . . . . 9 (𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
6160adantl 481 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑧 ⊆ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
62 prmssnn 16710 . . . . . . . . . 10 ℙ ⊆ ℕ
63 rabss2 4088 . . . . . . . . . 10 (ℙ ⊆ ℕ → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝𝑁})
6462, 63ax-mp 5 . . . . . . . . 9 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ {𝑝 ∈ ℕ ∣ 𝑝𝑁}
65 dvdsssfz1 16352 . . . . . . . . . 10 (𝑁 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝𝑁} ⊆ (1...𝑁))
6665adantr 480 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → {𝑝 ∈ ℕ ∣ 𝑝𝑁} ⊆ (1...𝑁))
6764, 66sstrid 4007 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ (1...𝑁))
6861, 67sstrd 4006 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑧 ⊆ (1...𝑁))
6959, 68sstrid 4007 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁))
70 ssfi 9212 . . . . . 6 (((1...𝑁) ∈ Fin ∧ ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ⊆ (1...𝑁)) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin)
7141, 69, 70sylancr 587 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) “ ℕ) ∈ Fin)
7229, 40, 71elrabd 3697 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin})
73 sqff1o.3 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
74 eqid 2735 . . . . . . 7 {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} = {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}
7573, 741arith 16961 . . . . . 6 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}
76 f1ocnv 6861 . . . . . 6 (𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} → 𝐺:{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ)
77 f1of 6849 . . . . . 6 (𝐺:{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}–1-1-onto→ℕ → 𝐺:{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}⟶ℕ)
7875, 76, 77mp2b 10 . . . . 5 𝐺:{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}⟶ℕ
7978ffvelcdmi 7103 . . . 4 ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ)
8072, 79syl 17 . . 3 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ)
81 f1ocnvfv2 7297 . . . . . . . . . . . 12 ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} ∧ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}) → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))
8275, 72, 81sylancr 587 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))
83731arithlem1 16957 . . . . . . . . . . . 12 ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))))
8480, 83syl 17 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))))
8582, 84eqtr3d 2777 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))))
8685fveq1d 6909 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑞) = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞))
87 elequ1 2113 . . . . . . . . . . 11 (𝑘 = 𝑞 → (𝑘𝑧𝑞𝑧))
8887ifbid 4554 . . . . . . . . . 10 (𝑘 = 𝑞 → if(𝑘𝑧, 1, 0) = if(𝑞𝑧, 1, 0))
8930, 31ifcli 4578 . . . . . . . . . . 11 if(𝑞𝑧, 1, 0) ∈ ℕ0
9089elexi 3501 . . . . . . . . . 10 if(𝑞𝑧, 1, 0) ∈ V
9188, 34, 90fvmpt 7016 . . . . . . . . 9 (𝑞 ∈ ℙ → ((𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))‘𝑞) = if(𝑞𝑧, 1, 0))
9286, 91sylan9req 2796 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞) = if(𝑞𝑧, 1, 0))
93 oveq1 7438 . . . . . . . . . 10 (𝑝 = 𝑞 → (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
94 eqid 2735 . . . . . . . . . 10 (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
95 ovex 7464 . . . . . . . . . 10 (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ∈ V
9693, 94, 95fvmpt 7016 . . . . . . . . 9 (𝑞 ∈ ℙ → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
9796adantl 481 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))‘𝑞) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
9892, 97eqtr3d 2777 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞𝑧, 1, 0) = (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
99 breq1 5151 . . . . . . . 8 (1 = if(𝑞𝑧, 1, 0) → (1 ≤ 1 ↔ if(𝑞𝑧, 1, 0) ≤ 1))
100 breq1 5151 . . . . . . . 8 (0 = if(𝑞𝑧, 1, 0) → (0 ≤ 1 ↔ if(𝑞𝑧, 1, 0) ≤ 1))
101 1le1 11889 . . . . . . . 8 1 ≤ 1
102 0le1 11784 . . . . . . . 8 0 ≤ 1
10399, 100, 101, 102keephyp 4602 . . . . . . 7 if(𝑞𝑧, 1, 0) ≤ 1
10498, 103eqbrtrrdi 5188 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1)
105104ralrimiva 3144 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1)
106 issqf 27194 . . . . . 6 ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ → ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1))
10780, 106syl 17 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ 1))
108105, 107mpbird 257 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0)
109 iftrue 4537 . . . . . . . . . . . 12 (𝑞𝑧 → if(𝑞𝑧, 1, 0) = 1)
110109adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → if(𝑞𝑧, 1, 0) = 1)
11161sselda 3995 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝑁})
112 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑁𝑞𝑁))
113112elrab 3695 . . . . . . . . . . . . . . 15 (𝑞 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝑁} ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑁))
114111, 113sylib 218 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → (𝑞 ∈ ℙ ∧ 𝑞𝑁))
115114simprd 495 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑞𝑁)
116114simpld 494 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑞 ∈ ℙ)
117 simpll 767 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 𝑁 ∈ ℕ)
118 pcelnn 16904 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞𝑁))
119116, 117, 118syl2anc 584 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → ((𝑞 pCnt 𝑁) ∈ ℕ ↔ 𝑞𝑁))
120115, 119mpbird 257 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → (𝑞 pCnt 𝑁) ∈ ℕ)
121120nnge1d 12312 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → 1 ≤ (𝑞 pCnt 𝑁))
122110, 121eqbrtrd 5170 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞𝑧) → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))
123122ex 412 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝑞𝑧 → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)))
124123adantr 480 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞𝑧 → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)))
125 simpr 484 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ)
12617ad2antrr 726 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → 𝑁 ∈ ℤ)
127 pcge0 16896 . . . . . . . . . 10 ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑞 pCnt 𝑁))
128125, 126, 127syl2anc 584 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → 0 ≤ (𝑞 pCnt 𝑁))
129 iffalse 4540 . . . . . . . . . 10 𝑞𝑧 → if(𝑞𝑧, 1, 0) = 0)
130129breq1d 5158 . . . . . . . . 9 𝑞𝑧 → (if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁) ↔ 0 ≤ (𝑞 pCnt 𝑁)))
131128, 130syl5ibrcom 247 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (¬ 𝑞𝑧 → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁)))
132124, 131pm2.61d 179 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → if(𝑞𝑧, 1, 0) ≤ (𝑞 pCnt 𝑁))
13398, 132eqbrtrrd 5172 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))
134133ralrimiva 3144 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁))
13580nnzd 12638 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℤ)
13617adantr 480 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → 𝑁 ∈ ℤ)
137 pc2dvds 16913 . . . . . 6 (((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)))
138135, 136, 137syl2anc 584 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≤ (𝑞 pCnt 𝑁)))
139134, 138mpbird 257 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁)
140108, 139jca 511 . . 3 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ∧ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁))
141 fveq2 6907 . . . . . 6 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → (μ‘𝑥) = (μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
142141neeq1d 2998 . . . . 5 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → ((μ‘𝑥) ≠ 0 ↔ (μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0))
143 breq1 5151 . . . . 5 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → (𝑥𝑁 ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁))
144142, 143anbi12d 632 . . . 4 (𝑥 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) → (((μ‘𝑥) ≠ 0 ∧ 𝑥𝑁) ↔ ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ∧ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁)))
145144, 6elrab2 3698 . . 3 ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ 𝑆 ↔ ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ ℕ ∧ ((μ‘(𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))) ≠ 0 ∧ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∥ 𝑁)))
14680, 140, 145sylanbrc 583 . 2 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁}) → (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ∈ 𝑆)
147 eqcom 2742 . . 3 (𝑛 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛)
1487simplbi 497 . . . . . . 7 (𝑛𝑆𝑛 ∈ ℕ)
149148ad2antrl 728 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑛 ∈ ℕ)
15023mptex 7243 . . . . . 6 (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V
15173fvmpt2 7027 . . . . . 6 ((𝑛 ∈ ℕ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V) → (𝐺𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
152149, 150, 151sylancl 586 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝐺𝑛) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
153152eqeq1d 2737 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝐺𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))))
15475a1i 11 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin})
15572adantrl 716 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin})
156 f1ocnvfvb 7299 . . . . 5 ((𝐺:ℕ–1-1-onto→{𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin} ∧ 𝑛 ∈ ℕ ∧ (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ∈ {𝑦 ∈ (ℕ0m ℙ) ∣ (𝑦 “ ℕ) ∈ Fin}) → ((𝐺𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛))
157154, 149, 155, 156syl3anc 1370 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝐺𝑛) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛))
15823a1i 11 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ℙ ∈ V)
159 0cnd 11252 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 0 ∈ ℂ)
160 1cnd 11254 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 1 ∈ ℂ)
161 0ne1 12335 . . . . . . . 8 0 ≠ 1
162161a1i 11 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 0 ≠ 1)
163158, 159, 160, 162pw2f1olem 9115 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ) ∧ 𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}))))
164 ssrab2 4090 . . . . . . . . 9 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ ℙ
165164sspwi 4617 . . . . . . . 8 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁} ⊆ 𝒫 ℙ
166 simprr 773 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
167165, 166sselid 3993 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → 𝑧 ∈ 𝒫 ℙ)
168167biantrurd 532 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ (𝑧 ∈ 𝒫 ℙ ∧ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)))))
169 id 22 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
170148adantl 481 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → 𝑛 ∈ ℕ)
171 pccl 16883 . . . . . . . . . . . . . . 15 ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → (𝑝 pCnt 𝑛) ∈ ℕ0)
172169, 170, 171syl2anr 597 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈ ℕ0)
173 elnn0 12526 . . . . . . . . . . . . . 14 ((𝑝 pCnt 𝑛) ∈ ℕ0 ↔ ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0))
174172, 173sylib 218 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ∨ (𝑝 pCnt 𝑛) = 0))
175174orcomd 871 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ))
1768simpld 494 . . . . . . . . . . . . . . . . 17 (𝑛𝑆 → (μ‘𝑛) ≠ 0)
177176adantl 481 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → (μ‘𝑛) ≠ 0)
178 issqf 27194 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((μ‘𝑛) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1))
179170, 178syl 17 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → ((μ‘𝑛) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1))
180177, 179mpbid 232 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑛) ≤ 1)
181180r19.21bi 3249 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ≤ 1)
182 nnle1eq1 12294 . . . . . . . . . . . . . 14 ((𝑝 pCnt 𝑛) ∈ ℕ → ((𝑝 pCnt 𝑛) ≤ 1 ↔ (𝑝 pCnt 𝑛) = 1))
183181, 182syl5ibcom 245 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ → (𝑝 pCnt 𝑛) = 1))
184183orim2d 968 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) ∈ ℕ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1)))
185175, 184mpd 15 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1))
186 ovex 7464 . . . . . . . . . . . 12 (𝑝 pCnt 𝑛) ∈ V
187186elpr 4655 . . . . . . . . . . 11 ((𝑝 pCnt 𝑛) ∈ {0, 1} ↔ ((𝑝 pCnt 𝑛) = 0 ∨ (𝑝 pCnt 𝑛) = 1))
188185, 187sylibr 234 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑛) ∈ {0, 1})
189188fmpttd 7135 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1})
190189adantrr 717 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1})
191 prex 5443 . . . . . . . . 9 {0, 1} ∈ V
192191, 23elmap 8910 . . . . . . . 8 ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ) ↔ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)):ℙ⟶{0, 1})
193190, 192sylibr 234 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ))
194193biantrurd 532 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ ({0, 1} ↑m ℙ) ∧ 𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}))))
195163, 168, 1943bitr4d 311 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ 𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1})))
196 eqid 2735 . . . . . . . . 9 (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))
197196mptiniseg 6261 . . . . . . . 8 (1 ∈ ℕ0 → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1})
19830, 197ax-mp 5 . . . . . . 7 ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1}
199 id 22 . . . . . . . . . . . 12 ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) = 1)
200 1nn 12275 . . . . . . . . . . . 12 1 ∈ ℕ
201199, 200eqeltrdi 2847 . . . . . . . . . . 11 ((𝑝 pCnt 𝑛) = 1 → (𝑝 pCnt 𝑛) ∈ ℕ)
202201, 183impbid2 226 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ (𝑝 pCnt 𝑛) ∈ ℕ))
203 simpr 484 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
204 pcelnn 16904 . . . . . . . . . . 11 ((𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝𝑛))
205203, 15, 204syl2anc 584 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) ∈ ℕ ↔ 𝑝𝑛))
206202, 205bitrd 279 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛𝑆) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝑛) = 1 ↔ 𝑝𝑛))
207206rabbidva 3440 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑛𝑆) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝𝑛})
208207adantrr 717 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → {𝑝 ∈ ℙ ∣ (𝑝 pCnt 𝑛) = 1} = {𝑝 ∈ ℙ ∣ 𝑝𝑛})
209198, 208eqtrid 2787 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) = {𝑝 ∈ ℙ ∣ 𝑝𝑛})
210209eqeq2d 2746 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑧 = ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) “ {1}) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
211195, 210bitrd 279 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) = (𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0)) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
212153, 157, 2113bitr3d 309 . . 3 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → ((𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) = 𝑛𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
213147, 212bitrid 283 . 2 ((𝑁 ∈ ℕ ∧ (𝑛𝑆𝑧 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})) → (𝑛 = (𝐺‘(𝑘 ∈ ℙ ↦ if(𝑘𝑧, 1, 0))) ↔ 𝑧 = {𝑝 ∈ ℙ ∣ 𝑝𝑛}))
2141, 26, 146, 213f1o2d 7687 1 (𝑁 ∈ ℕ → 𝐹:𝑆1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝𝑁})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wne 2938  wral 3059  {crab 3433  Vcvv 3478  wss 3963  ifcif 4531  𝒫 cpw 4605  {csn 4631  {cpr 4633   class class class wbr 5148  cmpt 5231  ccnv 5688  cima 5692   Fn wfn 6558  wf 6559  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  m cmap 8865  Fincfn 8984  cc 11151  0cc0 11153  1c1 11154  cle 11294  cn 12264  0cn0 12524  cz 12611  ...cfz 13544  cdvds 16287  cprime 16705   pCnt cpc 16870  μcmu 27153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-q 12989  df-rp 13033  df-fz 13545  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-dvds 16288  df-gcd 16529  df-prm 16706  df-pc 16871  df-mu 27159
This theorem is referenced by:  musum  27249
  Copyright terms: Public domain W3C validator