Theorem negsval2d

Description: Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Hypothesis	negsval2d.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	negsval2d	$$⊢\phi \to {+}_s\left(A\right)=0_s{-}_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		negsval2d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		negsval2	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)=0_s{-}_{s}A$$
3	1 2	syl	$$⊢\phi \to {+}_s\left(A\right)=0_s{-}_{s}A$$