Theorem isnirred

Description: The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irred.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	irred.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	irred.3	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irred.4	⊢ 𝑁 = ( 𝐵 ∖ 𝑈 )
	irred.5	⊢ · = ( .r ‘ 𝑅 )
Assertion	isnirred	⊢ ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		irred.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		irred.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		irred.3	⊢ 𝐼 = ( Irred ‘ 𝑅 )
4		irred.4	⊢ 𝑁 = ( 𝐵 ∖ 𝑈 )
5		irred.5	⊢ · = ( .r ‘ 𝑅 )
6	4	eleq2i	⊢ ( 𝑋 ∈ 𝑁 ↔ 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) )
7		eldif	⊢ ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) )
8	6 7	bitri	⊢ ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) )
9	8	baibr	⊢ ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ 𝑁 ) )
10		df-ne	⊢ ( ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ¬ ( 𝑥 · 𝑦 ) = 𝑋 )
11	10	ralbii	⊢ ( ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ∀ 𝑦 ∈ 𝑁 ¬ ( 𝑥 · 𝑦 ) = 𝑋 )
12		ralnex	⊢ ( ∀ 𝑦 ∈ 𝑁 ¬ ( 𝑥 · 𝑦 ) = 𝑋 ↔ ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
13	11 12	bitri	⊢ ( ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
14	13	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ∀ 𝑥 ∈ 𝑁 ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
15		ralnex	⊢ ( ∀ 𝑥 ∈ 𝑁 ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ↔ ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
16	14 15	bitr2i	⊢ ( ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 )
17	16	a1i	⊢ ( 𝑋 ∈ 𝐵 → ( ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
18	9 17	anbi12d	⊢ ( 𝑋 ∈ 𝐵 → ( ( ¬ 𝑋 ∈ 𝑈 ∧ ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) )
19		ioran	⊢ ( ¬ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ↔ ( ¬ 𝑋 ∈ 𝑈 ∧ ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) )
20	1 2 3 4 5	isirred	⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
21	18 19 20	3bitr4g	⊢ ( 𝑋 ∈ 𝐵 → ( ¬ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ↔ 𝑋 ∈ 𝐼 ) )
22	21	con1bid	⊢ ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ) )