Theorem slemul1ad

Description: Multiplication of both sides of surreal less-than or equal by a non-negative number. (Contributed by Scott Fenton, 17-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		slemul1ad.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		slemul1ad.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		slemul1ad.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		slemul1ad.4	⊢ ( 𝜑 → 0s ≤s 𝐶 )
5		slemul1ad.5	⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )
6	5	adantr	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐴 ≤s 𝐵 )
7	1	adantr	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐴 ∈ No )
8	2	adantr	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐵 ∈ No )
9	3	adantr	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐶 ∈ No )
10		simpr	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 0s <s 𝐶 )
11	7 8 9 10	slemul1d	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ) )
12	6 11	mpbid	⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) )
13		0sno	⊢ 0s ∈ No
14		slerflex	⊢ ( 0s ∈ No → 0s ≤s 0s )
15	13 14	mp1i	⊢ ( 𝜑 → 0s ≤s 0s )
16		muls01	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
17	1 16	syl	⊢ ( 𝜑 → ( 𝐴 ·s 0s ) = 0s )
18		muls01	⊢ ( 𝐵 ∈ No → ( 𝐵 ·s 0s ) = 0s )
19	2 18	syl	⊢ ( 𝜑 → ( 𝐵 ·s 0s ) = 0s )
20	15 17 19	3brtr4d	⊢ ( 𝜑 → ( 𝐴 ·s 0s ) ≤s ( 𝐵 ·s 0s ) )
21		oveq2	⊢ ( 0s = 𝐶 → ( 𝐴 ·s 0s ) = ( 𝐴 ·s 𝐶 ) )
22		oveq2	⊢ ( 0s = 𝐶 → ( 𝐵 ·s 0s ) = ( 𝐵 ·s 𝐶 ) )
23	21 22	breq12d	⊢ ( 0s = 𝐶 → ( ( 𝐴 ·s 0s ) ≤s ( 𝐵 ·s 0s ) ↔ ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ) )
24	20 23	syl5ibcom	⊢ ( 𝜑 → ( 0s = 𝐶 → ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ) )
25	24	imp	⊢ ( ( 𝜑 ∧ 0s = 𝐶 ) → ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) )
26		sleloe	⊢ ( ( 0s ∈ No ∧ 𝐶 ∈ No ) → ( 0s ≤s 𝐶 ↔ ( 0s <s 𝐶 ∨ 0s = 𝐶 ) ) )
27	13 3 26	sylancr	⊢ ( 𝜑 → ( 0s ≤s 𝐶 ↔ ( 0s <s 𝐶 ∨ 0s = 𝐶 ) ) )
28	4 27	mpbid	⊢ ( 𝜑 → ( 0s <s 𝐶 ∨ 0s = 𝐶 ) )
29	12 25 28	mpjaodan	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) )