Theorem slemul1d

Description: Multiplication of both sides of surreal less-than or equal by a positive number. (Contributed by Scott Fenton, 10-Mar-2025)

	Ref	Expression
Hypotheses	sltmul12d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	sltmul12d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	sltmul12d.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	sltmul12d.4	⊢ ( 𝜑 → 0s <s 𝐶 )
Assertion	slemul1d	⊢ ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sltmul12d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		sltmul12d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		sltmul12d.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		sltmul12d.4	⊢ ( 𝜑 → 0s <s 𝐶 )
5	2 1 3 4	sltmul1d	⊢ ( 𝜑 → ( 𝐵 <s 𝐴 ↔ ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ) )
6	5	notbid	⊢ ( 𝜑 → ( ¬ 𝐵 <s 𝐴 ↔ ¬ ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ) )
7		slenlt	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
9	1 3	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
10	2 3	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
11		slenlt	⊢ ( ( ( 𝐴 ·s 𝐶 ) ∈ No ∧ ( 𝐵 ·s 𝐶 ) ∈ No ) → ( ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ↔ ¬ ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ) )
12	9 10 11	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ↔ ¬ ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ) )
13	6 8 12	3bitr4d	⊢ ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) ) )