Metamath Proof Explorer


Theorem posdifsd

Description: Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses posdifsd.1 φ A No
posdifsd.2 φ B No
Assertion posdifsd φ A < s B 0 s < s B - s A

Proof

Step Hyp Ref Expression
1 posdifsd.1 φ A No
2 posdifsd.2 φ B No
3 0sno 0 s No
4 3 a1i φ 0 s No
5 2 1 subscld φ B - s A No
6 4 5 1 sltadd1d φ 0 s < s B - s A 0 s + s A < s B - s A + s A
7 addslid A No 0 s + s A = A
8 1 7 syl φ 0 s + s A = A
9 npcans B No A No B - s A + s A = B
10 2 1 9 syl2anc φ B - s A + s A = B
11 8 10 breq12d φ 0 s + s A < s B - s A + s A A < s B
12 6 11 bitr2d φ A < s B 0 s < s B - s A