sltmuldiv2wd

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	sltmuldiv2wd	$⊢ φ \to ((C \cdot_{s} A) <_{s} B \leftrightarrow A <_{s} (B /_{su} 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 3	mulscomd	$⊢ φ \to A \cdot_{s} C = C \cdot_{s} A$
7	6	breq1d	$⊢ φ \to ((A \cdot_{s} C) <_{s} B \leftrightarrow (C \cdot_{s} A) <_{s} B)$
8	1 2 3 4 5	sltmuldivwd	$⊢ φ \to ((A \cdot_{s} C) <_{s} B \leftrightarrow A <_{s} (B /_{su} C))$
9	7 8	bitr3d	$⊢ φ \to ((C \cdot_{s} A) <_{s} B \leftrightarrow A <_{s} (B /_{su} C))$

Metamath Proof Explorer