Metamath Proof Explorer


Theorem slt0neg2d

Description: Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypothesis slt0neg2d.1 φ A No
Assertion slt0neg2d φ 0 s < s A + s A < s 0 s

Proof

Step Hyp Ref Expression
1 slt0neg2d.1 φ A No
2 0sno 0 s No
3 sltneg 0 s No A No 0 s < s A + s A < s + s 0 s
4 2 1 3 sylancr φ 0 s < s A + s A < s + s 0 s
5 negs0s + s 0 s = 0 s
6 5 breq2i + s A < s + s 0 s + s A < s 0 s
7 4 6 bitrdi φ 0 s < s A + s A < s 0 s