Description: A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sltm1d.1 | ||
Assertion | sltm1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sltm1d.1 | ||
2 | 1 | sltp1d | |
3 | 1sno | ||
4 | 3 | a1i | |
5 | 1 4 1 | sltsubaddd | |
6 | 2 5 | mpbird |