Metamath Proof Explorer


Theorem irrednu

Description: An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i I = Irred R
irrednu.u U = Unit R
Assertion irrednu X I ¬ X U

Proof

Step Hyp Ref Expression
1 irredn0.i I = Irred R
2 irrednu.u U = Unit R
3 eqid Base R = Base R
4 eqid R = R
5 3 2 1 4 isirred2 X I X Base R ¬ X U x Base R y Base R x R y = X x U y U
6 5 simp2bi X I ¬ X U