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\in ℝ\to -A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		negeq	$$⊢x=A\to -x=-A$$
2	1	eleq1d	$$⊢x=A\to \left(-x\in ℝ\leftrightarrow -A\in ℝ\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	3 4	ifex	$$⊢if\left(x\in ℝ,x,0\right)\in \mathrm{V}$$
6		csbnegg	$$⊢if\left(x\in ℝ,x,0\right)\in \mathrm{V}\to ⦋if\left(x\in ℝ,x,0\right)/x⦌\left(-x\right)=-⦋if\left(x\in ℝ,x,0\right)/x⦌x$$
7	5 6	ax-mp	$$⊢⦋if\left(x\in ℝ,x,0\right)/x⦌\left(-x\right)=-⦋if\left(x\in ℝ,x,0\right)/x⦌x$$
8		csbvarg	$$⊢0\in \mathrm{V}\to ⦋0/x⦌x=0$$
9	4 8	ax-mp	$$⊢⦋0/x⦌x=0$$
10		0re	$$⊢0\in ℝ$$
11	9 10	eqeltri	$$⊢⦋0/x⦌x\in ℝ$$
12		sbcel1g	$$⊢0\in \mathrm{V}\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}x\in ℝ\leftrightarrow ⦋0/x⦌x\in ℝ\right)$$
13	4 12	ax-mp	$$⊢\underset{\dot{}}{[}0/x\underset{\dot{}}{]}x\in ℝ\leftrightarrow ⦋0/x⦌x\in ℝ$$
14	11 13	mpbir	$$⊢\underset{\dot{}}{[}0/x\underset{\dot{}}{]}x\in ℝ$$
15	14	elimhyps	$$⊢\underset{\dot{}}{[}if\left(x\in ℝ,x,0\right)/x\underset{\dot{}}{]}x\in ℝ$$
16		sbcel1g	$$⊢if\left(x\in ℝ,x,0\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}if\left(x\in ℝ,x,0\right)/x\underset{\dot{}}{]}x\in ℝ\leftrightarrow ⦋if\left(x\in ℝ,x,0\right)/x⦌x\in ℝ\right)$$
17	5 16	ax-mp	$$⊢\underset{\dot{}}{[}if\left(x\in ℝ,x,0\right)/x\underset{\dot{}}{]}x\in ℝ\leftrightarrow ⦋if\left(x\in ℝ,x,0\right)/x⦌x\in ℝ$$
18	15 17	mpbi	$$⊢⦋if\left(x\in ℝ,x,0\right)/x⦌x\in ℝ$$
19	18	renegcli	$$⊢-⦋if\left(x\in ℝ,x,0\right)/x⦌x\in ℝ$$
20	7 19	eqeltri	$$⊢⦋if\left(x\in ℝ,x,0\right)/x⦌\left(-x\right)\in ℝ$$
21		sbcel1g	$$⊢if\left(x\in ℝ,x,0\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}if\left(x\in ℝ,x,0\right)/x\underset{\dot{}}{]}-x\in ℝ\leftrightarrow ⦋if\left(x\in ℝ,x,0\right)/x⦌\left(-x\right)\in ℝ\right)$$
22	5 21	ax-mp	$$⊢\underset{\dot{}}{[}if\left(x\in ℝ,x,0\right)/x\underset{\dot{}}{]}-x\in ℝ\leftrightarrow ⦋if\left(x\in ℝ,x,0\right)/x⦌\left(-x\right)\in ℝ$$
23	20 22	mpbir	$$⊢\underset{\dot{}}{[}if\left(x\in ℝ,x,0\right)/x\underset{\dot{}}{]}-x\in ℝ$$
24	23	dedths	$$⊢x\in ℝ\to -x\in ℝ$$
25	2 24	vtoclga	$$⊢A\in ℝ\to -A\in ℝ$$