Theorem mulsge0d

Description: The product of two non-negative surreals is non-negative. (Contributed by Scott Fenton, 6-Mar-2025)

	Ref	Expression
Hypotheses	mulsge0d.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsge0d.2	$$⊢\phi \to B\in \mathrm{No}$$
	mulsge0d.3	No typesetting found for |- ( ph -> 0s <_s A ) with typecode |-
	mulsge0d.4	No typesetting found for |- ( ph -> 0s <_s B ) with typecode |-
Assertion	mulsge0d	Could not format assertion : No typesetting found for |- ( ph -> 0s <_s ( A x.s B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulsge0d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulsge0d.2	$$⊢\phi \to B\in \mathrm{No}$$
3		mulsge0d.3	Could not format ( ph -> 0s <_s A ) : No typesetting found for |- ( ph -> 0s <_s A ) with typecode |-
4		mulsge0d.4	Could not format ( ph -> 0s <_s B ) : No typesetting found for |- ( ph -> 0s <_s B ) with typecode |-
5		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
6	5	a1i	Could not format ( ( ( ph /\ 0s 0s e. No ) : No typesetting found for |- ( ( ( ph /\ 0s 0s e. No ) with typecode |-
7	1 2	mulscld	Could not format ( ph -> ( A x.s B ) e. No ) : No typesetting found for |- ( ph -> ( A x.s B ) e. No ) with typecode |-
8	7	ad2antrr	Could not format ( ( ( ph /\ 0s ( A x.s B ) e. No ) : No typesetting found for |- ( ( ( ph /\ 0s ( A x.s B ) e. No ) with typecode |-
9	1	ad2antrr	Could not format ( ( ( ph /\ 0s A e. No ) : No typesetting found for |- ( ( ( ph /\ 0s A e. No ) with typecode |-
10	2	ad2antrr	Could not format ( ( ( ph /\ 0s B e. No ) : No typesetting found for |- ( ( ( ph /\ 0s B e. No ) with typecode |-
11		simplr	Could not format ( ( ( ph /\ 0s 0s 0s
12		simpr	Could not format ( ( ( ph /\ 0s 0s 0s
13	9 10 11 12	mulsgt0d	Could not format ( ( ( ph /\ 0s 0s 0s
14	6 8 13	sltled	Could not format ( ( ( ph /\ 0s 0s <_s ( A x.s B ) ) : No typesetting found for |- ( ( ( ph /\ 0s 0s <_s ( A x.s B ) ) with typecode |-
15		slerflex	Could not format ( 0s e. No -> 0s <_s 0s ) : No typesetting found for |- ( 0s e. No -> 0s <_s 0s ) with typecode |-
16	5 15	ax-mp	Could not format 0s <_s 0s : No typesetting found for |- 0s <_s 0s with typecode |-
17		oveq2	Could not format ( 0s = B -> ( A x.s 0s ) = ( A x.s B ) ) : No typesetting found for |- ( 0s = B -> ( A x.s 0s ) = ( A x.s B ) ) with typecode |-
18	17	adantl	Could not format ( ( ph /\ 0s = B ) -> ( A x.s 0s ) = ( A x.s B ) ) : No typesetting found for |- ( ( ph /\ 0s = B ) -> ( A x.s 0s ) = ( A x.s B ) ) with typecode |-
19		muls01	Could not format ( A e. No -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |-
20	1 19	syl	Could not format ( ph -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( A x.s 0s ) = 0s ) with typecode |-
21	20	adantr	Could not format ( ( ph /\ 0s = B ) -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( ( ph /\ 0s = B ) -> ( A x.s 0s ) = 0s ) with typecode |-
22	18 21	eqtr3d	Could not format ( ( ph /\ 0s = B ) -> ( A x.s B ) = 0s ) : No typesetting found for |- ( ( ph /\ 0s = B ) -> ( A x.s B ) = 0s ) with typecode |-
23	16 22	breqtrrid	Could not format ( ( ph /\ 0s = B ) -> 0s <_s ( A x.s B ) ) : No typesetting found for |- ( ( ph /\ 0s = B ) -> 0s <_s ( A x.s B ) ) with typecode |-
24	23	adantlr	Could not format ( ( ( ph /\ 0s 0s <_s ( A x.s B ) ) : No typesetting found for |- ( ( ( ph /\ 0s 0s <_s ( A x.s B ) ) with typecode |-
25		sleloe	Could not format ( ( 0s e. No /\ B e. No ) -> ( 0s <_s B <-> ( 0s ( 0s <_s B <-> ( 0s
26	5 2 25	sylancr	Could not format ( ph -> ( 0s <_s B <-> ( 0s ( 0s <_s B <-> ( 0s
27	4 26	mpbid	Could not format ( ph -> ( 0s ( 0s
28	27	adantr	Could not format ( ( ph /\ 0s ( 0s ( 0s
29	14 24 28	mpjaodan	Could not format ( ( ph /\ 0s 0s <_s ( A x.s B ) ) : No typesetting found for |- ( ( ph /\ 0s 0s <_s ( A x.s B ) ) with typecode |-
30		oveq1	Could not format ( 0s = A -> ( 0s x.s B ) = ( A x.s B ) ) : No typesetting found for |- ( 0s = A -> ( 0s x.s B ) = ( A x.s B ) ) with typecode |-
31	30	adantl	Could not format ( ( ph /\ 0s = A ) -> ( 0s x.s B ) = ( A x.s B ) ) : No typesetting found for |- ( ( ph /\ 0s = A ) -> ( 0s x.s B ) = ( A x.s B ) ) with typecode |-
32		muls02	Could not format ( B e. No -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( B e. No -> ( 0s x.s B ) = 0s ) with typecode |-
33	2 32	syl	Could not format ( ph -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( ph -> ( 0s x.s B ) = 0s ) with typecode |-
34	33	adantr	Could not format ( ( ph /\ 0s = A ) -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( ( ph /\ 0s = A ) -> ( 0s x.s B ) = 0s ) with typecode |-
35	31 34	eqtr3d	Could not format ( ( ph /\ 0s = A ) -> ( A x.s B ) = 0s ) : No typesetting found for |- ( ( ph /\ 0s = A ) -> ( A x.s B ) = 0s ) with typecode |-
36	16 35	breqtrrid	Could not format ( ( ph /\ 0s = A ) -> 0s <_s ( A x.s B ) ) : No typesetting found for |- ( ( ph /\ 0s = A ) -> 0s <_s ( A x.s B ) ) with typecode |-
37		sleloe	Could not format ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A <-> ( 0s ( 0s <_s A <-> ( 0s
38	5 1 37	sylancr	Could not format ( ph -> ( 0s <_s A <-> ( 0s ( 0s <_s A <-> ( 0s
39	3 38	mpbid	Could not format ( ph -> ( 0s ( 0s
40	29 36 39	mpjaodan	Could not format ( ph -> 0s <_s ( A x.s B ) ) : No typesetting found for |- ( ph -> 0s <_s ( A x.s B ) ) with typecode |-