Metamath Proof Explorer


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. )