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 | |- I = ( Irred ` ZZring ) |
|
| Assertion | dfprm2 | |- Prime = ( NN i^i I ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prmirred.i | |- I = ( Irred ` ZZring ) |
|
| 2 | prmnn | |- ( x e. Prime -> x e. NN ) |
|
| 3 | 1 | prmirredlem | |- ( x e. NN -> ( x e. I <-> x e. Prime ) ) |
| 4 | 3 | bicomd | |- ( x e. NN -> ( x e. Prime <-> x e. I ) ) |
| 5 | 2 4 | biadanii | |- ( x e. Prime <-> ( x e. NN /\ x e. I ) ) |
| 6 | elin | |- ( x e. ( NN i^i I ) <-> ( x e. NN /\ x e. I ) ) |
|
| 7 | 5 6 | bitr4i | |- ( x e. Prime <-> x e. ( NN i^i I ) ) |
| 8 | 7 | eqriv | |- Prime = ( NN i^i I ) |