sleabs

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

		Ref	Expression
	Assertion	sleabs	$⊢ A \in No \to A \leq_{s} {abs}_{s} (A)$

Step	Hyp	Ref	Expression
1		slerflex	$⊢ A \in No \to A \leq_{s} A$
2	1	adantr	$⊢ (A \in No \land 0_{s} \leq_{s} A) \to A \leq_{s} A$
3		abssid	$⊢ (A \in No \land 0_{s} \leq_{s} A) \to {abs}_{s} (A) = A$
4	2 3	breqtrrd	$⊢ (A \in No \land 0_{s} \leq_{s} A) \to A \leq_{s} {abs}_{s} (A)$
5		simpl	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to A \in No$
6		0sno	$⊢ 0_{s} \in No$
7	6	a1i	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to 0_{s} \in No$
8		negscl	$⊢ A \in No \to +_{s} (A) \in No$
9	8	adantr	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to +_{s} (A) \in No$
10		simpr	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to A \leq_{s} 0_{s}$
11		negs0s	$⊢ +_{s} (0_{s}) = 0_{s}$
12	5 7	slenegd	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to (A \leq_{s} 0_{s} \leftrightarrow +_{s} (0_{s}) \leq_{s} +_{s} (A))$
13	10 12	mpbid	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to +_{s} (0_{s}) \leq_{s} +_{s} (A)$
14	11 13	eqbrtrrid	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to 0_{s} \leq_{s} +_{s} (A)$
15	5 7 9 10 14	sletrd	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to A \leq_{s} +_{s} (A)$
16		abssnid	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to {abs}_{s} (A) = +_{s} (A)$
17	15 16	breqtrrd	$⊢ (A \in No \land A \leq_{s} 0_{s}) \to A \leq_{s} {abs}_{s} (A)$
18		sletric	$⊢ (0_{s} \in No \land A \in No) \to (0_{s} \leq_{s} A \lor A \leq_{s} 0_{s})$
19	6 18	mpan	$⊢ A \in No \to (0_{s} \leq_{s} A \lor A \leq_{s} 0_{s})$
20	4 17 19	mpjaodan	$⊢ A \in No \to A \leq_{s} {abs}_{s} (A)$

Metamath Proof Explorer