Metamath Proof Explorer


Theorem sltm1d

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

Ref Expression
Hypothesis sltm1d.1 φ A No
Assertion sltm1d φ A - s 1 s < s A

Proof

Step Hyp Ref Expression
1 sltm1d.1 φ A No
2 1 sltp1d φ A < s A + s 1 s
3 1sno 1 s No
4 3 a1i φ 1 s No
5 1 4 1 sltsubaddd φ A - s 1 s < s A A < s A + s 1 s
6 2 5 mpbird φ A - s 1 s < s A