Theorem leabss

Description: A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	leabss	⊢ ( 𝐴 ∈ No → 𝐴 ≤s ( abss ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		lesid	⊢ ( 𝐴 ∈ No → 𝐴 ≤s 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → 𝐴 ≤s 𝐴 )
3		abssid	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( abss ‘ 𝐴 ) = 𝐴 )
4	2 3	breqtrrd	⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → 𝐴 ≤s ( abss ‘ 𝐴 ) )
5		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 𝐴 ∈ No )
6		0no	⊢ 0s ∈ No
7	6	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 0s ∈ No )
8		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
9	8	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( -us ‘ 𝐴 ) ∈ No )
10		simpr	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 𝐴 ≤s 0s )
11		neg0s	⊢ ( -us ‘ 0s ) = 0s
12	5 7	lenegsd	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
13	10 12	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) )
14	11 13	eqbrtrrid	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 0s ≤s ( -us ‘ 𝐴 ) )
15	5 7 9 10 14	lestrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 𝐴 ≤s ( -us ‘ 𝐴 ) )
16		abssnid	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) )
17	15 16	breqtrrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → 𝐴 ≤s ( abss ‘ 𝐴 ) )
18		lestric	⊢ ( ( 0s ∈ No ∧ 𝐴 ∈ No ) → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
19	6 18	mpan	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
20	4 17 19	mpjaodan	⊢ ( 𝐴 ∈ No → 𝐴 ≤s ( abss ‘ 𝐴 ) )