Description: An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | irredn0.i | ||
irrednu.u | |||
Assertion | irrednu |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | irredn0.i | ||
2 | irrednu.u | ||
3 | eqid | ||
4 | eqid | ||
5 | 3 2 1 4 | isirred2 | |
6 | 5 | simp2bi |