Theorem rernegcl

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

	Ref	Expression
Assertion	rernegcl	|- ( A e. RR -> ( 0 -R A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		elre0re	|- ( A e. RR -> 0 e. RR )
2		resubval	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 -R A ) = ( iota_ x e. RR ( A + x ) = 0 ) )
3	1 2	mpancom	|- ( A e. RR -> ( 0 -R A ) = ( iota_ x e. RR ( A + x ) = 0 ) )
4		renegeu	|- ( A e. RR -> E! x e. RR ( A + x ) = 0 )
5		riotacl	|- ( E! x e. RR ( A + x ) = 0 -> ( iota_ x e. RR ( A + x ) = 0 ) e. RR )
6	4 5	syl	|- ( A e. RR -> ( iota_ x e. RR ( A + x ) = 0 ) e. RR )
7	3 6	eqeltrd	|- ( A e. RR -> ( 0 -R A ) e. RR )