Theorem sltm1d

Description: A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Hypothesis	sltm1d.1	|- ( ph -> A e. No )
Assertion	sltm1d	|- ( ph -> ( A -s 1s )

Proof

Step	Hyp	Ref	Expression
1		sltm1d.1	|- ( ph -> A e. No )
2	1	sltp1d	|- ( ph -> A
3		1sno	|- 1s e. No
4	3	a1i	|- ( ph -> 1s e. No )
5	1 4 1	sltsubaddd	|- ( ph -> ( ( A -s 1s ) A
6	2 5	mpbird	|- ( ph -> ( A -s 1s )