Theorem sltmuldiv2d

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

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

Proof

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