Metamath Proof Explorer
Description: Define the set of square positive integers. (Contributed by Stefan
O'Rear, 18-Sep-2014)
|
|
Ref |
Expression |
|
Assertion |
df-squarenn |
⊢ ◻NN = { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ } |
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
csquarenn |
⊢ ◻NN |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
cn |
⊢ ℕ |
3 |
|
csqrt |
⊢ √ |
4 |
1
|
cv |
⊢ 𝑥 |
5 |
4 3
|
cfv |
⊢ ( √ ‘ 𝑥 ) |
6 |
|
cq |
⊢ ℚ |
7 |
5 6
|
wcel |
⊢ ( √ ‘ 𝑥 ) ∈ ℚ |
8 |
7 1 2
|
crab |
⊢ { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ } |
9 |
0 8
|
wceq |
⊢ ◻NN = { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ } |