Metamath Proof Explorer

Theorem absslt

Description: Surreal absolute value and less-than relation. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion absslt 
|- ( ( A e. No /\ B e. No ) -> ( ( abs_s ` A )  ( ( -us ` B )

Proof

Step Hyp Ref Expression
1 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
2 1 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( -us ` A ) e. No )
3 absscl 
 |-  ( ( -us ` A ) e. No -> ( abs_s ` ( -us ` A ) ) e. No )
4 1 3 syl 
 |-  ( A e. No -> ( abs_s ` ( -us ` A ) ) e. No )
5 4 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( abs_s ` ( -us ` A ) ) e. No )
6 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  B e. No )
7 sleabs 
 |-  ( ( -us ` A ) e. No -> ( -us ` A ) <_s ( abs_s ` ( -us ` A ) ) )
8 1 7 syl 
 |-  ( A e. No -> ( -us ` A ) <_s ( abs_s ` ( -us ` A ) ) )
9 8 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( -us ` A ) <_s ( abs_s ` ( -us ` A ) ) )
10 abssneg 
 |-  ( A e. No -> ( abs_s ` ( -us ` A ) ) = ( abs_s ` A ) )
11 10 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( abs_s ` ( -us ` A ) ) = ( abs_s ` A ) )
12 11 breq1d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( abs_s ` ( -us ` A ) )  ( abs_s ` A )
13 12 biimpar 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( abs_s ` ( -us ` A ) )
14 2 5 6 9 13 slelttrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( -us ` A )
15 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  A e. No )
16 absscl 
 |-  ( A e. No -> ( abs_s ` A ) e. No )
17 16 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( abs_s ` A ) e. No )
18 sleabs 
 |-  ( A e. No -> A <_s ( abs_s ` A ) )
19 18 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  A <_s ( abs_s ` A ) )
20 simpr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( abs_s ` A )
21 15 17 6 19 20 slelttrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  A
22 14 21 jca 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( abs_s ` A )  ( ( -us ` A )
23 22 ex 
 |-  ( ( A e. No /\ B e. No ) -> ( ( abs_s ` A )  ( ( -us ` A )
24 abssor 
 |-  ( A e. No -> ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) )
25 24 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) )
26 breq1 
 |-  ( ( abs_s ` A ) = A -> ( ( abs_s ` A )  A
27 26 biimprd 
 |-  ( ( abs_s ` A ) = A -> ( A  ( abs_s ` A )
28 breq1 
 |-  ( ( abs_s ` A ) = ( -us ` A ) -> ( ( abs_s ` A )  ( -us ` A )
29 28 biimprd 
 |-  ( ( abs_s ` A ) = ( -us ` A ) -> ( ( -us ` A )  ( abs_s ` A )
30 27 29 jaoa 
 |-  ( ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) -> ( ( A  ( abs_s ` A )
31 30 ancomsd 
 |-  ( ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) -> ( ( ( -us ` A )  ( abs_s ` A )
32 25 31 syl 
 |-  ( ( A e. No /\ B e. No ) -> ( ( ( -us ` A )  ( abs_s ` A )
33 23 32 impbid 
 |-  ( ( A e. No /\ B e. No ) -> ( ( abs_s ` A )  ( ( -us ` A )
34 1 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( -us ` A ) e. No )
35 simpr 
 |-  ( ( A e. No /\ B e. No ) -> B e. No )
36 34 35 sltnegd 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` A )  ( -us ` B )
37 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
38 37 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( -us ` ( -us ` A ) ) = A )
39 38 breq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` B )  ( -us ` B )
40 36 39 bitrd 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` A )  ( -us ` B )
41 40 anbi1d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( ( -us ` A )  ( ( -us ` B )
42 33 41 bitrd 
 |-  ( ( A e. No /\ B e. No ) -> ( ( abs_s ` A )  ( ( -us ` B )