This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ I → ¬ X ∈ 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
5 3 2 1 4 isirred2 ⊢ X ∈ I ↔ X ∈ Base R ∧ ¬ X ∈ U ∧ ∀ x ∈ Base R ∀ y ∈ Base R x ⋅ R y = X → x ∈ U ∨ y ∈ U
6 5 simp2bi ⊢ X ∈ I → ¬ X ∈ U