Theorem nnsrecgt0d

Description: The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025)

	Ref	Expression
Hypothesis	nnsrecgt0d.1	⊢ ( 𝜑 → 𝐴 ∈ ℕs )
Assertion	nnsrecgt0d	⊢ ( 𝜑 → 0s <s ( 1s /su 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nnsrecgt0d.1	⊢ ( 𝜑 → 𝐴 ∈ ℕs )
2	1	nnnod	⊢ ( 𝜑 → 𝐴 ∈ No )
3		muls02	⊢ ( 𝐴 ∈ No → ( 0s ·s 𝐴 ) = 0s )
4	2 3	syl	⊢ ( 𝜑 → ( 0s ·s 𝐴 ) = 0s )
5		0lt1s	⊢ 0s <s 1s
6	4 5	eqbrtrdi	⊢ ( 𝜑 → ( 0s ·s 𝐴 ) <s 1s )
7		0no	⊢ 0s ∈ No
8	7	a1i	⊢ ( 𝜑 → 0s ∈ No )
9		1no	⊢ 1s ∈ No
10	9	a1i	⊢ ( 𝜑 → 1s ∈ No )
11		nnsgt0	⊢ ( 𝐴 ∈ ℕs → 0s <s 𝐴 )
12	1 11	syl	⊢ ( 𝜑 → 0s <s 𝐴 )
13	8 10 2 12	ltmuldivsd	⊢ ( 𝜑 → ( ( 0s ·s 𝐴 ) <s 1s ↔ 0s <s ( 1s /su 𝐴 ) ) )
14	6 13	mpbid	⊢ ( 𝜑 → 0s <s ( 1s /su 𝐴 ) )