Metamath Proof Explorer

Theorem abssid

Description: The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion abssid 
|- ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` A ) = A )

Proof

Step Hyp Ref Expression
1 abssval 
 |-  ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )
2 iftrue 
 |-  ( 0s <_s A -> if ( 0s <_s A , A , ( -us ` A ) ) = A )
3 1 2 sylan9eq 
 |-  ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` A ) = A )