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) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

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 fz01pr ⊢ ( 0 ... 1 ) = { 0 , 1 }
57 55 56 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt 𝑦 ) ∈ { 0 , 1 } )
58 0elpr01 ⊢ 0 ∈ { 0 , 1 }
59 58 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑛 ∈ ℙ ) → 0 ∈ { 0 , 1 } )
60 57 59 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) ∧ 𝑛 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ∈ { 0 , 1 } )
61 60 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) : ( 1 ... 𝐾 ) ⟶ { 0 , 1 } )
62 prex ⊢ { 0 , 1 } ∈ V
63 ovex ⊢ ( 1 ... 𝐾 ) ∈ V
64 62 63 elmap ⊢ ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) : ( 1 ... 𝐾 ) ⟶ { 0 , 1 } )
65 61 64 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) )
66 65 ex ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
67 8 66 biimtrid ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ∈ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
68 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑄 ‘ 𝑥 ) = 1 ↔ ( 𝑄 ‘ 𝑧 ) = 1 ) )
69 68 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) )
70 8 69 anbi12i ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∧ 𝑧 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ↔ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) )
71 ovex ⊢ ( 𝑛 pCnt 𝑦 ) ∈ V
72 c0ex ⊢ 0 ∈ V
73 71 72 ifex ⊢ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ∈ V
74 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) )
75 73 74 fnmpti ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) Fn ( 1 ... 𝐾 )
76 ovex ⊢ ( 𝑛 pCnt 𝑧 ) ∈ V
77 76 72 ifex ⊢ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ∈ V
78 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) )
79 77 78 fnmpti ⊢ ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) Fn ( 1 ... 𝐾 )
80 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 ) ) ‘ 𝑝 ) ) )
81 75 79 80 mp2an ⊢ ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) )
82 eleq1w ⊢ ( 𝑛 = 𝑝 → ( 𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ ) )
83 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑦 ) )
84 82 83 ifbieq1d ⊢ ( 𝑛 = 𝑝 → if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) )
85 ovex ⊢ ( 𝑝 pCnt 𝑦 ) ∈ V
86 85 72 ifex ⊢ if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) ∈ V
87 84 74 86 fvmpt ⊢ ( 𝑝 ∈ ( 1 ... 𝐾 ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) )
88 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 pCnt 𝑧 ) = ( 𝑝 pCnt 𝑧 ) )
89 82 88 ifbieq1d ⊢ ( 𝑛 = 𝑝 → if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
90 ovex ⊢ ( 𝑝 pCnt 𝑧 ) ∈ V
91 90 72 ifex ⊢ if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∈ V
92 89 78 91 fvmpt ⊢ ( 𝑝 ∈ ( 1 ... 𝐾 ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
93 87 92 eqeq12d ⊢ ( 𝑝 ∈ ( 1 ... 𝐾 ) → ( ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) ↔ if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
94 93 ralbiia ⊢ ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
95 81 94 bitri ⊢ ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
96 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ 𝑀 )
97 breq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦 ) )
98 97 notbid ⊢ ( 𝑛 = 𝑦 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦 ) )
99 98 ralbidv ⊢ ( 𝑛 = 𝑦 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
100 99 4 elrab2 ⊢ ( 𝑦 ∈ 𝑀 ↔ ( 𝑦 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
101 100 simprbi ⊢ ( 𝑦 ∈ 𝑀 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 )
102 96 101 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 )
103 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑧 ∈ 𝑀 )
104 breq2 ⊢ ( 𝑛 = 𝑧 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧 ) )
105 104 notbid ⊢ ( 𝑛 = 𝑧 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧 ) )
106 105 ralbidv ⊢ ( 𝑛 = 𝑧 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) )
107 106 4 elrab2 ⊢ ( 𝑧 ∈ 𝑀 ↔ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) )
108 107 simprbi ⊢ ( 𝑧 ∈ 𝑀 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 )
109 103 108 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 )
110 r19.26 ⊢ ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) )
111 eldifi ⊢ ( 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℙ )
112 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
113 9 112 sstri ⊢ 𝑀 ⊆ ℕ
114 113 96 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ ℕ )
115 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑦 ) = 0 ↔ ¬ 𝑝 ∥ 𝑦 ) )
116 111 114 115 syl2anr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 pCnt 𝑦 ) = 0 ↔ ¬ 𝑝 ∥ 𝑦 ) )
117 113 103 sselid ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑧 ∈ ℕ )
118 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑧 ) = 0 ↔ ¬ 𝑝 ∥ 𝑧 ) )
119 111 117 118 syl2anr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 pCnt 𝑧 ) = 0 ↔ ¬ 𝑝 ∥ 𝑧 ) )
120 116 119 anbi12d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( ( 𝑝 pCnt 𝑦 ) = 0 ∧ ( 𝑝 pCnt 𝑧 ) = 0 ) ↔ ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) ) )
121 eqtr3 ⊢ ( ( ( 𝑝 pCnt 𝑦 ) = 0 ∧ ( 𝑝 pCnt 𝑧 ) = 0 ) → ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
122 120 121 biimtrrdi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) → ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
123 122 ralimdva ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( ¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
124 110 123 biimtrrid ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑧 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
125 102 109 124 mp2and ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
126 125 biantrud ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) ) )
127 incom ⊢ ( ℙ ∩ ( 1 ... 𝐾 ) ) = ( ( 1 ... 𝐾 ) ∩ ℙ )
128 127 uneq1i ⊢ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) = ( ( ( 1 ... 𝐾 ) ∩ ℙ ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) )
129 inundif ⊢ ( ( ( 1 ... 𝐾 ) ∩ ℙ ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) = ( 1 ... 𝐾 )
130 128 129 eqtri ⊢ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) = ( 1 ... 𝐾 )
131 130 raleqi ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
132 ralunb ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ( 1 ... 𝐾 ) ∖ ℙ ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
133 131 132 bitr3i ⊢ ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
134 eldifn ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) → ¬ 𝑝 ∈ ℙ )
135 iffalse ⊢ ( ¬ 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = 0 )
136 iffalse ⊢ ( ¬ 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) = 0 )
137 135 136 eqtr4d ⊢ ( ¬ 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
138 134 137 syl ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) )
139 138 rgen ⊢ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 )
140 139 biantru ⊢ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) )
141 elinel1 ⊢ ( 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℙ )
142 iftrue ⊢ ( 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = ( 𝑝 pCnt 𝑦 ) )
143 iftrue ⊢ ( 𝑝 ∈ ℙ → if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) = ( 𝑝 pCnt 𝑧 ) )
144 142 143 eqeq12d ⊢ ( 𝑝 ∈ ℙ → ( if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
145 141 144 syl ⊢ ( 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) → ( if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
146 145 ralbiia ⊢ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
147 140 146 bitr3i ⊢ ( ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐾 ) ∖ ℙ ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ) ↔ ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
148 133 147 bitri ⊢ ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
149 inundif ⊢ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) = ℙ
150 149 raleqi ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) )
151 ralunb ⊢ ( ∀ 𝑝 ∈ ( ( ℙ ∩ ( 1 ... 𝐾 ) ) ∪ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
152 150 151 bitr3i ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ↔ ( ∀ 𝑝 ∈ ( ℙ ∩ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
153 126 148 152 3bitr4g ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
154 114 nnnn0d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ ℕ0 )
155 117 nnnn0d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑧 ∈ ℕ0 )
156 pc11 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) → ( 𝑦 = 𝑧 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
157 154 155 156 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( 𝑦 = 𝑧 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑦 ) = ( 𝑝 pCnt 𝑧 ) ) )
158 153 157 bitr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ∀ 𝑝 ∈ ( 1 ... 𝐾 ) if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑦 ) , 0 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 pCnt 𝑧 ) , 0 ) ↔ 𝑦 = 𝑧 ) )
159 95 158 bitrid ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ 𝑦 = 𝑧 ) )
160 159 ex ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ 𝑦 = 𝑧 ) ) )
161 70 160 biimtrid ⊢ ( 𝜑 → ( ( 𝑦 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∧ 𝑧 ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) → ( ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑦 ) , 0 ) ) = ( 𝑛 ∈ ( 1 ... 𝐾 ) ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 pCnt 𝑧 ) , 0 ) ) ↔ 𝑦 = 𝑧 ) ) )
162 67 161 dom2d ⊢ ( 𝜑 → ( ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ∈ V → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
163 6 162 mpi ⊢ ( 𝜑 → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) )
164 hashdomi ⊢ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ≼ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
165 163 164 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) )
166 prfi ⊢ { 0 , 1 } ∈ Fin
167 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐾 ) ∈ Fin )
168 hashmap ⊢ ( ( { 0 , 1 } ∈ Fin ∧ ( 1 ... 𝐾 ) ∈ Fin ) → ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) = ( ( ♯ ‘ { 0 , 1 } ) ↑ ( ♯ ‘ ( 1 ... 𝐾 ) ) ) )
169 166 167 168 sylancr ⊢ ( 𝜑 → ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) = ( ( ♯ ‘ { 0 , 1 } ) ↑ ( ♯ ‘ ( 1 ... 𝐾 ) ) ) )
170 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
171 170 a1i ⊢ ( 𝜑 → ( ♯ ‘ { 0 , 1 } ) = 2 )
172 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
173 hashfz1 ⊢ ( 𝐾 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
174 172 173 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
175 171 174 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ { 0 , 1 } ) ↑ ( ♯ ‘ ( 1 ... 𝐾 ) ) ) = ( 2 ↑ 𝐾 ) )
176 169 175 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( { 0 , 1 } ↑m ( 1 ... 𝐾 ) ) ) = ( 2 ↑ 𝐾 ) )
177 165 176 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( 2 ↑ 𝐾 ) )