Theorem abssge0

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

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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( 0s <_s A -> 0s <_s A )
2		iftrue	|- ( 0s <_s A -> if ( 0s <_s A , A , ( -us ` A ) ) = A )
3	1 2	breqtrrd	|- ( 0s <_s A -> 0s <_s if ( 0s <_s A , A , ( -us ` A ) ) )
4	3	adantr	|- ( ( 0s <_s A /\ A e. No ) -> 0s <_s if ( 0s <_s A , A , ( -us ` A ) ) )
5		negs0s	|- ( -us ` 0s ) = 0s
6		0sno	|- 0s e. No
7		sletric	|- ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
8	6 7	mpan	|- ( A e. No -> ( 0s <_s A \/ A <_s 0s ) )
9	8	ord	|- ( A e. No -> ( -. 0s <_s A -> A <_s 0s ) )
10	9	impcom	|- ( ( -. 0s <_s A /\ A e. No ) -> A <_s 0s )
11		simpr	|- ( ( -. 0s <_s A /\ A e. No ) -> A e. No )
12	6	a1i	|- ( ( -. 0s <_s A /\ A e. No ) -> 0s e. No )
13	11 12	slenegd	|- ( ( -. 0s <_s A /\ A e. No ) -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
14	10 13	mpbid	|- ( ( -. 0s <_s A /\ A e. No ) -> ( -us ` 0s ) <_s ( -us ` A ) )
15	5 14	eqbrtrrid	|- ( ( -. 0s <_s A /\ A e. No ) -> 0s <_s ( -us ` A ) )
16		iffalse	|- ( -. 0s <_s A -> if ( 0s <_s A , A , ( -us ` A ) ) = ( -us ` A ) )
17	16	adantr	|- ( ( -. 0s <_s A /\ A e. No ) -> if ( 0s <_s A , A , ( -us ` A ) ) = ( -us ` A ) )
18	15 17	breqtrrd	|- ( ( -. 0s <_s A /\ A e. No ) -> 0s <_s if ( 0s <_s A , A , ( -us ` A ) ) )
19	4 18	pm2.61ian	|- ( A e. No -> 0s <_s if ( 0s <_s A , A , ( -us ` A ) ) )
20		abssval	|- ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )
21	19 20	breqtrrd	|- ( A e. No -> 0s <_s ( abs_s ` A ) )