Metamath Proof Explorer


Theorem addsgt0d

Description: The sum of two positive surreals is positive. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Hypotheses addsgt0d.1 φ A No
addsgt0d.2 φ B No
addsgt0d.3 φ 0 s < s A
addsgt0d.4 φ 0 s < s B
Assertion addsgt0d φ 0 s < s A + s B

Proof

Step Hyp Ref Expression
1 addsgt0d.1 φ A No
2 addsgt0d.2 φ B No
3 addsgt0d.3 φ 0 s < s A
4 addsgt0d.4 φ 0 s < s B
5 0sno 0 s No
6 addsrid 0 s No 0 s + s 0 s = 0 s
7 5 6 ax-mp 0 s + s 0 s = 0 s
8 5 a1i φ 0 s No
9 8 8 1 2 3 4 slt2addd φ 0 s + s 0 s < s A + s B
10 7 9 eqbrtrrid φ 0 s < s A + s B