Theorem addsge01d

Description: A surreal is less-than or equal to itself plus a non-negative surreal. (Contributed by Scott Fenton, 24-Feb-2026)

	Ref	Expression
Hypotheses	addsge01d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	addsge01d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	addsge01d	⊢ ( 𝜑 → ( 0s ≤s 𝐵 ↔ 𝐴 ≤s ( 𝐴 +s 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsge01d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		addsge01d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		0sno	⊢ 0s ∈ No
4	3	a1i	⊢ ( 𝜑 → 0s ∈ No )
5	4 2 1	sleadd2d	⊢ ( 𝜑 → ( 0s ≤s 𝐵 ↔ ( 𝐴 +s 0s ) ≤s ( 𝐴 +s 𝐵 ) ) )
6	1	addsridd	⊢ ( 𝜑 → ( 𝐴 +s 0s ) = 𝐴 )
7	6	breq1d	⊢ ( 𝜑 → ( ( 𝐴 +s 0s ) ≤s ( 𝐴 +s 𝐵 ) ↔ 𝐴 ≤s ( 𝐴 +s 𝐵 ) ) )
8	5 7	bitrd	⊢ ( 𝜑 → ( 0s ≤s 𝐵 ↔ 𝐴 ≤s ( 𝐴 +s 𝐵 ) ) )