Theorem sleabs

Description: A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	sleabs	|- ( A e. No -> A <_s ( abs_s ` A ) )

Proof

Step	Hyp	Ref	Expression
1		slerflex	|- ( A e. No -> A <_s A )
2	1	adantr	|- ( ( A e. No /\ 0s <_s A ) -> A <_s A )
3		abssid	|- ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` A ) = A )
4	2 3	breqtrrd	|- ( ( A e. No /\ 0s <_s A ) -> A <_s ( abs_s ` A ) )
5		simpl	|- ( ( A e. No /\ A <_s 0s ) -> A e. No )
6		0sno	|- 0s e. No
7	6	a1i	|- ( ( A e. No /\ A <_s 0s ) -> 0s e. No )
8		negscl	|- ( A e. No -> ( -us ` A ) e. No )
9	8	adantr	|- ( ( A e. No /\ A <_s 0s ) -> ( -us ` A ) e. No )
10		simpr	|- ( ( A e. No /\ A <_s 0s ) -> A <_s 0s )
11		negs0s	|- ( -us ` 0s ) = 0s
12	5 7	slenegd	|- ( ( A e. No /\ A <_s 0s ) -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
13	10 12	mpbid	|- ( ( A e. No /\ A <_s 0s ) -> ( -us ` 0s ) <_s ( -us ` A ) )
14	11 13	eqbrtrrid	|- ( ( A e. No /\ A <_s 0s ) -> 0s <_s ( -us ` A ) )
15	5 7 9 10 14	sletrd	|- ( ( A e. No /\ A <_s 0s ) -> A <_s ( -us ` A ) )
16		abssnid	|- ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` A ) = ( -us ` A ) )
17	15 16	breqtrrd	|- ( ( A e. No /\ A <_s 0s ) -> A <_s ( abs_s ` A ) )
18		sletric	|- ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
19	6 18	mpan	|- ( A e. No -> ( 0s <_s A \/ A <_s 0s ) )
20	4 17 19	mpjaodan	|- ( A e. No -> A <_s ( abs_s ` A ) )