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 )