Metamath Proof Explorer


Theorem rernegcl

Description: Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion rernegcl A0-A

Proof

Step Hyp Ref Expression
1 elre0re A0
2 resubval 0A0-A=ιx|A+x=0
3 1 2 mpancom A0-A=ιx|A+x=0
4 renegeu A∃!xA+x=0
5 riotacl ∃!xA+x=0ιx|A+x=0
6 4 5 syl Aιx|A+x=0
7 3 6 eqeltrd A0-A