Theorem divsrecd

Description: Relationship between surreal division and reciprocal. (Contributed by Scott Fenton, 13-Aug-2025)

	Ref	Expression
Hypotheses	divsrecd.1	|- ( ph -> A e. No )
	divsrecd.2	|- ( ph -> B e. No )
	divsrecd.3	|- ( ph -> B =/= 0s )
Assertion	divsrecd	|- ( ph -> ( A /su B ) = ( A x.s ( 1s /su B ) ) )

Proof

Step	Hyp	Ref	Expression
1		divsrecd.1	|- ( ph -> A e. No )
2		divsrecd.2	|- ( ph -> B e. No )
3		divsrecd.3	|- ( ph -> B =/= 0s )
4		1sno	|- 1s e. No
5	4	a1i	|- ( ph -> 1s e. No )
6	5 2 3	divscld	|- ( ph -> ( 1s /su B ) e. No )
7	2 1 6	muls12d	|- ( ph -> ( B x.s ( A x.s ( 1s /su B ) ) ) = ( A x.s ( B x.s ( 1s /su B ) ) ) )
8	5 2 3	divscan2d	|- ( ph -> ( B x.s ( 1s /su B ) ) = 1s )
9	8	oveq2d	|- ( ph -> ( A x.s ( B x.s ( 1s /su B ) ) ) = ( A x.s 1s ) )
10	1	mulsridd	|- ( ph -> ( A x.s 1s ) = A )
11	7 9 10	3eqtrd	|- ( ph -> ( B x.s ( A x.s ( 1s /su B ) ) ) = A )
12	1 6	mulscld	|- ( ph -> ( A x.s ( 1s /su B ) ) e. No )
13	1 12 2 3	divsmuld	|- ( ph -> ( ( A /su B ) = ( A x.s ( 1s /su B ) ) <-> ( B x.s ( A x.s ( 1s /su B ) ) ) = A ) )
14	11 13	mpbird	|- ( ph -> ( A /su B ) = ( A x.s ( 1s /su B ) ) )