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	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	irredn1	$⊢ (R \in Ring \land X \in I) \to X \neq \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		irredn0.i	$⊢ I = Irred (R)$
2		irredn1.o	$⊢ \underset{˙}{1} = 1_{R}$
3		eqid	$⊢ Unit (R) = Unit (R)$
4	3 2	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in Unit (R)$
5		eleq1	$⊢ X = \underset{˙}{1} \to (X \in Unit (R) \leftrightarrow \underset{˙}{1} \in Unit (R))$
6	4 5	syl5ibrcom	$⊢ R \in Ring \to (X = \underset{˙}{1} \to X \in Unit (R))$
7	6	necon3bd	$⊢ R \in Ring \to (\neg X \in Unit (R) \to X \neq \underset{˙}{1})$
8	1 3	irrednu	$⊢ X \in I \to \neg X \in Unit (R)$
9	7 8	impel	$⊢ (R \in Ring \land X \in I) \to X \neq \underset{˙}{1}$

Metamath Proof Explorer