Theorem irrednu

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

	Ref	Expression
Hypotheses	irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irrednu.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	irrednu	⊢ ( 𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
2		irrednu.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5	3 2 1 4	isirred2	⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
6	5	simp2bi	⊢ ( 𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ 𝑈 )