Description: The positive irreducible elements of ZZ are the prime numbers. This is an alternative way to define Prime . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | prmirred.i | ⊢ 𝐼 = ( Irred ‘ ℤring ) | |
| Assertion | dfprm2 | ⊢ ℙ = ( ℕ ∩ 𝐼 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prmirred.i | ⊢ 𝐼 = ( Irred ‘ ℤring ) | |
| 2 | prmnn | ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℕ ) | |
| 3 | 1 | prmirredlem | ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 ∈ 𝐼 ↔ 𝑥 ∈ ℙ ) ) |
| 4 | 3 | bicomd | ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 ∈ ℙ ↔ 𝑥 ∈ 𝐼 ) ) |
| 5 | 2 4 | biadanii | ⊢ ( 𝑥 ∈ ℙ ↔ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ 𝐼 ) ) |
| 6 | elin | ⊢ ( 𝑥 ∈ ( ℕ ∩ 𝐼 ) ↔ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ 𝐼 ) ) | |
| 7 | 5 6 | bitr4i | ⊢ ( 𝑥 ∈ ℙ ↔ 𝑥 ∈ ( ℕ ∩ 𝐼 ) ) |
| 8 | 7 | eqriv | ⊢ ℙ = ( ℕ ∩ 𝐼 ) |