Theorem ltmuldivs2d

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

	Ref	Expression
Hypotheses	ltdivmulsd.1	|- ( ph -> A e. No )
	ltdivmulsd.2	|- ( ph -> B e. No )
	ltdivmulsd.3	|- ( ph -> C e. No )
	ltdivmulsd.4	|- ( ph -> 0s
Assertion	ltmuldivs2d	|- ( ph -> ( ( C x.s A ) A

Proof

Step	Hyp	Ref	Expression
1		ltdivmulsd.1	|- ( ph -> A e. No )
2		ltdivmulsd.2	|- ( ph -> B e. No )
3		ltdivmulsd.3	|- ( ph -> C e. No )
4		ltdivmulsd.4	|- ( ph -> 0s
5	4	gt0ne0sd	|- ( ph -> C =/= 0s )
6	3 5	recsexd	|- ( ph -> E. x e. No ( C x.s x ) = 1s )
7	1 2 3 4 6	ltmuldivs2wd	|- ( ph -> ( ( C x.s A ) A