This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-prm

Description: Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion df-prm ℙ = { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprime ⊢ ℙ
1 vp ⊢ 𝑝
2 cn ⊢ ℕ
3 vn ⊢ 𝑛
4 3 cv ⊢ 𝑛
5 cdvds ⊢ ∥
6 1 cv ⊢ 𝑝
7 4 6 5 wbr ⊢ 𝑛 ∥ 𝑝
8 7 3 2 crab ⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 }
9 cen ⊢ ≈
10 c2o ⊢ 2o
11 8 10 9 wbr ⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o
12 11 1 2 crab ⊢ { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }
13 0 12 wceq ⊢ ℙ = { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }