Theorem addsgt0d

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

	Ref	Expression
Hypotheses	addsgt0d.1	|- ( ph -> A e. No )
	addsgt0d.2	|- ( ph -> B e. No )
	addsgt0d.3	|- ( ph -> 0s
	addsgt0d.4	|- ( ph -> 0s
Assertion	addsgt0d	|- ( ph -> 0s

Proof

Step	Hyp	Ref	Expression
1		addsgt0d.1	|- ( ph -> A e. No )
2		addsgt0d.2	|- ( ph -> B e. No )
3		addsgt0d.3	|- ( ph -> 0s
4		addsgt0d.4	|- ( ph -> 0s
5		0sno	|- 0s e. No
6		addsrid	|- ( 0s e. No -> ( 0s +s 0s ) = 0s )
7	5 6	ax-mp	|- ( 0s +s 0s ) = 0s
8	5	a1i	|- ( ph -> 0s e. No )
9	8 8 1 2 3 4	slt2addd	|- ( ph -> ( 0s +s 0s )
10	7 9	eqbrtrrid	|- ( ph -> 0s