Theorem mulsgt0

Description: The product of two positive surreals is positive. Theorem 9 of Conway p. 20. (Contributed by Scott Fenton, 6-Mar-2025)

	Ref	Expression
Assertion	mulsgt0	|- ( ( ( A e. No /\ 0s 0s

Proof

Step	Hyp	Ref	Expression
1		0sno	|- 0s e. No
2	1	a1i	|- ( ( ( A e. No /\ 0s 0s e. No )
3		simpll	|- ( ( ( A e. No /\ 0s A e. No )
4		simprl	|- ( ( ( A e. No /\ 0s B e. No )
5		simplr	|- ( ( ( A e. No /\ 0s 0s
6		simprr	|- ( ( ( A e. No /\ 0s 0s
7	2 3 2 4 5 6	sltmuld	|- ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) )
8		muls02	|- ( B e. No -> ( 0s x.s B ) = 0s )
9	4 8	syl	|- ( ( ( A e. No /\ 0s ( 0s x.s B ) = 0s )
10		muls02	|- ( 0s e. No -> ( 0s x.s 0s ) = 0s )
11	1 10	ax-mp	|- ( 0s x.s 0s ) = 0s
12	11	a1i	|- ( ( ( A e. No /\ 0s ( 0s x.s 0s ) = 0s )
13	9 12	oveq12d	|- ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) = ( 0s -s 0s ) )
14		subsid	|- ( 0s e. No -> ( 0s -s 0s ) = 0s )
15	1 14	ax-mp	|- ( 0s -s 0s ) = 0s
16	13 15	eqtrdi	|- ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) = 0s )
17		muls01	|- ( A e. No -> ( A x.s 0s ) = 0s )
18	3 17	syl	|- ( ( ( A e. No /\ 0s ( A x.s 0s ) = 0s )
19	18	oveq2d	|- ( ( ( A e. No /\ 0s ( ( A x.s B ) -s ( A x.s 0s ) ) = ( ( A x.s B ) -s 0s ) )
20		mulscl	|- ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No )
21	20	ad2ant2r	|- ( ( ( A e. No /\ 0s ( A x.s B ) e. No )
22		subsid1	|- ( ( A x.s B ) e. No -> ( ( A x.s B ) -s 0s ) = ( A x.s B ) )
23	21 22	syl	|- ( ( ( A e. No /\ 0s ( ( A x.s B ) -s 0s ) = ( A x.s B ) )
24	19 23	eqtrd	|- ( ( ( A e. No /\ 0s ( ( A x.s B ) -s ( A x.s 0s ) ) = ( A x.s B ) )
25	7 16 24	3brtr3d	|- ( ( ( A e. No /\ 0s 0s