Metamath Proof Explorer


Theorem dfprm2

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=Irredring
Assertion dfprm2 =I

Proof

Step Hyp Ref Expression
1 prmirred.i I=Irredring
2 prmnn xx
3 1 prmirredlem xxIx
4 3 bicomd xxxI
5 2 4 biadanii xxxI
6 elin xIxxI
7 5 6 bitr4i xxI
8 7 eqriv =I