Theorem nnsrecgt0d

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

	Ref	Expression
Hypothesis	nnsrecgt0d.1	|- ( ph -> A e. NN_s )
Assertion	nnsrecgt0d	|- ( ph -> 0s

Proof

Step	Hyp	Ref	Expression
1		nnsrecgt0d.1	|- ( ph -> A e. NN_s )
2	1	nnsnod	|- ( ph -> A e. No )
3		muls02	|- ( A e. No -> ( 0s x.s A ) = 0s )
4	2 3	syl	|- ( ph -> ( 0s x.s A ) = 0s )
5		0slt1s	|- 0s
6	4 5	eqbrtrdi	|- ( ph -> ( 0s x.s A )
7		0sno	|- 0s e. No
8	7	a1i	|- ( ph -> 0s e. No )
9		1sno	|- 1s e. No
10	9	a1i	|- ( ph -> 1s e. No )
11		nnsgt0	|- ( A e. NN_s -> 0s
12	1 11	syl	|- ( ph -> 0s
13	8 10 2 12	sltmuldivd	|- ( ph -> ( ( 0s x.s A ) 0s
14	6 13	mpbid	|- ( ph -> 0s