Metamath Proof Explorer

Theorem sqff1o

Description: There is a bijection from the squarefree divisors of a number N to the powerset of the prime divisors of N . Among other things, this implies that a number has 2 ^ k squarefree divisors where k is the number of prime divisors, and a squarefree number has 2 ^ k divisors (because all divisors of a squarefree number are squarefree). The inverse function to F takes the product of all the primes in some subset of prime divisors of N . (Contributed by Mario Carneiro, 1-Jul-2015)

Ref Expression
Hypotheses sqff1o.1 ⊢ 𝑆 = { 𝑥 ∈ ℕ ∣ ( ( μ ‘ 𝑥 ) ≠ 0 ∧ 𝑥 ∥ 𝑁 ) }
sqff1o.2 ⊢ 𝐹 = ( 𝑛 ∈ 𝑆 ↦ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } )
sqff1o.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
Assertion sqff1o ( 𝑁 ∈ ℕ → 𝐹 : 𝑆 –1-1-onto→ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )

Proof

Step Hyp Ref Expression
1 sqff1o.1 ⊢ 𝑆 = { 𝑥 ∈ ℕ ∣ ( ( μ ‘ 𝑥 ) ≠ 0 ∧ 𝑥 ∥ 𝑁 ) }
2 sqff1o.2 ⊢ 𝐹 = ( 𝑛 ∈ 𝑆 ↦ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } )
3 sqff1o.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
4 fveq2 ⊢ ( 𝑥 = 𝑛 → ( μ ‘ 𝑥 ) = ( μ ‘ 𝑛 ) )
5 4 neeq1d ⊢ ( 𝑥 = 𝑛 → ( ( μ ‘ 𝑥 ) ≠ 0 ↔ ( μ ‘ 𝑛 ) ≠ 0 ) )
6 breq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁 ) )
7 5 6 anbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ( μ ‘ 𝑥 ) ≠ 0 ∧ 𝑥 ∥ 𝑁 ) ↔ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛 ∥ 𝑁 ) ) )
8 7 1 elrab2 ⊢ ( 𝑛 ∈ 𝑆 ↔ ( 𝑛 ∈ ℕ ∧ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛 ∥ 𝑁 ) ) )
9 8 simprbi ⊢ ( 𝑛 ∈ 𝑆 → ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛 ∥ 𝑁 ) )
10 9 simprd ⊢ ( 𝑛 ∈ 𝑆 → 𝑛 ∥ 𝑁 )
11 10 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑛 ∥ 𝑁 )
12 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
13 12 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
14 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑛 ∈ 𝑆 )
15 14 8 sylib ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑛 ∈ ℕ ∧ ( ( μ ‘ 𝑛 ) ≠ 0 ∧ 𝑛 ∥ 𝑁 ) ) )
16 15 simpld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑛 ∈ ℕ )
17 16 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑛 ∈ ℤ )
18 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
19 18 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℤ )
20 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑝 ∥ 𝑛 ∧ 𝑛 ∥ 𝑁 ) → 𝑝 ∥ 𝑁 ) )
21 13 17 19 20 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝑛 ∧ 𝑛 ∥ 𝑁 ) → 𝑝 ∥ 𝑁 ) )
22 11 21 mpan2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑛 → 𝑝 ∥ 𝑁 ) )
23 22 ss2rabdv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ⊆ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
24 prmex ⊢ ℙ ∈ V
25 24 rabex ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ∈ V
26 25 elpw ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ⊆ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
27 23 26 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
28 cnveq ⊢ ( 𝑦 = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) → ◡ 𝑦 = ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) )
29 28 imaeq1d ⊢ ( 𝑦 = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) → ( ◡ 𝑦 “ ℕ ) = ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) )
30 29 eleq1d ⊢ ( 𝑦 = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) → ( ( ◡ 𝑦 “ ℕ ) ∈ Fin ↔ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ∈ Fin ) )
31 1nn0 ⊢ 1 ∈ ℕ0
32 0nn0 ⊢ 0 ∈ ℕ0
33 31 32 ifcli ⊢ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ∈ ℕ0
34 33 rgenw ⊢ ∀ 𝑘 ∈ ℙ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ∈ ℕ0
35 eqid ⊢ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) )
36 35 fmpt ⊢ ( ∀ 𝑘 ∈ ℙ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ∈ ℕ0 ↔ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) : ℙ ⟶ ℕ0 )
37 34 36 mpbi ⊢ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) : ℙ ⟶ ℕ0
38 37 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) : ℙ ⟶ ℕ0 )
39 nn0ex ⊢ ℕ0 ∈ V
40 39 24 elmap ⊢ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ ( ℕ0 ↑m ℙ ) ↔ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) : ℙ ⟶ ℕ0 )
41 38 40 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ ( ℕ0 ↑m ℙ ) )
42 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
43 ffn ⊢ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) : ℙ ⟶ ℕ0 → ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) Fn ℙ )
44 elpreima ⊢ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) Fn ℙ → ( 𝑥 ∈ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ↔ ( 𝑥 ∈ ℙ ∧ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑥 ) ∈ ℕ ) ) )
45 37 43 44 mp2b ⊢ ( 𝑥 ∈ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ↔ ( 𝑥 ∈ ℙ ∧ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑥 ) ∈ ℕ ) )
46 elequ1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
47 46 ifbid ⊢ ( 𝑘 = 𝑥 → if ( 𝑘 ∈ 𝑧 , 1 , 0 ) = if ( 𝑥 ∈ 𝑧 , 1 , 0 ) )
48 31 32 ifcli ⊢ if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ0
49 48 elexi ⊢ if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ V
50 47 35 49 fvmpt ⊢ ( 𝑥 ∈ ℙ → ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑧 , 1 , 0 ) )
51 50 eleq1d ⊢ ( 𝑥 ∈ ℙ → ( ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑥 ) ∈ ℕ ↔ if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ ) )
52 51 biimpa ⊢ ( ( 𝑥 ∈ ℙ ∧ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑥 ) ∈ ℕ ) → if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ )
53 45 52 sylbi ⊢ ( 𝑥 ∈ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) → if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ )
54 0nnn ⊢ ¬ 0 ∈ ℕ
55 iffalse ⊢ ( ¬ 𝑥 ∈ 𝑧 → if ( 𝑥 ∈ 𝑧 , 1 , 0 ) = 0 )
56 55 eleq1d ⊢ ( ¬ 𝑥 ∈ 𝑧 → ( if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ ↔ 0 ∈ ℕ ) )
57 54 56 mtbiri ⊢ ( ¬ 𝑥 ∈ 𝑧 → ¬ if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ )
58 57 con4i ⊢ ( if ( 𝑥 ∈ 𝑧 , 1 , 0 ) ∈ ℕ → 𝑥 ∈ 𝑧 )
59 53 58 syl ⊢ ( 𝑥 ∈ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) → 𝑥 ∈ 𝑧 )
60 59 ssriv ⊢ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ⊆ 𝑧
61 elpwi ⊢ ( 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } → 𝑧 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
62 61 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → 𝑧 ⊆ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
63 prmssnn ⊢ ℙ ⊆ ℕ
64 rabss2 ⊢ ( ℙ ⊆ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁 } )
65 63 64 ax-mp ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁 }
66 dvdsssfz1 ⊢ ( 𝑁 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
67 66 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
68 65 67 sstrid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
69 62 68 sstrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → 𝑧 ⊆ ( 1 ... 𝑁 ) )
70 60 69 sstrid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ⊆ ( 1 ... 𝑁 ) )
71 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ⊆ ( 1 ... 𝑁 ) ) → ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ∈ Fin )
72 42 70 71 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ◡ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) “ ℕ ) ∈ Fin )
73 30 41 72 elrabd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } )
74 eqid ⊢ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } = { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin }
75 3 74 1arith ⊢ 𝐺 : ℕ –1-1-onto→ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin }
76 f1ocnv ⊢ ( 𝐺 : ℕ –1-1-onto→ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } → ◡ 𝐺 : { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } –1-1-onto→ ℕ )
77 f1of ⊢ ( ◡ 𝐺 : { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } –1-1-onto→ ℕ → ◡ 𝐺 : { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } ⟶ ℕ )
78 75 76 77 mp2b ⊢ ◡ 𝐺 : { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } ⟶ ℕ
79 78 ffvelrni ⊢ ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } → ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℕ )
80 73 79 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℕ )
81 f1ocnvfv2 ⊢ ( ( 𝐺 : ℕ –1-1-onto→ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } ∧ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) )
82 75 73 81 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) )
83 3 1arithlem1 ⊢ ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℕ → ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) )
84 80 83 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) )
85 82 84 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) )
86 85 fveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑞 ) = ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) ‘ 𝑞 ) )
87 elequ1 ⊢ ( 𝑘 = 𝑞 → ( 𝑘 ∈ 𝑧 ↔ 𝑞 ∈ 𝑧 ) )
88 87 ifbid ⊢ ( 𝑘 = 𝑞 → if ( 𝑘 ∈ 𝑧 , 1 , 0 ) = if ( 𝑞 ∈ 𝑧 , 1 , 0 ) )
89 31 32 ifcli ⊢ if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ∈ ℕ0
90 89 elexi ⊢ if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ∈ V
91 88 35 90 fvmpt ⊢ ( 𝑞 ∈ ℙ → ( ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ‘ 𝑞 ) = if ( 𝑞 ∈ 𝑧 , 1 , 0 ) )
92 86 91 sylan9req ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) ‘ 𝑞 ) = if ( 𝑞 ∈ 𝑧 , 1 , 0 ) )
93 oveq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) = ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
94 eqid ⊢ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
95 ovex ⊢ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ∈ V
96 93 94 95 fvmpt ⊢ ( 𝑞 ∈ ℙ → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) ‘ 𝑞 ) = ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
97 96 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ) ‘ 𝑞 ) = ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
98 92 97 eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) = ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
99 breq1 ⊢ ( 1 = if ( 𝑞 ∈ 𝑧 , 1 , 0 ) → ( 1 ≤ 1 ↔ if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ 1 ) )
100 breq1 ⊢ ( 0 = if ( 𝑞 ∈ 𝑧 , 1 , 0 ) → ( 0 ≤ 1 ↔ if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ 1 ) )
101 1le1 ⊢ 1 ≤ 1
102 0le1 ⊢ 0 ≤ 1
103 99 100 101 102 keephyp ⊢ if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ 1
104 98 103 eqbrtrrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ 1 )
105 104 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ 1 )
106 issqf ⊢ ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℕ → ( ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ 1 ) )
107 80 106 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ 1 ) )
108 105 107 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 )
109 iftrue ⊢ ( 𝑞 ∈ 𝑧 → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) = 1 )
110 109 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) = 1 )
111 62 sselda ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → 𝑞 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
112 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁 ) )
113 112 elrab ⊢ ( 𝑞 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ↔ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁 ) )
114 111 113 sylib ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁 ) )
115 114 simprd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → 𝑞 ∥ 𝑁 )
116 114 simpld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → 𝑞 ∈ ℙ )
117 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → 𝑁 ∈ ℕ )
118 pcelnn ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑞 pCnt 𝑁 ) ∈ ℕ ↔ 𝑞 ∥ 𝑁 ) )
119 116 117 118 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → ( ( 𝑞 pCnt 𝑁 ) ∈ ℕ ↔ 𝑞 ∥ 𝑁 ) )
120 115 119 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → ( 𝑞 pCnt 𝑁 ) ∈ ℕ )
121 120 nnge1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → 1 ≤ ( 𝑞 pCnt 𝑁 ) )
122 110 121 eqbrtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ 𝑧 ) → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ ( 𝑞 pCnt 𝑁 ) )
123 122 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( 𝑞 ∈ 𝑧 → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ ( 𝑞 pCnt 𝑁 ) ) )
124 123 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∈ 𝑧 → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ ( 𝑞 pCnt 𝑁 ) ) )
125 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ℙ )
126 18 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → 𝑁 ∈ ℤ )
127 pcge0 ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → 0 ≤ ( 𝑞 pCnt 𝑁 ) )
128 125 126 127 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → 0 ≤ ( 𝑞 pCnt 𝑁 ) )
129 iffalse ⊢ ( ¬ 𝑞 ∈ 𝑧 → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) = 0 )
130 129 breq1d ⊢ ( ¬ 𝑞 ∈ 𝑧 → ( if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ ( 𝑞 pCnt 𝑁 ) ↔ 0 ≤ ( 𝑞 pCnt 𝑁 ) ) )
131 128 130 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → ( ¬ 𝑞 ∈ 𝑧 → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ ( 𝑞 pCnt 𝑁 ) ) )
132 124 131 pm2.61d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → if ( 𝑞 ∈ 𝑧 , 1 , 0 ) ≤ ( 𝑞 pCnt 𝑁 ) )
133 98 132 eqbrtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ ( 𝑞 pCnt 𝑁 ) )
134 133 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ ( 𝑞 pCnt 𝑁 ) )
135 80 nnzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℤ )
136 18 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → 𝑁 ∈ ℤ )
137 pc2dvds ⊢ ( ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ ( 𝑞 pCnt 𝑁 ) ) )
138 135 136 137 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≤ ( 𝑞 pCnt 𝑁 ) ) )
139 134 138 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 )
140 108 139 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 ∧ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 ) )
141 fveq2 ⊢ ( 𝑥 = ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) → ( μ ‘ 𝑥 ) = ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
142 141 neeq1d ⊢ ( 𝑥 = ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) → ( ( μ ‘ 𝑥 ) ≠ 0 ↔ ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 ) )
143 breq1 ⊢ ( 𝑥 = ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) → ( 𝑥 ∥ 𝑁 ↔ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 ) )
144 142 143 anbi12d ⊢ ( 𝑥 = ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) → ( ( ( μ ‘ 𝑥 ) ≠ 0 ∧ 𝑥 ∥ 𝑁 ) ↔ ( ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 ∧ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 ) ) )
145 144 1 elrab2 ⊢ ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ 𝑆 ↔ ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ ℕ ∧ ( ( μ ‘ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) ≠ 0 ∧ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∥ 𝑁 ) ) )
146 80 140 145 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) → ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ∈ 𝑆 )
147 eqcom ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) = 𝑛 )
148 8 simplbi ⊢ ( 𝑛 ∈ 𝑆 → 𝑛 ∈ ℕ )
149 148 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 𝑛 ∈ ℕ )
150 24 mptex ⊢ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ V
151 3 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
152 149 150 151 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝐺 ‘ 𝑛 ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
153 152 eqeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( 𝐺 ‘ 𝑛 ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ↔ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) )
154 75 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 𝐺 : ℕ –1-1-onto→ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } )
155 73 adantrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } )
156 f1ocnvfvb ⊢ ( ( 𝐺 : ℕ –1-1-onto→ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } ∧ 𝑛 ∈ ℕ ∧ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ∈ { 𝑦 ∈ ( ℕ0 ↑m ℙ ) ∣ ( ◡ 𝑦 “ ℕ ) ∈ Fin } ) → ( ( 𝐺 ‘ 𝑛 ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) = 𝑛 ) )
157 154 149 155 156 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( 𝐺 ‘ 𝑛 ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) = 𝑛 ) )
158 24 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ℙ ∈ V )
159 0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 0 ∈ ℂ )
160 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 1 ∈ ℂ )
161 0ne1 ⊢ 0 ≠ 1
162 161 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 0 ≠ 1 )
163 158 159 160 162 pw2f1olem ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( 𝑧 ∈ 𝒫 ℙ ∧ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ↔ ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ ( { 0 , 1 } ↑m ℙ ) ∧ 𝑧 = ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) ) ) )
164 ssrab2 ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ⊆ ℙ
165 164 sspwi ⊢ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ⊆ 𝒫 ℙ
166 simprr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )
167 165 166 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → 𝑧 ∈ 𝒫 ℙ )
168 167 biantrurd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ↔ ( 𝑧 ∈ 𝒫 ℙ ∧ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ) )
169 id ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℙ )
170 148 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → 𝑛 ∈ ℕ )
171 pccl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ ) → ( 𝑝 pCnt 𝑛 ) ∈ ℕ0 )
172 169 170 171 syl2anr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑛 ) ∈ ℕ0 )
173 elnn0 ⊢ ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ0 ↔ ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ ∨ ( 𝑝 pCnt 𝑛 ) = 0 ) )
174 172 173 sylib ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ ∨ ( 𝑝 pCnt 𝑛 ) = 0 ) )
175 174 orcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) = 0 ∨ ( 𝑝 pCnt 𝑛 ) ∈ ℕ ) )
176 9 simpld ⊢ ( 𝑛 ∈ 𝑆 → ( μ ‘ 𝑛 ) ≠ 0 )
177 176 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → ( μ ‘ 𝑛 ) ≠ 0 )
178 issqf ⊢ ( 𝑛 ∈ ℕ → ( ( μ ‘ 𝑛 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑛 ) ≤ 1 ) )
179 170 178 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → ( ( μ ‘ 𝑛 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑛 ) ≤ 1 ) )
180 177 179 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑛 ) ≤ 1 )
181 180 r19.21bi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑛 ) ≤ 1 )
182 nnle1eq1 ⊢ ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ → ( ( 𝑝 pCnt 𝑛 ) ≤ 1 ↔ ( 𝑝 pCnt 𝑛 ) = 1 ) )
183 181 182 syl5ibcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ → ( 𝑝 pCnt 𝑛 ) = 1 ) )
184 183 orim2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝑛 ) = 0 ∨ ( 𝑝 pCnt 𝑛 ) ∈ ℕ ) → ( ( 𝑝 pCnt 𝑛 ) = 0 ∨ ( 𝑝 pCnt 𝑛 ) = 1 ) ) )
185 175 184 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) = 0 ∨ ( 𝑝 pCnt 𝑛 ) = 1 ) )
186 ovex ⊢ ( 𝑝 pCnt 𝑛 ) ∈ V
187 186 elpr ⊢ ( ( 𝑝 pCnt 𝑛 ) ∈ { 0 , 1 } ↔ ( ( 𝑝 pCnt 𝑛 ) = 0 ∨ ( 𝑝 pCnt 𝑛 ) = 1 ) )
188 185 187 sylibr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑛 ) ∈ { 0 , 1 } )
189 188 fmpttd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) : ℙ ⟶ { 0 , 1 } )
190 189 adantrr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) : ℙ ⟶ { 0 , 1 } )
191 prex ⊢ { 0 , 1 } ∈ V
192 191 24 elmap ⊢ ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ ( { 0 , 1 } ↑m ℙ ) ↔ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) : ℙ ⟶ { 0 , 1 } )
193 190 192 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ ( { 0 , 1 } ↑m ℙ ) )
194 193 biantrurd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝑧 = ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) ↔ ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) ∈ ( { 0 , 1 } ↑m ℙ ) ∧ 𝑧 = ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) ) ) )
195 163 168 194 3bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ↔ 𝑧 = ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) ) )
196 eqid ⊢ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) )
197 196 mptiniseg ⊢ ( 1 ∈ ℕ0 → ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) = { 𝑝 ∈ ℙ ∣ ( 𝑝 pCnt 𝑛 ) = 1 } )
198 31 197 ax-mp ⊢ ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) = { 𝑝 ∈ ℙ ∣ ( 𝑝 pCnt 𝑛 ) = 1 }
199 id ⊢ ( ( 𝑝 pCnt 𝑛 ) = 1 → ( 𝑝 pCnt 𝑛 ) = 1 )
200 1nn ⊢ 1 ∈ ℕ
201 199 200 eqeltrdi ⊢ ( ( 𝑝 pCnt 𝑛 ) = 1 → ( 𝑝 pCnt 𝑛 ) ∈ ℕ )
202 201 183 impbid2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) = 1 ↔ ( 𝑝 pCnt 𝑛 ) ∈ ℕ ) )
203 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
204 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ ↔ 𝑝 ∥ 𝑛 ) )
205 203 16 204 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) ∈ ℕ ↔ 𝑝 ∥ 𝑛 ) )
206 202 205 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝑛 ) = 1 ↔ 𝑝 ∥ 𝑛 ) )
207 206 rabbidva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ 𝑆 ) → { 𝑝 ∈ ℙ ∣ ( 𝑝 pCnt 𝑛 ) = 1 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } )
208 207 adantrr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → { 𝑝 ∈ ℙ ∣ ( 𝑝 pCnt 𝑛 ) = 1 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } )
209 198 208 eqtrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } )
210 209 eqeq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝑧 = ( ◡ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) “ { 1 } ) ↔ 𝑧 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ) )
211 195 210 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ↔ 𝑧 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ) )
212 153 157 211 3bitr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) = 𝑛 ↔ 𝑧 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ) )
213 147 212 syl5bb ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 ∈ 𝑆 ∧ 𝑧 ∈ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } ) ) → ( 𝑛 = ( ◡ 𝐺 ‘ ( 𝑘 ∈ ℙ ↦ if ( 𝑘 ∈ 𝑧 , 1 , 0 ) ) ) ↔ 𝑧 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑛 } ) )
214 2 27 146 213 f1o2d ⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝑆 –1-1-onto→ 𝒫 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁 } )