mulsge0d

Description: The product of two non-negative surreals is non-negative. (Contributed by Scott Fenton, 6-Mar-2025)

	Ref	Expression
Hypotheses	mulsge0d.1	$⊢ φ \to A \in No$
	mulsge0d.2	$⊢ φ \to B \in No$
	mulsge0d.3	$⊢ φ \to 0_{s} \leq_{s} A$
	mulsge0d.4	$⊢ φ \to 0_{s} \leq_{s} B$
Assertion	mulsge0d	$⊢ φ \to 0_{s} \leq_{s} (A \cdot_{s} B)$

Proof

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

Metamath Proof Explorer

Theorem mulsge0d

Proof