Theorem abssid

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

	Ref	Expression
Assertion	abssid	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( abss ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		abssval	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
2		iftrue	⊢ ( 0s ≤s 𝐴 → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = 𝐴 )
3	1 2	sylan9eq	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( abss ‘ 𝐴 ) = 𝐴 )