Theorem irredn1

Description: The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	|- I = ( Irred ` R )
	irredn1.o	|- .1. = ( 1r ` R )
Assertion	irredn1	|- ( ( R e. Ring /\ X e. I ) -> X =/= .1. )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	|- I = ( Irred ` R )
2		irredn1.o	|- .1. = ( 1r ` R )
3		eqid	|- ( Unit ` R ) = ( Unit ` R )
4	3 2	1unit	|- ( R e. Ring -> .1. e. ( Unit ` R ) )
5		eleq1	|- ( X = .1. -> ( X e. ( Unit ` R ) <-> .1. e. ( Unit ` R ) ) )
6	4 5	syl5ibrcom	|- ( R e. Ring -> ( X = .1. -> X e. ( Unit ` R ) ) )
7	6	necon3bd	|- ( R e. Ring -> ( -. X e. ( Unit ` R ) -> X =/= .1. ) )
8	1 3	irrednu	|- ( X e. I -> -. X e. ( Unit ` R ) )
9	7 8	impel	|- ( ( R e. Ring /\ X e. I ) -> X =/= .1. )