Metamath Proof Explorer

Theorem ltmuldivsd

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

	Ref	Expression
Hypotheses	ltdivmulsd.1	$⊢ φ \to A \in No$
	ltdivmulsd.2	$⊢ φ \to B \in No$
	ltdivmulsd.3	$⊢ φ \to C \in No$
	ltdivmulsd.4	$⊢ φ \to 0_{s} <_{s} C$
Assertion	ltmuldivsd	$⊢ φ \to ((A \cdot_{s} C) <_{s} B \leftrightarrow A <_{s} (B /_{su} C))$

Step	Hyp	Ref	Expression
1		ltdivmulsd.1	$⊢ φ \to A \in No$
2		ltdivmulsd.2	$⊢ φ \to B \in No$
3		ltdivmulsd.3	$⊢ φ \to C \in No$
4		ltdivmulsd.4	$⊢ φ \to 0_{s} <_{s} C$
5	4	gt0ne0sd	$⊢ φ \to C \neq 0_{s}$
6	3 5	recsexd	$⊢ φ \to \exists x \in No C \cdot_{s} x = 1_{s}$
7	1 2 3 4 6	ltmuldivswd	$⊢ φ \to ((A \cdot_{s} C) <_{s} B \leftrightarrow A <_{s} (B /_{su} C))$