Theorem divsrecd

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

	Ref	Expression
Hypotheses	divsrecd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	divsrecd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	divsrecd.3	⊢ ( 𝜑 → 𝐵 ≠ 0s )
Assertion	divsrecd	⊢ ( 𝜑 → ( 𝐴 /su 𝐵 ) = ( 𝐴 ·s ( 1s /su 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		divsrecd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		divsrecd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		divsrecd.3	⊢ ( 𝜑 → 𝐵 ≠ 0s )
4		1no	⊢ 1s ∈ No
5	4	a1i	⊢ ( 𝜑 → 1s ∈ No )
6	5 2 3	divscld	⊢ ( 𝜑 → ( 1s /su 𝐵 ) ∈ No )
7	2 1 6	muls12d	⊢ ( 𝜑 → ( 𝐵 ·s ( 𝐴 ·s ( 1s /su 𝐵 ) ) ) = ( 𝐴 ·s ( 𝐵 ·s ( 1s /su 𝐵 ) ) ) )
8	5 2 3	divscan2d	⊢ ( 𝜑 → ( 𝐵 ·s ( 1s /su 𝐵 ) ) = 1s )
9	8	oveq2d	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 ·s ( 1s /su 𝐵 ) ) ) = ( 𝐴 ·s 1s ) )
10	1	mulsridd	⊢ ( 𝜑 → ( 𝐴 ·s 1s ) = 𝐴 )
11	7 9 10	3eqtrd	⊢ ( 𝜑 → ( 𝐵 ·s ( 𝐴 ·s ( 1s /su 𝐵 ) ) ) = 𝐴 )
12	1 6	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s ( 1s /su 𝐵 ) ) ∈ No )
13	1 12 2 3	divmulsd	⊢ ( 𝜑 → ( ( 𝐴 /su 𝐵 ) = ( 𝐴 ·s ( 1s /su 𝐵 ) ) ↔ ( 𝐵 ·s ( 𝐴 ·s ( 1s /su 𝐵 ) ) ) = 𝐴 ) )
14	11 13	mpbird	⊢ ( 𝜑 → ( 𝐴 /su 𝐵 ) = ( 𝐴 ·s ( 1s /su 𝐵 ) ) )