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 e. I -> -. X e. 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 ) = ( .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 )