Theorem addsgt0d

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

	Ref	Expression
Hypotheses	addsgt0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	addsgt0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	addsgt0d.3	⊢ ( 𝜑 → 0s <s 𝐴 )
	addsgt0d.4	⊢ ( 𝜑 → 0s <s 𝐵 )
Assertion	addsgt0d	⊢ ( 𝜑 → 0s <s ( 𝐴 +s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		addsgt0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		addsgt0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		addsgt0d.3	⊢ ( 𝜑 → 0s <s 𝐴 )
4		addsgt0d.4	⊢ ( 𝜑 → 0s <s 𝐵 )
5		0no	⊢ 0s ∈ No
6		addsrid	⊢ ( 0s ∈ No → ( 0s +s 0s ) = 0s )
7	5 6	ax-mp	⊢ ( 0s +s 0s ) = 0s
8	5	a1i	⊢ ( 𝜑 → 0s ∈ No )
9	8 8 1 2 3 4	lt2addsd	⊢ ( 𝜑 → ( 0s +s 0s ) <s ( 𝐴 +s 𝐵 ) )
10	7 9	eqbrtrrid	⊢ ( 𝜑 → 0s <s ( 𝐴 +s 𝐵 ) )