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
|
sseldi |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 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
|
sseldi |
⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) → 𝑦 ∈ ℕ ) |
121 |
|
pceq0 |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑦 ) = 0 ↔ ¬ 𝑝 ∥ 𝑦 ) ) |
122 |
117 120 121
|
syl2anr |
⊢ ( ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 1 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑧 ) = 1 ) ) ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 pCnt 𝑦 ) = 0 ↔ ¬ 𝑝 ∥ 𝑦 ) ) |
123 |
119 109
|
sseldi |
⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝑀 ∧ ( 𝑄 ‘ 𝑦 ) = 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 ↑ 𝐾 ) ) |