Theorem ltsm1d

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

	Ref	Expression
Hypothesis	ltsm1d.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	ltsm1d	$$⊢\phi \to \left(A{-}_s{1}_s\right){<}_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		ltsm1d.1	$$⊢\phi \to A\in \mathrm{No}$$
2	1	ltsp1d	$$⊢\phi \to A{<}_s\left(A{+}_s{1}_s\right)$$
3		1no	$$⊢1_s\in \mathrm{No}$$
4	3	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
5	1 4 1	ltsubaddsd	$$⊢\phi \to \left(\left(A{-}_s{1}_s\right){<}_{s}A\leftrightarrow A{<}_s\left(A{+}_s{1}_s\right)\right)$$
6	2 5	mpbird	$$⊢\phi \to \left(A{-}_s{1}_s\right){<}_{s}A$$