Metamath Proof Explorer


Theorem absslt

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

Ref Expression
Assertion absslt ( ( 𝐴 No 𝐵 No ) → ( ( abss𝐴 ) <s 𝐵 ↔ ( ( -us𝐵 ) <s 𝐴𝐴 <s 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 negscl ( 𝐴 No → ( -us𝐴 ) ∈ No )
2 1 ad2antrr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( -us𝐴 ) ∈ No )
3 absscl ( ( -us𝐴 ) ∈ No → ( abss ‘ ( -us𝐴 ) ) ∈ No )
4 1 3 syl ( 𝐴 No → ( abss ‘ ( -us𝐴 ) ) ∈ No )
5 4 ad2antrr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( abss ‘ ( -us𝐴 ) ) ∈ No )
6 simplr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → 𝐵 No )
7 sleabs ( ( -us𝐴 ) ∈ No → ( -us𝐴 ) ≤s ( abss ‘ ( -us𝐴 ) ) )
8 1 7 syl ( 𝐴 No → ( -us𝐴 ) ≤s ( abss ‘ ( -us𝐴 ) ) )
9 8 ad2antrr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( -us𝐴 ) ≤s ( abss ‘ ( -us𝐴 ) ) )
10 abssneg ( 𝐴 No → ( abss ‘ ( -us𝐴 ) ) = ( abss𝐴 ) )
11 10 adantr ( ( 𝐴 No 𝐵 No ) → ( abss ‘ ( -us𝐴 ) ) = ( abss𝐴 ) )
12 11 breq1d ( ( 𝐴 No 𝐵 No ) → ( ( abss ‘ ( -us𝐴 ) ) <s 𝐵 ↔ ( abss𝐴 ) <s 𝐵 ) )
13 12 biimpar ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( abss ‘ ( -us𝐴 ) ) <s 𝐵 )
14 2 5 6 9 13 slelttrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( -us𝐴 ) <s 𝐵 )
15 simpll ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → 𝐴 No )
16 absscl ( 𝐴 No → ( abss𝐴 ) ∈ No )
17 16 ad2antrr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( abss𝐴 ) ∈ No )
18 sleabs ( 𝐴 No 𝐴 ≤s ( abss𝐴 ) )
19 18 ad2antrr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → 𝐴 ≤s ( abss𝐴 ) )
20 simpr ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( abss𝐴 ) <s 𝐵 )
21 15 17 6 19 20 slelttrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → 𝐴 <s 𝐵 )
22 14 21 jca ( ( ( 𝐴 No 𝐵 No ) ∧ ( abss𝐴 ) <s 𝐵 ) → ( ( -us𝐴 ) <s 𝐵𝐴 <s 𝐵 ) )
23 22 ex ( ( 𝐴 No 𝐵 No ) → ( ( abss𝐴 ) <s 𝐵 → ( ( -us𝐴 ) <s 𝐵𝐴 <s 𝐵 ) ) )
24 abssor ( 𝐴 No → ( ( abss𝐴 ) = 𝐴 ∨ ( abss𝐴 ) = ( -us𝐴 ) ) )
25 24 adantr ( ( 𝐴 No 𝐵 No ) → ( ( abss𝐴 ) = 𝐴 ∨ ( abss𝐴 ) = ( -us𝐴 ) ) )
26 breq1 ( ( abss𝐴 ) = 𝐴 → ( ( abss𝐴 ) <s 𝐵𝐴 <s 𝐵 ) )
27 26 biimprd ( ( abss𝐴 ) = 𝐴 → ( 𝐴 <s 𝐵 → ( abss𝐴 ) <s 𝐵 ) )
28 breq1 ( ( abss𝐴 ) = ( -us𝐴 ) → ( ( abss𝐴 ) <s 𝐵 ↔ ( -us𝐴 ) <s 𝐵 ) )
29 28 biimprd ( ( abss𝐴 ) = ( -us𝐴 ) → ( ( -us𝐴 ) <s 𝐵 → ( abss𝐴 ) <s 𝐵 ) )
30 27 29 jaoa ( ( ( abss𝐴 ) = 𝐴 ∨ ( abss𝐴 ) = ( -us𝐴 ) ) → ( ( 𝐴 <s 𝐵 ∧ ( -us𝐴 ) <s 𝐵 ) → ( abss𝐴 ) <s 𝐵 ) )
31 30 ancomsd ( ( ( abss𝐴 ) = 𝐴 ∨ ( abss𝐴 ) = ( -us𝐴 ) ) → ( ( ( -us𝐴 ) <s 𝐵𝐴 <s 𝐵 ) → ( abss𝐴 ) <s 𝐵 ) )
32 25 31 syl ( ( 𝐴 No 𝐵 No ) → ( ( ( -us𝐴 ) <s 𝐵𝐴 <s 𝐵 ) → ( abss𝐴 ) <s 𝐵 ) )
33 23 32 impbid ( ( 𝐴 No 𝐵 No ) → ( ( abss𝐴 ) <s 𝐵 ↔ ( ( -us𝐴 ) <s 𝐵𝐴 <s 𝐵 ) ) )
34 1 adantr ( ( 𝐴 No 𝐵 No ) → ( -us𝐴 ) ∈ No )
35 simpr ( ( 𝐴 No 𝐵 No ) → 𝐵 No )
36 34 35 sltnegd ( ( 𝐴 No 𝐵 No ) → ( ( -us𝐴 ) <s 𝐵 ↔ ( -us𝐵 ) <s ( -us ‘ ( -us𝐴 ) ) ) )
37 negnegs ( 𝐴 No → ( -us ‘ ( -us𝐴 ) ) = 𝐴 )
38 37 adantr ( ( 𝐴 No 𝐵 No ) → ( -us ‘ ( -us𝐴 ) ) = 𝐴 )
39 38 breq2d ( ( 𝐴 No 𝐵 No ) → ( ( -us𝐵 ) <s ( -us ‘ ( -us𝐴 ) ) ↔ ( -us𝐵 ) <s 𝐴 ) )
40 36 39 bitrd ( ( 𝐴 No 𝐵 No ) → ( ( -us𝐴 ) <s 𝐵 ↔ ( -us𝐵 ) <s 𝐴 ) )
41 40 anbi1d ( ( 𝐴 No 𝐵 No ) → ( ( ( -us𝐴 ) <s 𝐵𝐴 <s 𝐵 ) ↔ ( ( -us𝐵 ) <s 𝐴𝐴 <s 𝐵 ) ) )
42 33 41 bitrd ( ( 𝐴 No 𝐵 No ) → ( ( abss𝐴 ) <s 𝐵 ↔ ( ( -us𝐵 ) <s 𝐴𝐴 <s 𝐵 ) ) )