Description: The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | irredn0.i | |
|
irredneg.n | |
||
Assertion | irredneg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | irredn0.i | |
|
2 | irredneg.n | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | simpl | |
|
7 | 1 3 | irredcl | |
8 | 7 | adantl | |
9 | 3 4 5 2 6 8 | rngnegr | |
10 | eqid | |
|
11 | 10 5 | 1unit | |
12 | 10 2 | unitnegcl | |
13 | 11 12 | mpdan | |
14 | 13 | adantr | |
15 | 1 10 4 | irredrmul | |
16 | 14 15 | mpd3an3 | |
17 | 9 16 | eqeltrrd | |