sltdivmul2wd

Description: Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025)

	Ref	Expression
Hypotheses	sltdivmulwd.1	$⊢ φ \to A \in No$
	sltdivmulwd.2	$⊢ φ \to B \in No$
	sltdivmulwd.3	$⊢ φ \to C \in No$
	sltdivmulwd.4	$⊢ φ \to 0_{s} <_{s} C$
	sltdivmulwd.5	$⊢ φ \to \exists x \in No C \cdot_{s} x = 1_{s}$
Assertion	sltdivmul2wd	$⊢ φ \to ((A /_{su} C) <_{s} B \leftrightarrow A <_{s} (B \cdot_{s} C))$

Step	Hyp	Ref	Expression
1		sltdivmulwd.1	$⊢ φ \to A \in No$
2		sltdivmulwd.2	$⊢ φ \to B \in No$
3		sltdivmulwd.3	$⊢ φ \to C \in No$
4		sltdivmulwd.4	$⊢ φ \to 0_{s} <_{s} C$
5		sltdivmulwd.5	$⊢ φ \to \exists x \in No C \cdot_{s} x = 1_{s}$
6	1 2 3 4 5	sltdivmulwd	$⊢ φ \to ((A /_{su} C) <_{s} B \leftrightarrow A <_{s} (C \cdot_{s} B))$
7	2 3	mulscomd	$⊢ φ \to B \cdot_{s} C = C \cdot_{s} B$
8	7	breq2d	$⊢ φ \to (A <_{s} (B \cdot_{s} C) \leftrightarrow A <_{s} (C \cdot_{s} B))$
9	6 8	bitr4d	$⊢ φ \to ((A /_{su} C) <_{s} B \leftrightarrow A <_{s} (B \cdot_{s} C))$

Metamath Proof Explorer