Theorem absmuls

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

	Ref	Expression
Assertion	absmuls	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( abss ‘ ( 𝐴 ·s 𝐵 ) ) = ( ( abss ‘ 𝐴 ) ·s ( abss ‘ 𝐵 ) ) )

Proof

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