Metamath Proof Explorer

Theorem abslts

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

Ref Expression
Assertion abslts ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ A < s B ↔ + s ⁡ B < s A ∧ A < s B

Proof

Step Hyp Ref Expression
1 negscl ⊢ A ∈ No → + s ⁡ A ∈ No
2 1 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → + s ⁡ A ∈ No
3 absscl ⊢ + s ⁡ A ∈ No → abs s ⁡ + s ⁡ A ∈ No
4 1 3 syl ⊢ A ∈ No → abs s ⁡ + s ⁡ A ∈ No
5 4 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → abs s ⁡ + s ⁡ A ∈ No
6 simplr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → B ∈ No
7 leabss ⊢ + s ⁡ A ∈ No → + s ⁡ A ≤ s abs s ⁡ + s ⁡ A
8 1 7 syl ⊢ A ∈ No → + s ⁡ A ≤ s abs s ⁡ + s ⁡ A
9 8 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → + s ⁡ A ≤ s abs s ⁡ + s ⁡ A
10 absnegs ⊢ A ∈ No → abs s ⁡ + s ⁡ A = abs s ⁡ A
11 10 adantr ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ + s ⁡ A = abs s ⁡ A
12 11 breq1d ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ + s ⁡ A < s B ↔ abs s ⁡ A < s B
13 12 biimpar ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → abs s ⁡ + s ⁡ A < s B
14 2 5 6 9 13 leltstrd ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → + s ⁡ A < s B
15 simpll ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → A ∈ No
16 absscl ⊢ A ∈ No → abs s ⁡ A ∈ No
17 16 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → abs s ⁡ A ∈ No
18 leabss ⊢ A ∈ No → A ≤ s abs s ⁡ A
19 18 ad2antrr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → A ≤ s abs s ⁡ A
20 simpr ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → abs s ⁡ A < s B
21 15 17 6 19 20 leltstrd ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → A < s B
22 14 21 jca ⊢ A ∈ No ∧ B ∈ No ∧ abs s ⁡ A < s B → + s ⁡ A < s B ∧ A < s B
23 22 ex ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ A < s B → + s ⁡ A < s B ∧ A < s B
24 abssor ⊢ A ∈ No → abs s ⁡ A = A ∨ abs s ⁡ A = + s ⁡ A
25 24 adantr ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ A = A ∨ abs s ⁡ A = + s ⁡ A
26 breq1 ⊢ abs s ⁡ A = A → abs s ⁡ A < s B ↔ A < s B
27 26 biimprd ⊢ abs s ⁡ A = A → A < s B → abs s ⁡ A < s B
28 breq1 ⊢ abs s ⁡ A = + s ⁡ A → abs s ⁡ A < s B ↔ + s ⁡ A < s B
29 28 biimprd ⊢ abs s ⁡ A = + s ⁡ A → + s ⁡ A < s B → abs s ⁡ A < s B
30 27 29 jaoa ⊢ abs s ⁡ A = A ∨ abs s ⁡ A = + s ⁡ A → A < s B ∧ + s ⁡ A < s B → abs s ⁡ A < s B
31 30 ancomsd ⊢ abs s ⁡ A = A ∨ abs s ⁡ A = + s ⁡ A → + s ⁡ A < s B ∧ A < s B → abs s ⁡ A < s B
32 25 31 syl ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A < s B ∧ A < s B → abs s ⁡ A < s B
33 23 32 impbid ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ A < s B ↔ + s ⁡ A < s B ∧ A < s B
34 1 adantr ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A ∈ No
35 simpr ⊢ A ∈ No ∧ B ∈ No → B ∈ No
36 34 35 ltnegsd ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A < s B ↔ + s ⁡ B < s + s ⁡ + s ⁡ A
37 negnegs ⊢ A ∈ No → + s ⁡ + s ⁡ A = A
38 37 adantr ⊢ A ∈ No ∧ B ∈ No → + s ⁡ + s ⁡ A = A
39 38 breq2d ⊢ A ∈ No ∧ B ∈ No → + s ⁡ B < s + s ⁡ + s ⁡ A ↔ + s ⁡ B < s A
40 36 39 bitrd ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A < s B ↔ + s ⁡ B < s A
41 40 anbi1d ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A < s B ∧ A < s B ↔ + s ⁡ B < s A ∧ A < s B
42 33 41 bitrd ⊢ A ∈ No ∧ B ∈ No → abs s ⁡ A < s B ↔ + s ⁡ B < s A ∧ A < s B