Metamath Proof Explorer

Theorem absmuls

Description: Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion absmuls 
|- ( ( A e. No /\ B e. No ) -> ( abs_s ` ( A x.s B ) ) = ( ( abs_s ` A ) x.s ( abs_s ` B ) ) )

Proof

Step Hyp Ref Expression
1 mulscl 
 |-  ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No )
2 1 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) -> ( A x.s B ) e. No )
3 simplll 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> A e. No )
4 simpllr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> B e. No )
5 simplr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> 0s <_s A )
6 simpr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> 0s <_s B )
7 3 4 5 6 mulsge0d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> 0s <_s ( A x.s B ) )
8 abssid 
 |-  ( ( ( A x.s B ) e. No /\ 0s <_s ( A x.s B ) ) -> ( abs_s ` ( A x.s B ) ) = ( A x.s B ) )
9 2 7 8 syl2an2r 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> ( abs_s ` ( A x.s B ) ) = ( A x.s B ) )
10 abssid 
 |-  ( ( B e. No /\ 0s <_s B ) -> ( abs_s ` B ) = B )
11 10 ad4ant24 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> ( abs_s ` B ) = B )
12 11 oveq2d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> ( A x.s ( abs_s ` B ) ) = ( A x.s B ) )
13 9 12 eqtr4d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ 0s <_s B ) -> ( abs_s ` ( A x.s B ) ) = ( A x.s ( abs_s ` B ) ) )
14 simplll 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> A e. No )
15 simpllr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> B e. No )
16 14 15 mulnegs2d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( A x.s ( -us ` B ) ) = ( -us ` ( A x.s B ) ) )
17 abssnid 
 |-  ( ( B e. No /\ B <_s 0s ) -> ( abs_s ` B ) = ( -us ` B ) )
18 17 ad4ant24 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( abs_s ` B ) = ( -us ` B ) )
19 18 oveq2d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( A x.s ( abs_s ` B ) ) = ( A x.s ( -us ` B ) ) )
20 negs0s 
 |-  ( -us ` 0s ) = 0s
21 15 negscld 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( -us ` B ) e. No )
22 simplr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> 0s <_s A )
23 simpr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> B <_s 0s )
24 0sno 
 |-  0s e. No
25 24 a1i 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> 0s e. No )
26 15 25 slenegd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( B <_s 0s <-> ( -us ` 0s ) <_s ( -us ` B ) ) )
27 23 26 mpbid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( -us ` 0s ) <_s ( -us ` B ) )
28 20 27 eqbrtrrid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> 0s <_s ( -us ` B ) )
29 14 21 22 28 mulsge0d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> 0s <_s ( A x.s ( -us ` B ) ) )
30 29 16 breqtrd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> 0s <_s ( -us ` ( A x.s B ) ) )
31 20 30 eqbrtrid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( -us ` 0s ) <_s ( -us ` ( A x.s B ) ) )
32 2 adantr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( A x.s B ) e. No )
33 32 25 slenegd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( ( A x.s B ) <_s 0s <-> ( -us ` 0s ) <_s ( -us ` ( A x.s B ) ) ) )
34 31 33 mpbird 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( A x.s B ) <_s 0s )
35 abssnid 
 |-  ( ( ( A x.s B ) e. No /\ ( A x.s B ) <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( -us ` ( A x.s B ) ) )
36 2 34 35 syl2an2r 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( -us ` ( A x.s B ) ) )
37 16 19 36 3eqtr4rd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) /\ B <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( A x.s ( abs_s ` B ) ) )
38 sletric 
 |-  ( ( 0s e. No /\ B e. No ) -> ( 0s <_s B \/ B <_s 0s ) )
39 24 38 mpan 
 |-  ( B e. No -> ( 0s <_s B \/ B <_s 0s ) )
40 39 ad2antlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) -> ( 0s <_s B \/ B <_s 0s ) )
41 13 37 40 mpjaodan 
 |-  ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) -> ( abs_s ` ( A x.s B ) ) = ( A x.s ( abs_s ` B ) ) )
42 abssid 
 |-  ( ( A e. No /\ 0s <_s A ) -> ( abs_s ` A ) = A )
43 42 adantlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) -> ( abs_s ` A ) = A )
44 43 oveq1d 
 |-  ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) -> ( ( abs_s ` A ) x.s ( abs_s ` B ) ) = ( A x.s ( abs_s ` B ) ) )
45 41 44 eqtr4d 
 |-  ( ( ( A e. No /\ B e. No ) /\ 0s <_s A ) -> ( abs_s ` ( A x.s B ) ) = ( ( abs_s ` A ) x.s ( abs_s ` B ) ) )
46 simplll 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> A e. No )
47 simpllr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> B e. No )
48 46 47 mulnegs1d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( ( -us ` A ) x.s B ) = ( -us ` ( A x.s B ) ) )
49 10 ad4ant24 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( abs_s ` B ) = B )
50 49 oveq2d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( ( -us ` A ) x.s ( abs_s ` B ) ) = ( ( -us ` A ) x.s B ) )
51 1 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) -> ( A x.s B ) e. No )
52 46 negscld 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( -us ` A ) e. No )
53 simplr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> A <_s 0s )
54 24 a1i 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> 0s e. No )
55 46 54 slenegd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
56 53 55 mpbid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( -us ` 0s ) <_s ( -us ` A ) )
57 20 56 eqbrtrrid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> 0s <_s ( -us ` A ) )
58 simpr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> 0s <_s B )
59 52 47 57 58 mulsge0d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> 0s <_s ( ( -us ` A ) x.s B ) )
60 59 48 breqtrd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> 0s <_s ( -us ` ( A x.s B ) ) )
61 20 60 eqbrtrid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( -us ` 0s ) <_s ( -us ` ( A x.s B ) ) )
62 51 adantr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( A x.s B ) e. No )
63 62 54 slenegd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( ( A x.s B ) <_s 0s <-> ( -us ` 0s ) <_s ( -us ` ( A x.s B ) ) ) )
64 61 63 mpbird 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( A x.s B ) <_s 0s )
65 51 64 35 syl2an2r 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( abs_s ` ( A x.s B ) ) = ( -us ` ( A x.s B ) ) )
66 48 50 65 3eqtr4rd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ 0s <_s B ) -> ( abs_s ` ( A x.s B ) ) = ( ( -us ` A ) x.s ( abs_s ` B ) ) )
67 simplll 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> A e. No )
68 simpllr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> B e. No )
69 67 68 mul2negsd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( A x.s B ) )
70 17 ad4ant24 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( abs_s ` B ) = ( -us ` B ) )
71 70 oveq2d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( ( -us ` A ) x.s ( abs_s ` B ) ) = ( ( -us ` A ) x.s ( -us ` B ) ) )
72 67 negscld 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( -us ` A ) e. No )
73 68 negscld 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( -us ` B ) e. No )
74 simplr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> A <_s 0s )
75 24 a1i 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> 0s e. No )
76 67 75 slenegd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
77 74 76 mpbid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( -us ` 0s ) <_s ( -us ` A ) )
78 20 77 eqbrtrrid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> 0s <_s ( -us ` A ) )
79 simpr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> B <_s 0s )
80 68 75 slenegd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( B <_s 0s <-> ( -us ` 0s ) <_s ( -us ` B ) ) )
81 79 80 mpbid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( -us ` 0s ) <_s ( -us ` B ) )
82 20 81 eqbrtrrid 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> 0s <_s ( -us ` B ) )
83 72 73 78 82 mulsge0d 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> 0s <_s ( ( -us ` A ) x.s ( -us ` B ) ) )
84 83 69 breqtrd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> 0s <_s ( A x.s B ) )
85 51 84 8 syl2an2r 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( A x.s B ) )
86 69 71 85 3eqtr4rd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) /\ B <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( ( -us ` A ) x.s ( abs_s ` B ) ) )
87 39 ad2antlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) -> ( 0s <_s B \/ B <_s 0s ) )
88 66 86 87 mpjaodan 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( ( -us ` A ) x.s ( abs_s ` B ) ) )
89 abssnid 
 |-  ( ( A e. No /\ A <_s 0s ) -> ( abs_s ` A ) = ( -us ` A ) )
90 89 oveq1d 
 |-  ( ( A e. No /\ A <_s 0s ) -> ( ( abs_s ` A ) x.s ( abs_s ` B ) ) = ( ( -us ` A ) x.s ( abs_s ` B ) ) )
91 90 adantlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) -> ( ( abs_s ` A ) x.s ( abs_s ` B ) ) = ( ( -us ` A ) x.s ( abs_s ` B ) ) )
92 88 91 eqtr4d 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s 0s ) -> ( abs_s ` ( A x.s B ) ) = ( ( abs_s ` A ) x.s ( abs_s ` B ) ) )
93 sletric 
 |-  ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
94 24 93 mpan 
 |-  ( A e. No -> ( 0s <_s A \/ A <_s 0s ) )
95 94 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
96 45 92 95 mpjaodan 
 |-  ( ( A e. No /\ B e. No ) -> ( abs_s ` ( A x.s B ) ) = ( ( abs_s ` A ) x.s ( abs_s ` B ) ) )