absmuls

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

		Ref	Expression
	Assertion	absmuls	$⊢ (A \in No \land B \in No) \to {abs}_{s} (A \cdot_{s} B) = {abs}_{s} (A) \cdot_{s} {abs}_{s} (B)$

Proof

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

Metamath Proof Explorer

Theorem absmuls

Proof