Theorem irrednu

Description: An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	$$⊢I=\mathrm{Irred}\left(R\right)$$
	irrednu.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	irrednu	$$⊢X\in I\to \neg X\in U$$

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	$$⊢I=\mathrm{Irred}\left(R\right)$$
2		irrednu.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4		eqid	$$⊢{\cdot }_R={\cdot }_R$$
5	3 2 1 4	isirred2	$$⊢X\in I\leftrightarrow \left(X\in {\mathrm{Base}}_R\wedge \neg X\in U\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{R}y=X\to \left(x\in U\vee y\in U\right)\right)\right)$$
6	5	simp2bi	$$⊢X\in I\to \neg X\in U$$