Metamath Proof Explorer

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 
|- ( ph -> A e. No )
mulsge0d.2 
|- ( ph -> B e. No )
mulsge0d.3 
|- ( ph -> 0s <_s A )
mulsge0d.4 
|- ( ph -> 0s <_s B )
Assertion mulsge0d 
|- ( ph -> 0s <_s ( A x.s B ) )

Proof

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