Theorem nnsrecgt0d

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

	Ref	Expression
Hypothesis	nnsrecgt0d.1	$$⊢\phi \to A\in {\mathbb{N}}_s$$
Assertion	nnsrecgt0d	$$⊢\phi \to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnsrecgt0d.1	$$⊢\phi \to A\in {\mathbb{N}}_s$$
2	1	nnnod	$$⊢\phi \to A\in \mathrm{No}$$
3		muls02	$$⊢A\in \mathrm{No}\to 0_s{\cdot }_{s}A=0_s$$
4	2 3	syl	$$⊢\phi \to 0_s{\cdot }_{s}A=0_s$$
5		0lt1s	$$⊢0_s{<}_s{1}_s$$
6	4 5	eqbrtrdi	$$⊢\phi \to \left(0_s{\cdot }_{s}A\right){<}_s{1}_s$$
7		0no	$$⊢0_s\in \mathrm{No}$$
8	7	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
9		1no	$$⊢1_s\in \mathrm{No}$$
10	9	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
11		nnsgt0	$$⊢A\in {\mathbb{N}}_s\to 0_s{<}_{s}A$$
12	1 11	syl	$$⊢\phi \to 0_s{<}_{s}A$$
13	8 10 2 12	ltmuldivsd	$$⊢\phi \to \left(\left(0_s{\cdot }_{s}A\right){<}_s{1}_s\leftrightarrow 0_s{<}_s\left(1_s{/}_{\mathrm{su}}A\right)\right)$$
14	6 13	mpbid	$$⊢\phi \to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}A\right)$$