Metamath Proof Explorer

Theorem lemuls1ad

Description: Multiplication of both sides of surreal less-than or equal by a non-negative number. (Contributed by Scott Fenton, 17-Apr-2025)

Ref Expression
Hypotheses lemuls1ad.1 
|- ( ph -> A e. No )
lemuls1ad.2 
|- ( ph -> B e. No )
lemuls1ad.3 
|- ( ph -> C e. No )
lemuls1ad.4 
|- ( ph -> 0s <_s C )
lemuls1ad.5 
|- ( ph -> A <_s B )
Assertion lemuls1ad 
|- ( ph -> ( A x.s C ) <_s ( B x.s C ) )

Proof

Step Hyp Ref Expression
1 lemuls1ad.1 
 |-  ( ph -> A e. No )
2 lemuls1ad.2 
 |-  ( ph -> B e. No )
3 lemuls1ad.3 
 |-  ( ph -> C e. No )
4 lemuls1ad.4 
 |-  ( ph -> 0s <_s C )
5 lemuls1ad.5 
 |-  ( ph -> A <_s B )
6 5 adantr 
 |-  ( ( ph /\ 0s  A <_s B )
7 1 adantr 
 |-  ( ( ph /\ 0s  A e. No )
8 2 adantr 
 |-  ( ( ph /\ 0s  B e. No )
9 3 adantr 
 |-  ( ( ph /\ 0s  C e. No )
10 simpr 
 |-  ( ( ph /\ 0s  0s
11 7 8 9 10 lemuls1d 
 |-  ( ( ph /\ 0s  ( A <_s B <-> ( A x.s C ) <_s ( B x.s C ) ) )
12 6 11 mpbid 
 |-  ( ( ph /\ 0s  ( A x.s C ) <_s ( B x.s C ) )
13 0no 
 |-  0s e. No
14 lesid 
 |-  ( 0s e. No -> 0s <_s 0s )
15 13 14 mp1i 
 |-  ( ph -> 0s <_s 0s )
16 muls01 
 |-  ( A e. No -> ( A x.s 0s ) = 0s )
17 1 16 syl 
 |-  ( ph -> ( A x.s 0s ) = 0s )
18 muls01 
 |-  ( B e. No -> ( B x.s 0s ) = 0s )
19 2 18 syl 
 |-  ( ph -> ( B x.s 0s ) = 0s )
20 15 17 19 3brtr4d 
 |-  ( ph -> ( A x.s 0s ) <_s ( B x.s 0s ) )
21 oveq2 
 |-  ( 0s = C -> ( A x.s 0s ) = ( A x.s C ) )
22 oveq2 
 |-  ( 0s = C -> ( B x.s 0s ) = ( B x.s C ) )
23 21 22 breq12d 
 |-  ( 0s = C -> ( ( A x.s 0s ) <_s ( B x.s 0s ) <-> ( A x.s C ) <_s ( B x.s C ) ) )
24 20 23 syl5ibcom 
 |-  ( ph -> ( 0s = C -> ( A x.s C ) <_s ( B x.s C ) ) )
25 24 imp 
 |-  ( ( ph /\ 0s = C ) -> ( A x.s C ) <_s ( B x.s C ) )
26 lesloe 
 |-  ( ( 0s e. No /\ C e. No ) -> ( 0s <_s C <-> ( 0s
27 13 3 26 sylancr 
 |-  ( ph -> ( 0s <_s C <-> ( 0s
28 4 27 mpbid 
 |-  ( ph -> ( 0s
29 12 25 28 mpjaodan 
 |-  ( ph -> ( A x.s C ) <_s ( B x.s C ) )