Metamath Proof Explorer


Theorem irredneg

Description: The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i I=IrredR
irredneg.n N=invgR
Assertion irredneg RRingXINXI

Proof

Step Hyp Ref Expression
1 irredn0.i I=IrredR
2 irredneg.n N=invgR
3 eqid BaseR=BaseR
4 eqid R=R
5 eqid 1R=1R
6 simpl RRingXIRRing
7 1 3 irredcl XIXBaseR
8 7 adantl RRingXIXBaseR
9 3 4 5 2 6 8 rngnegr RRingXIXRN1R=NX
10 eqid UnitR=UnitR
11 10 5 1unit RRing1RUnitR
12 10 2 unitnegcl RRing1RUnitRN1RUnitR
13 11 12 mpdan RRingN1RUnitR
14 13 adantr RRingXIN1RUnitR
15 1 10 4 irredrmul RRingXIN1RUnitRXRN1RI
16 14 15 mpd3an3 RRingXIXRN1RI
17 9 16 eqeltrrd RRingXINXI