Metamath Proof Explorer


Theorem sltnegim

Description: The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion sltnegim A No B No A < s B + s B < s + s A

Proof

Step Hyp Ref Expression
1 negsprop A No B No + s A No A < s B + s B < s + s A
2 1 simprd A No B No A < s B + s B < s + s A