Theorem abslts

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

	Ref	Expression
Assertion	abslts	⊢ ( ( 𝐴 ∈ 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		leabss	⊢ ( ( -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		absnegs	⊢ ( 𝐴 ∈ 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	leltstrd	⊢ ( ( ( 𝐴 ∈ 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		leabss	⊢ ( 𝐴 ∈ 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	leltstrd	⊢ ( ( ( 𝐴 ∈ 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	ltnegsd	⊢ ( ( 𝐴 ∈ 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 𝐵 ) ) )