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 e. I -> -. X e. U ) |
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 ) = ( .r ` R ) |
|
5 | 3 2 1 4 | isirred2 | |- ( X e. I <-> ( X e. ( Base ` R ) /\ -. X e. U /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
6 | 5 | simp2bi | |- ( X e. I -> -. X e. U ) |