Theorem irredn1

Description: The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irredn1.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	irredn1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ≠ 1 )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
2		irredn1.o	⊢ 1 = ( 1r ‘ 𝑅 )
3		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
4	3 2	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
5		eleq1	⊢ ( 𝑋 = 1 → ( 𝑋 ∈ ( Unit ‘ 𝑅 ) ↔ 1 ∈ ( Unit ‘ 𝑅 ) ) )
6	4 5	syl5ibrcom	⊢ ( 𝑅 ∈ Ring → ( 𝑋 = 1 → 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
7	6	necon3bd	⊢ ( 𝑅 ∈ Ring → ( ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) → 𝑋 ≠ 1 ) )
8	1 3	irrednu	⊢ ( 𝑋 ∈ 𝐼 → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
9	7 8	impel	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ≠ 1 )