Theorem absnegs

Description: Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	absnegs	⊢ ( 𝐴 ∈ No → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( abss ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negnegs	⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
3		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
4		0no	⊢ 0s ∈ No
5	4	a1i	⊢ ( 𝐴 ∈ No → 0s ∈ No )
6		id	⊢ ( 𝐴 ∈ No → 𝐴 ∈ No )
7	5 6	lenegsd	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 ↔ ( -us ‘ 𝐴 ) ≤s ( -us ‘ 0s ) ) )
8		neg0s	⊢ ( -us ‘ 0s ) = 0s
9	8	breq2i	⊢ ( ( -us ‘ 𝐴 ) ≤s ( -us ‘ 0s ) ↔ ( -us ‘ 𝐴 ) ≤s 0s )
10	7 9	bitrdi	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 ↔ ( -us ‘ 𝐴 ) ≤s 0s ) )
11	10	biimpa	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( -us ‘ 𝐴 ) ≤s 0s )
12		abssnid	⊢ ( ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us ‘ 𝐴 ) ≤s 0s ) → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( -us ‘ ( -us ‘ 𝐴 ) ) )
13	3 11 12	syl2an2r	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( -us ‘ ( -us ‘ 𝐴 ) ) )
14		abssid	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( abss ‘ 𝐴 ) = 𝐴 )
15	2 13 14	3eqtr4d	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( abss ‘ 𝐴 ) )
16	6 5	lenegsd	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
17	8	breq1i	⊢ ( ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ↔ 0s ≤s ( -us ‘ 𝐴 ) )
18	16 17	bitrdi	⊢ ( 𝐴 ∈ No → ( 𝐴 ≤s 0s ↔ 0s ≤s ( -us ‘ 𝐴 ) ) )
19	18	biimpa	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 0s ≤s ( -us ‘ 𝐴 ) )
20		abssid	⊢ ( ( ( -us ‘ 𝐴 ) ∈ No ∧ 0s ≤s ( -us ‘ 𝐴 ) ) → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) )
21	3 19 20	syl2an2r	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) )
22		abssnid	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) )
23	21 22	eqtr4d	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( abss ‘ 𝐴 ) )
24		lestric	⊢ ( ( 0s ∈ No ∧ 𝐴 ∈ No ) → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
25	4 24	mpan	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
26	15 23 25	mpjaodan	⊢ ( 𝐴 ∈ No → ( abss ‘ ( -us ‘ 𝐴 ) ) = ( abss ‘ 𝐴 ) )