Theorem renegclALT

Description: Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl . (Contributed by NM, 15-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	renegclALT	|- ( A e. RR -> -u A e. RR )

Proof

Step	Hyp	Ref	Expression
1		negeq	|- ( x = A -> -u x = -u A )
2	1	eleq1d	|- ( x = A -> ( -u x e. RR <-> -u A e. RR ) )
3		vex	|- x e. _V
4		c0ex	|- 0 e. _V
5	3 4	ifex	|- if ( x e. RR , x , 0 ) e. _V
6		csbnegg	|- ( if ( x e. RR , x , 0 ) e. _V -> [_ if ( x e. RR , x , 0 ) / x ]_ -u x = -u [_ if ( x e. RR , x , 0 ) / x ]_ x )
7	5 6	ax-mp	|- [_ if ( x e. RR , x , 0 ) / x ]_ -u x = -u [_ if ( x e. RR , x , 0 ) / x ]_ x
8		csbvarg	|- ( 0 e. _V -> [_ 0 / x ]_ x = 0 )
9	4 8	ax-mp	|- [_ 0 / x ]_ x = 0
10		0re	|- 0 e. RR
11	9 10	eqeltri	|- [_ 0 / x ]_ x e. RR
12		sbcel1g	|- ( 0 e. _V -> ( [. 0 / x ]. x e. RR <-> [_ 0 / x ]_ x e. RR ) )
13	4 12	ax-mp	|- ( [. 0 / x ]. x e. RR <-> [_ 0 / x ]_ x e. RR )
14	11 13	mpbir	|- [. 0 / x ]. x e. RR
15	14	elimhyps	|- [. if ( x e. RR , x , 0 ) / x ]. x e. RR
16		sbcel1g	|- ( if ( x e. RR , x , 0 ) e. _V -> ( [. if ( x e. RR , x , 0 ) / x ]. x e. RR <-> [_ if ( x e. RR , x , 0 ) / x ]_ x e. RR ) )
17	5 16	ax-mp	|- ( [. if ( x e. RR , x , 0 ) / x ]. x e. RR <-> [_ if ( x e. RR , x , 0 ) / x ]_ x e. RR )
18	15 17	mpbi	|- [_ if ( x e. RR , x , 0 ) / x ]_ x e. RR
19	18	renegcli	|- -u [_ if ( x e. RR , x , 0 ) / x ]_ x e. RR
20	7 19	eqeltri	|- [_ if ( x e. RR , x , 0 ) / x ]_ -u x e. RR
21		sbcel1g	|- ( if ( x e. RR , x , 0 ) e. _V -> ( [. if ( x e. RR , x , 0 ) / x ]. -u x e. RR <-> [_ if ( x e. RR , x , 0 ) / x ]_ -u x e. RR ) )
22	5 21	ax-mp	|- ( [. if ( x e. RR , x , 0 ) / x ]. -u x e. RR <-> [_ if ( x e. RR , x , 0 ) / x ]_ -u x e. RR )
23	20 22	mpbir	|- [. if ( x e. RR , x , 0 ) / x ]. -u x e. RR
24	23	dedths	|- ( x e. RR -> -u x e. RR )
25	2 24	vtoclga	|- ( A e. RR -> -u A e. RR )