Metamath Proof Explorer

Theorem prmreclem2

Description: Lemma for prmrec . There are at most 2 ^ K squarefree numbers which divide no primes larger than K . (We could strengthen this to 2 ^ # ( Prime i^i ( 1 ... K ) ) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to K completely determine it because all higher prime counts are zero, and they are all at most 1 because no square divides the number, so there are at most 2 ^ K possibilities. (Contributed by Mario Carneiro, 5-Aug-2014)

Ref Expression
Hypotheses prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
prmreclem2.5 ⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
Assertion prmreclem2 ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( 2 ↑ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
2 prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
5 prmreclem2.5 ⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
6 ovex ⊢ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ∈ V
7 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑄 ‘ 𝑥 ) = 1 ↔ ( 𝑄 ‘ 𝑦 ) = 1 ) )
8 7 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ↔ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) )
9 4 ssrab3 ⊢ 𝑀 ⊆ ( 1 ... 𝑁 )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) → 𝑦 ∈ 𝑀 )
11 10 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑦 ∈ 𝑀 )
12 9 11 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑦 ∈ ( 1 ... 𝑁 ) )
13 elfznn ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ∈ ℕ )
14 12 13 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑦 ∈ ℕ )
15 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑛 ∈ ℙ )
16 prmuz2 ⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ( ℤ≥ ‘ 2 ) )
17 15 16 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑛 ∈ ( ℤ≥ ‘ 2 ) )
18 5 prmreclem1 ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
19 18 simp3d ⊢ ( 𝑦 ∈ ℕ → ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
20 14 17 19 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ¬ ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) → ( 𝑄 ‘ 𝑦 ) = 1 )
22 21 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑄 ‘ 𝑦 ) = 1 )
23 22 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( 1 ↑ 2 ) )
24 sq1 ⊢ ( 1 ↑ 2 ) = 1
25 23 24 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = 1 )
26 25 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑦 / 1 ) )
27 14 nncnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑦 ∈ ℂ )
28 27 div1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑦 / 1 ) = 𝑦 )
29 26 28 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = 𝑦 )
30 29 breq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ↔ ( 𝑛 ↑ 2 ) ∥ 𝑦 ) )
31 14 nnzd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 𝑦 ∈ ℤ )
32 2nn0 ⊢ 2 ∈ ℕ0
33 32 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → 2 ∈ ℕ0 )
34 pcdvdsb ⊢ ( ( 𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 2 ≤ ( 𝑛 pCnt 𝑦 ) ↔ ( 𝑛 ↑ 2 ) ∥ 𝑦 ) )
35 15 31 33 34 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 2 ≤ ( 𝑛 pCnt 𝑦 ) ↔ ( 𝑛 ↑ 2 ) ∥ 𝑦 ) )
36 30 35 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ↔ 2 ≤ ( 𝑛 pCnt 𝑦 ) ) )
37 20 36 mtbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ¬ 2 ≤ ( 𝑛 pCnt 𝑦 ) )
38 15 14 pccld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ ℕ0 )
39 38 nn0red ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ ℝ )
40 2re ⊢ 2 ∈ ℝ
41 ltnle ⊢ ( ( ( 𝑛 pCnt 𝑦 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝑛 pCnt 𝑦 ) < 2 ↔ ¬ 2 ≤ ( 𝑛 pCnt 𝑦 ) ) )
42 39 40 41 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 pCnt 𝑦 ) < 2 ↔ ¬ 2 ≤ ( 𝑛 pCnt 𝑦 ) ) )
43 37 42 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) < 2 )
44 df-2 ⊢ 2 = ( 1 + 1 )
45 43 44 breqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) < ( 1 + 1 ) )
46 38 nn0zd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ ℤ )
47 1z ⊢ 1 ∈ ℤ
48 zleltp1 ⊢ ( ( ( 𝑛 pCnt 𝑦 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑛 pCnt 𝑦 ) ≤ 1 ↔ ( 𝑛 pCnt 𝑦 ) < ( 1 + 1 ) ) )
49 46 47 48 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 pCnt 𝑦 ) ≤ 1 ↔ ( 𝑛 pCnt 𝑦 ) < ( 1 + 1 ) ) )
50 45 49 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ≤ 1 )
51 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
52 38 51 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ ( ℤ≥ ‘ 0 ) )
53 elfz5 ⊢ ( ( ( 𝑛 pCnt 𝑦 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 1 ∈ ℤ ) → ( ( 𝑛 pCnt 𝑦 ) ∈ ( 0 ... 1 ) ↔ ( 𝑛 pCnt 𝑦 ) ≤ 1 ) )
54 52 47 53 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 pCnt 𝑦 ) ∈ ( 0 ... 1 ) ↔ ( 𝑛 pCnt 𝑦 ) ≤ 1 ) )
55 50 54 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ ( 0 ... 1 ) )
56 0z ⊢ 0 ∈ ℤ
57 fzpr ⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
58 56 57 ax-mp ⊢ ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
59 1e0p1 ⊢ 1 = ( 0 + 1 )
60 59 oveq2i ⊢ ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
61 59 preq2i ⊢ { 0 , 1 } = { 0 , ( 0 + 1 ) }
62 58 60 61 3eqtr4i ⊢ ( 0 ... 1 ) = { 0 , 1 }
63 55 62 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ { 0 , 1 } )
64 c0ex ⊢ 0 ∈ V
65 64 prid1 ⊢ 0 ∈ { 0 , 1 }
66 65 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑛 ∈ ℙ ) → 0 ∈ { 0 , 1 } )
67 63 66 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ∈ { 0 , 1 } )
68 67 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) : ( 1 ... 𝐾 ) ⟶ { 0 , 1 } )
69 prex ⊢ { 0 , 1 } ∈ V
70 ovex ⊢ ( 1 ... 𝐾 ) ∈ V
71 69 70 elmap ⊢ ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) : ( 1 ... 𝐾 ) ⟶ { 0 , 1 } )
72 68 71 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) )
73 72 ex ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
74 8 73 syl5bi ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
75 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑄 ‘ 𝑥 ) = 1 ↔ ( 𝑄 ‘ 𝑧 ) = 1 ) )
76 75 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) )
77 8 76 anbi12i ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∧ 𝑧 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ↔ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) )
78 ovex ⊢ ( 𝑛 pCnt 𝑦 ) ∈ V
79 78 64 ifex ⊢ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ∈ V
80 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) )
81 79 80 fnmpti ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) Fn ( 1 ... 𝐾 )
82 ovex ⊢ ( 𝑛 pCnt 𝑧 ) ∈ V
83 82 64 ifex ⊢ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ∈ V
84 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) )
85 83 84 fnmpti ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) Fn ( 1 ... 𝐾 )
86 eqfnfv ⊢ ( ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) Fn ( 1 ... 𝐾 ) ∧ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) Fn ( 1 ... 𝐾 ) ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) ) )
87 81 85 86 mp2an ⊢ ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) )
88 eleq1w ⊢ ( 𝑛 = 𝑝 → ( 𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ ) )
89 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑦 ) )
90 88 89 ifbieq1d ⊢ ( 𝑛 = 𝑝 → if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) )
91 ovex ⊢ ( 𝑝 pCnt 𝑦 ) ∈ V
92 91 64 ifex ⊢ if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) ∈ V
93 90 80 92 fvmpt ⊢ ( 𝑝 ∈ ( 1 ... 𝐾 ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) )
94 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 pCnt 𝑧 ) = ( 𝑝 pCnt 𝑧 ) )
95 88 94 ifbieq1d ⊢ ( 𝑛 = 𝑝 → if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
96 ovex ⊢ ( 𝑝 pCnt 𝑧 ) ∈ V
97 96 64 ifex ⊢ if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∈ V
98 95 84 97 fvmpt ⊢ ( 𝑝 ∈ ( 1 ... 𝐾 ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
99 93 98 eqeq12d ⊢ ( 𝑝 ∈ ( 1 ... 𝐾 ) → ( ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) ↔ if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
100 99 ralbiia ⊢ ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
101 87 100 bitri ⊢ ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
102 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ 𝑀 )
103 breq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦 ) )
104 103 notbid ⊢ ( 𝑛 = 𝑦 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦 ) )
105 104 ralbidv ⊢ ( 𝑛 = 𝑦 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
106 105 4 elrab2 ⊢ ( 𝑦 ∈ 𝑀 ↔ ( 𝑦 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
107 106 simprbi ⊢ ( 𝑦 ∈ 𝑀 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 )
108 102 107 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 )
109 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑧 ∈ 𝑀 )
110 breq2 ⊢ ( 𝑛 = 𝑧 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧 ) )
111 110 notbid ⊢ ( 𝑛 = 𝑧 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧 ) )
112 111 ralbidv ⊢ ( 𝑛 = 𝑧 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) )
113 112 4 elrab2 ⊢ ( 𝑧 ∈ 𝑀 ↔ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) )
114 113 simprbi ⊢ ( 𝑧 ∈ 𝑀 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 )
115 109 114 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 )
116 r19.26 ⊢ ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) )
117 eldifi ⊢ ( 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℙ )
118 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
119 9 118 sstri ⊢ 𝑀 ⊆ ℕ
120 119 102 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ ℕ )
121 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑦 ) = 0 ↔ ¬ 𝑝 ∥ 𝑦 ) )
122 117 120 121 syl2anr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 pCnt 𝑦 ) = 0 ↔ ¬ 𝑝 ∥ 𝑦 ) )
123 119 109 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑧 ∈ ℕ )
124 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑧 ) = 0 ↔ ¬ 𝑝 ∥ 𝑧 ) )
125 117 123 124 syl2anr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 pCnt 𝑧 ) = 0 ↔ ¬ 𝑝 ∥ 𝑧 ) )
126 122 125 anbi12d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( ( 𝑝 pCnt 𝑦 ) = 0 ∧ ( 𝑝 pCnt 𝑧 ) = 0 ) ↔ ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) ) )
127 eqtr3 ⊢ ( ( ( 𝑝 pCnt 𝑦 ) = 0 ∧ ( 𝑝 pCnt 𝑧 ) = 0 ) → ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
128 126 127 syl6bir ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) → ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
129 128 ralimdva ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
130 116 129 syl5bir ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
131 108 115 130 mp2and ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
132 131 biantrud ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) ) )
133 incom ⊢ ( ℙ ∩ ( 1 ... 𝐾 ) ) = ( ( 1 ... 𝐾 ) ∩ ℙ )
134 133 uneq1i ⊢ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) = ( ( ( 1 ... 𝐾 ) ∩ ℙ ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) )
135 inundif ⊢ ( ( ( 1 ... 𝐾 ) ∩ ℙ ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) = ( 1 ... 𝐾 )
136 134 135 eqtri ⊢ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) = ( 1 ... 𝐾 )
137 136 raleqi ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
138 ralunb ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
139 137 138 bitr3i ⊢ ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
140 eldifn ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) → ¬ 𝑝 ∈ ℙ )
141 iffalse ⊢ ( ¬ 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = 0 )
142 iffalse ⊢ ( ¬ 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) = 0 )
143 141 142 eqtr4d ⊢ ( ¬ 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
144 140 143 syl ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
145 144 rgen ⊢ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 )
146 145 biantru ⊢ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
147 elinel1 ⊢ ( 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℙ )
148 iftrue ⊢ ( 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = ( 𝑝 pCnt 𝑦 ) )
149 iftrue ⊢ ( 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) = ( 𝑝 pCnt 𝑧 ) )
150 148 149 eqeq12d ⊢ ( 𝑝 ∈ ℙ → ( if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
151 147 150 syl ⊢ ( 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) → ( if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
152 151 ralbiia ⊢ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
153 146 152 bitr3i ⊢ ( ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
154 139 153 bitri ⊢ ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
155 inundif ⊢ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) = ℙ
156 155 raleqi ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
157 ralunb ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
158 156 157 bitr3i ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
159 132 154 158 3bitr4g ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
160 120 nnnn0d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ ℕ0 )
161 123 nnnn0d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑧 ∈ ℕ0 )
162 pc11 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) → ( 𝑦 = 𝑧 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
163 160 161 162 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( 𝑦 = 𝑧 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
164 159 163 bitr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ 𝑦 = 𝑧 ) )
165 101 164 syl5bb ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ 𝑦 = 𝑧 ) )
166 165 ex ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ 𝑦 = 𝑧 ) ) )
167 77 166 syl5bi ⊢ ( 𝜑 → ( ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∧ 𝑧 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ 𝑦 = 𝑧 ) ) )
168 74 167 dom2d ⊢ ( 𝜑 → ( ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ∈ V → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
169 6 168 mpi ⊢ ( 𝜑 → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) )
170 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
171 ssrab2 ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 } ⊆ ( 1 ... 𝑁 )
172 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 } ⊆ ( 1 ... 𝑁 ) ) → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 } ∈ Fin )
173 170 171 172 mp2an ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 } ∈ Fin
174 4 173 eqeltri ⊢ 𝑀 ∈ Fin
175 ssrab2 ⊢ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ⊆ 𝑀
176 ssfi ⊢ ( ( 𝑀 ∈ Fin ∧ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ⊆ 𝑀 ) → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin )
177 174 175 176 mp2an ⊢ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin
178 prfi ⊢ { 0 , 1 } ∈ Fin
179 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐾 ) ∈ Fin )
180 mapfi ⊢ ( ( { 0 , 1 } ∈ Fin ∧ ( 1 ... 𝐾 ) ∈ Fin ) → ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ∈ Fin )
181 178 179 180 sylancr ⊢ ( 𝜑 → ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ∈ Fin )
182 hashdom ⊢ ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin ∧ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ∈ Fin ) → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) ↔ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
183 177 181 182 sylancr ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) ↔ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
184 169 183 mpbird ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
185 hashmap ⊢ ( ( { 0 , 1 } ∈ Fin ∧ ( 1 ... 𝐾 ) ∈ Fin ) → ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) = ( ( ♯ ‘ { 0 , 1 } ) ↑ ( ♯ ‘ ( 1 ... 𝐾 ) ) ) )
186 178 179 185 sylancr ⊢ ( 𝜑 → ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) = ( ( ♯ ‘ { 0 , 1 } ) ↑ ( ♯ ‘ ( 1 ... 𝐾 ) ) ) )
187 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
188 187 a1i ⊢ ( 𝜑 → ( ♯ ‘ { 0 , 1 } ) = 2 )
189 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
190 hashfz1 ⊢ ( 𝐾 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
191 189 190 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
192 188 191 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ { 0 , 1 } ) ↑ ( ♯ ‘ ( 1 ... 𝐾 ) ) ) = ( 2 ↑ 𝐾 ) )
193 186 192 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) = ( 2 ↑ 𝐾 ) )
194 184 193 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( 2 ↑ 𝐾 ) )