Theorem negsval2

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

	Ref	Expression
Assertion	negsval2	|- ( A e. No -> ( -us ` A ) = ( 0s -s A ) )

Proof

Step	Hyp	Ref	Expression
1		0sno	|- 0s e. No
2		subsval	|- ( ( 0s e. No /\ A e. No ) -> ( 0s -s A ) = ( 0s +s ( -us ` A ) ) )
3	1 2	mpan	|- ( A e. No -> ( 0s -s A ) = ( 0s +s ( -us ` A ) ) )
4		negscl	|- ( A e. No -> ( -us ` A ) e. No )
5		addslid	|- ( ( -us ` A ) e. No -> ( 0s +s ( -us ` A ) ) = ( -us ` A ) )
6	4 5	syl	|- ( A e. No -> ( 0s +s ( -us ` A ) ) = ( -us ` A ) )
7	3 6	eqtr2d	|- ( A e. No -> ( -us ` A ) = ( 0s -s A ) )