Theorem mulsge0d

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

	Ref	Expression
Hypotheses	mulsge0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulsge0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	mulsge0d.3	⊢ ( 𝜑 → 0s ≤s 𝐴 )
	mulsge0d.4	⊢ ( 𝜑 → 0s ≤s 𝐵 )
Assertion	mulsge0d	⊢ ( 𝜑 → 0s ≤s ( 𝐴 ·s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mulsge0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulsge0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		mulsge0d.3	⊢ ( 𝜑 → 0s ≤s 𝐴 )
4		mulsge0d.4	⊢ ( 𝜑 → 0s ≤s 𝐵 )
5		0no	⊢ 0s ∈ No
6	5	a1i	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 0s ∈ No )
7	1 2	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
8	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → ( 𝐴 ·s 𝐵 ) ∈ No )
9	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 𝐴 ∈ No )
10	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 𝐵 ∈ No )
11		simplr	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 0s <s 𝐴 )
12		simpr	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 0s <s 𝐵 )
13	9 10 11 12	mulsgt0d	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 0s <s ( 𝐴 ·s 𝐵 ) )
14	6 8 13	ltlesd	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s <s 𝐵 ) → 0s ≤s ( 𝐴 ·s 𝐵 ) )
15		lesid	⊢ ( 0s ∈ No → 0s ≤s 0s )
16	5 15	ax-mp	⊢ 0s ≤s 0s
17		oveq2	⊢ ( 0s = 𝐵 → ( 𝐴 ·s 0s ) = ( 𝐴 ·s 𝐵 ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ 0s = 𝐵 ) → ( 𝐴 ·s 0s ) = ( 𝐴 ·s 𝐵 ) )
19		muls01	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
20	1 19	syl	⊢ ( 𝜑 → ( 𝐴 ·s 0s ) = 0s )
21	20	adantr	⊢ ( ( 𝜑 ∧ 0s = 𝐵 ) → ( 𝐴 ·s 0s ) = 0s )
22	18 21	eqtr3d	⊢ ( ( 𝜑 ∧ 0s = 𝐵 ) → ( 𝐴 ·s 𝐵 ) = 0s )
23	16 22	breqtrrid	⊢ ( ( 𝜑 ∧ 0s = 𝐵 ) → 0s ≤s ( 𝐴 ·s 𝐵 ) )
24	23	adantlr	⊢ ( ( ( 𝜑 ∧ 0s <s 𝐴 ) ∧ 0s = 𝐵 ) → 0s ≤s ( 𝐴 ·s 𝐵 ) )
25		lesloe	⊢ ( ( 0s ∈ No ∧ 𝐵 ∈ No ) → ( 0s ≤s 𝐵 ↔ ( 0s <s 𝐵 ∨ 0s = 𝐵 ) ) )
26	5 2 25	sylancr	⊢ ( 𝜑 → ( 0s ≤s 𝐵 ↔ ( 0s <s 𝐵 ∨ 0s = 𝐵 ) ) )
27	4 26	mpbid	⊢ ( 𝜑 → ( 0s <s 𝐵 ∨ 0s = 𝐵 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 0s <s 𝐴 ) → ( 0s <s 𝐵 ∨ 0s = 𝐵 ) )
29	14 24 28	mpjaodan	⊢ ( ( 𝜑 ∧ 0s <s 𝐴 ) → 0s ≤s ( 𝐴 ·s 𝐵 ) )
30		oveq1	⊢ ( 0s = 𝐴 → ( 0s ·s 𝐵 ) = ( 𝐴 ·s 𝐵 ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 0s = 𝐴 ) → ( 0s ·s 𝐵 ) = ( 𝐴 ·s 𝐵 ) )
32		muls02	⊢ ( 𝐵 ∈ No → ( 0s ·s 𝐵 ) = 0s )
33	2 32	syl	⊢ ( 𝜑 → ( 0s ·s 𝐵 ) = 0s )
34	33	adantr	⊢ ( ( 𝜑 ∧ 0s = 𝐴 ) → ( 0s ·s 𝐵 ) = 0s )
35	31 34	eqtr3d	⊢ ( ( 𝜑 ∧ 0s = 𝐴 ) → ( 𝐴 ·s 𝐵 ) = 0s )
36	16 35	breqtrrid	⊢ ( ( 𝜑 ∧ 0s = 𝐴 ) → 0s ≤s ( 𝐴 ·s 𝐵 ) )
37		lesloe	⊢ ( ( 0s ∈ No ∧ 𝐴 ∈ No ) → ( 0s ≤s 𝐴 ↔ ( 0s <s 𝐴 ∨ 0s = 𝐴 ) ) )
38	5 1 37	sylancr	⊢ ( 𝜑 → ( 0s ≤s 𝐴 ↔ ( 0s <s 𝐴 ∨ 0s = 𝐴 ) ) )
39	3 38	mpbid	⊢ ( 𝜑 → ( 0s <s 𝐴 ∨ 0s = 𝐴 ) )
40	29 36 39	mpjaodan	⊢ ( 𝜑 → 0s ≤s ( 𝐴 ·s 𝐵 ) )