Theorem abssnid

Description: For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		0no	⊢ 0s ∈ No
2		lesloe	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 ≤s 0s ↔ ( 𝐴 <s 0s ∨ 𝐴 = 0s ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s ↔ ( 𝐴 <s 0s ∨ 𝐴 = 0s ) ) )
4		ltnles	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 <s 0s ↔ ¬ 0s ≤s 𝐴 ) )
5	1 4	mpan2	⊢ ( 𝐴 ∈ No → ( 𝐴 <s 0s ↔ ¬ 0s ≤s 𝐴 ) )
6		abssval	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
7		iffalse	⊢ ( ¬ 0s ≤s 𝐴 → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) )
8	6 7	sylan9eq	⊢ ( ( 𝐴 ∈ No ∧ ¬ 0s ≤s 𝐴 ) → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) )
9	8	ex	⊢ ( 𝐴 ∈ No → ( ¬ 0s ≤s 𝐴 → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )
10	5 9	sylbid	⊢ ( 𝐴 ∈ No → ( 𝐴 <s 0s → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )
11		abs0s	⊢ ( abss ‘ 0s ) = 0s
12		neg0s	⊢ ( -us ‘ 0s ) = 0s
13	11 12	eqtr4i	⊢ ( abss ‘ 0s ) = ( -us ‘ 0s )
14		fveq2	⊢ ( 𝐴 = 0s → ( abss ‘ 𝐴 ) = ( abss ‘ 0s ) )
15		fveq2	⊢ ( 𝐴 = 0s → ( -us ‘ 𝐴 ) = ( -us ‘ 0s ) )
16	13 14 15	3eqtr4a	⊢ ( 𝐴 = 0s → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) )
17	16	a1i	⊢ ( 𝐴 ∈ No → ( 𝐴 = 0s → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )
18	10 17	jaod	⊢ ( 𝐴 ∈ No → ( ( 𝐴 <s 0s ∨ 𝐴 = 0s ) → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )
19	3 18	sylbid	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )
20	19	imp	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) )