Step |
Hyp |
Ref |
Expression |
0 |
|
crqp |
⊢ /Qp |
1 |
|
vp |
⊢ 𝑝 |
2 |
|
cprime |
⊢ ℙ |
3 |
|
ceqp |
⊢ ~Qp |
4 |
|
vf |
⊢ 𝑓 |
5 |
|
cz |
⊢ ℤ |
6 |
|
cmap |
⊢ ↑m |
7 |
5 5 6
|
co |
⊢ ( ℤ ↑m ℤ ) |
8 |
|
vx |
⊢ 𝑥 |
9 |
|
cuz |
⊢ ℤ≥ |
10 |
9
|
crn |
⊢ ran ℤ≥ |
11 |
4
|
cv |
⊢ 𝑓 |
12 |
11
|
ccnv |
⊢ ◡ 𝑓 |
13 |
|
cc0 |
⊢ 0 |
14 |
13
|
csn |
⊢ { 0 } |
15 |
5 14
|
cdif |
⊢ ( ℤ ∖ { 0 } ) |
16 |
12 15
|
cima |
⊢ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) |
17 |
8
|
cv |
⊢ 𝑥 |
18 |
16 17
|
wss |
⊢ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 |
19 |
18 8 10
|
wrex |
⊢ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 |
20 |
19 4 7
|
crab |
⊢ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } |
21 |
|
vy |
⊢ 𝑦 |
22 |
21
|
cv |
⊢ 𝑦 |
23 |
|
cfz |
⊢ ... |
24 |
1
|
cv |
⊢ 𝑝 |
25 |
|
cmin |
⊢ − |
26 |
|
c1 |
⊢ 1 |
27 |
24 26 25
|
co |
⊢ ( 𝑝 − 1 ) |
28 |
13 27 23
|
co |
⊢ ( 0 ... ( 𝑝 − 1 ) ) |
29 |
5 28 6
|
co |
⊢ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) |
30 |
22 29
|
cin |
⊢ ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) |
31 |
22 30
|
cxp |
⊢ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) |
32 |
21 20 31
|
csb |
⊢ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) |
33 |
3 32
|
cin |
⊢ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) ) |
34 |
1 2 33
|
cmpt |
⊢ ( 𝑝 ∈ ℙ ↦ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) ) ) |
35 |
0 34
|
wceq |
⊢ /Qp = ( 𝑝 ∈ ℙ ↦ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) ) ) |