Theorem addsgt0d

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

	Ref	Expression
Hypotheses	addsgt0d.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsgt0d.2	$$⊢\phi \to B\in \mathrm{No}$$
	addsgt0d.3	No typesetting found for |- ( ph -> 0s
	addsgt0d.4	No typesetting found for |- ( ph -> 0s
Assertion	addsgt0d	Could not format assertion : No typesetting found for |- ( ph -> 0s

Proof

Step	Hyp	Ref	Expression
1		addsgt0d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsgt0d.2	$$⊢\phi \to B\in \mathrm{No}$$
3		addsgt0d.3	Could not format ( ph -> 0s 0s
4		addsgt0d.4	Could not format ( ph -> 0s 0s
5		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
6		addsrid	Could not format ( 0s e. No -> ( 0s +s 0s ) = 0s ) : No typesetting found for |- ( 0s e. No -> ( 0s +s 0s ) = 0s ) with typecode |-
7	5 6	ax-mp	Could not format ( 0s +s 0s ) = 0s : No typesetting found for |- ( 0s +s 0s ) = 0s with typecode |-
8	5	a1i	Could not format ( ph -> 0s e. No ) : No typesetting found for |- ( ph -> 0s e. No ) with typecode |-
9	8 8 1 2 3 4	slt2addd	Could not format ( ph -> ( 0s +s 0s ) ( 0s +s 0s )
10	7 9	eqbrtrrid	Could not format ( ph -> 0s 0s